Theorem: LoVe.Set.unordered_pair_comm (LoVe/LoVelib.lean)

State before:
α : Type
a b : α
⊢ {a, b} = {b, a}
Tactic:
apply Set.ext
State after:
case h
α : Type
a b : α
⊢ ∀ (x : α), x ∈ {a, b} ↔ x ∈ {b, a}

State before:
case h
α : Type
a b : α
⊢ ∀ (x : α), x ∈ {a, b} ↔ x ∈ {b, a}
Tactic:
simp [insert, singleton, Set.insert, Set.singleton]
State after:
case h
α : Type
a b : α
⊢ ∀ (x : α), x = a ∨ x = b ↔ x = b ∨ x = a

State before:
case h
α : Type
a b : α
⊢ ∀ (x : α), x = a ∨ x = b ↔ x = b ∨ x = a
Tactic:
aesop
State after:
no goals