Theorem: union_singleton_is_insert (Pdl/Setsimp.lean)

State before:
X : Finset Formula
ϕ : Formula
⊢ X ∪ {ϕ} = insert ϕ X
Tactic:
have fo := Finset.insert_eq ϕ X
State after:
X : Finset Formula
ϕ : Formula
fo : insert ϕ X = {ϕ} ∪ X
⊢ X ∪ {ϕ} = insert ϕ X

State before:
X : Finset Formula
ϕ : Formula
fo : insert ϕ X = {ϕ} ∪ X
⊢ X ∪ {ϕ} = insert ϕ X
Tactic:
aesop
State after:
no goals