case mp =>
  intro (_ : (a₁, b₁) ≃ (a₂, b₂))
  show a₁ ≃ a₂ ∧ b₁ ≃ b₂
  have elem_eqv : expanded_eqv := ‹(a₁, b₁) ≃ (a₂, b₂)›
  have : a₁ ≃ a₂ := elem_eqv Hand.L
  have : b₁ ≃ b₂ := elem_eqv Hand.R
  exact And.intro ‹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
⊢ (a₁, b₁) ≃ (a₂, b₂) → a₁ ≃ a₂ ∧ b₁ ≃ b₂
no goals