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