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

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