have : b₁ ≃ b₂ := elem_eqv Hand.R
α β : 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
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂
α β : 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
x✝ : (a₁, b₁) ≃ (a₂, b₂)
elem_eqv : expanded_eqv
this✝ : a₁ ≃ a₂
this : b₁ ≃ b₂
⊢ a₁ ≃ a₂ ∧ b₁ ≃ b₂