Theorem: Quotient.prod_eq_mk (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
aa : Quotient sa
bb : Quotient sb
a : α
b : β
⊢ prod aa bb = ⟦(a, b)⟧ ↔ aa = ⟦a⟧ ∧ bb = ⟦b⟧
Tactic:
rcases aa.exists_rep with ⟨a',rfl⟩
State after:
case intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
bb : Quotient sb
a : α
b : β
a' : α
⊢ prod ⟦a'⟧ bb = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ bb = ⟦b⟧

State before:
case intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
bb : Quotient sb
a : α
b : β
a' : α
⊢ prod ⟦a'⟧ bb = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ bb = ⟦b⟧
Tactic:
rcases bb.exists_rep with ⟨b',rfl⟩
State after:
case intro.intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
a : α
b : β
a' : α
b' : β
⊢ prod ⟦a'⟧ ⟦b'⟧ = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ ⟦b'⟧ = ⟦b⟧

State before:
case intro.intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
a : α
b : β
a' : α
b' : β
⊢ prod ⟦a'⟧ ⟦b'⟧ = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ ⟦b'⟧ = ⟦b⟧
Tactic:
simp [Setoid.prod]
State after:
no goals