Theorem: IMOSL.Extra.symmDiff_singleton_eq_erase (IMOSLLean4/Extra/CharTwo/Finset.lean)

State before:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
⊢ symmDiff {i} S = S.erase i
Tactic:
have h0 : {i} \ S = ∅ :=
  Finset.sdiff_eq_empty_iff_subset.mpr λ c h0 ↦ Finset.mem_singleton.mp h0 ▸ h
State after:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ symmDiff {i} S = S.erase i

State before:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ symmDiff {i} S = S.erase i
Tactic:
rw [symmDiff, Finset.sdiff_singleton_eq_erase, h0]
State after:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ ∅ ⊔ S.erase i = S.erase i

State before:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ ∅ ⊔ S.erase i = S.erase i
Tactic:
exact bot_sup_eq _
State after:
no goals