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

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

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

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