Theorem: Setoid.prod.pair (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
⊢ (a1, b1) ≈ (a2, b2) ↔ a1 ≈ a2 ∧ b1 ≈ b2
Tactic:
constructor <;> (intro h; cases h; constructor <;> assumption)
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
⊢ a1 ≈ a2 ∧ b1 ≈ b2 → (a1, b1) ≈ (a2, b2)
Tactic:
intro h
State after:
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)

State before:
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)
Tactic:
cases h
State after:
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)

State before:
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)
Tactic:
constructor <;> assumption
State after:
no goals