Theorem: sdiff_singleton_is_erase (Bml/Setsimp.lean)

State before:
X : Finset Formula
ϕ : Formula
⊢ X \ {ϕ} = X.erase ϕ
Tactic:
induction X using Finset.induction_on
State after:
case empty
ϕ : Formula
⊢ ∅ \ {ϕ} = ∅.erase ϕ

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ

State before:
case empty
ϕ : Formula
⊢ ∅ \ {ϕ} = ∅.erase ϕ

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ
Tactic:
simp
State after:
case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ

State before:
case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ \ {ϕ} = s✝.erase ϕ
⊢ insert a✝² s✝ \ {ϕ} = (insert a✝² s✝).erase ϕ
Tactic:
ext1
State after:
case insert.a
ϕ a✝³ : Formula
s✝ : Finset Formula
a✝² : a✝³ ∉ s✝
a✝¹ : s✝ \ {ϕ} = s✝.erase ϕ
a✝ : Formula
⊢ a✝ ∈ insert a✝³ s✝ \ {ϕ} ↔ a✝ ∈ (insert a✝³ s✝).erase ϕ

State before:
case insert.a
ϕ a✝³ : Formula
s✝ : Finset Formula
a✝² : a✝³ ∉ s✝
a✝¹ : s✝ \ {ϕ} = s✝.erase ϕ
a✝ : Formula
⊢ a✝ ∈ insert a✝³ s✝ \ {ϕ} ↔ a✝ ∈ (insert a✝³ s✝).erase ϕ
Tactic:
aesop
State after:
no goals