Theorem: Set.insert_comm (GMLInit/Data/Set/Insert.lean)

State before:
α : Sort u_1
a₁ a₂ : α
s : Set α
⊢ (s.insert a₁).insert a₂ = ((Set.pure a₂).union (Set.pure a₁)).union s
Tactic:
rw [union_assoc]
State after:
no goals

State before:
α : Sort u_1
a₁ a₂ : α
s : Set α
⊢ ((Set.pure a₂).union (Set.pure a₁)).union s = ((Set.pure a₁).union (Set.pure a₂)).union s
Tactic:
rw [union_comm (Set.pure a₁) (Set.pure a₂)]
State after:
no goals

State before:
α : Sort u_1
a₁ a₂ : α
s : Set α
⊢ ((Set.pure a₁).union (Set.pure a₂)).union s = (Set.pure a₁).union ((Set.pure a₂).union s)
Tactic:
rw [union_assoc]
State after:
no goals