Theorem: LoVe.UPair.mk_symm (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
α : Type
a b : α
⊢ Quotient.mk (Setoid α) (a, b) = Quotient.mk (Setoid α) (b, a)
Tactic:
apply Quotient.sound
State after:
case a
α : Type
a b : α
⊢ (a, b) ≈ (b, a)

State before:
case a
α : Type
a b : α
⊢ (a, b) ≈ (b, a)
Tactic:
rw [UPair.Setoid_Iff]
State after:
case a
α : Type
a b : α
⊢ {(a, b).fst, (a, b).snd} = {(b, a).fst, (b, a).snd}

State before:
case a
α : Type
a b : α
⊢ {(a, b).fst, (a, b).snd} = {(b, a).fst, (b, a).snd}
Tactic:
simp [Set.unordered_pair_comm]
State after:
no goals