cases h
case mpr
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
h : a1 ≈ a2 ∧ b1 ≈ b2
⊢ (a1, b1) ≈ (a2, b2)
case mpr.intro
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
left✝ : a1 ≈ a2
right✝ : b1 ≈ b2
⊢ (a1, b1) ≈ (a2, b2)