apply Iff.intro
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ (a₁, b₁) ≃ (a₂, b₂) ↔ a₁ ≃ a₂ ∧ b₁ ≃ b₂
case mp
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ (a₁, b₁) ≃ (a₂, b₂) → a₁ ≃ a₂ ∧ b₁ ≃ b₂

case mpr
α β : Type
inst✝¹ : EqvOp α
inst✝ : EqvOp β
a₁ a₂ : α
b₁ b₂ : β
dffp : {α β : Type} → α × β → (hand : Hand) → hand.pick α β := @depFn_from_prod
expanded_eqv : Prop := ∀ (hand : Hand), dffp (a₁, b₁) hand ≃ dffp (a₂, b₂) hand
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂ → (a₁, b₁) ≃ (a₂, b₂)