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

State before:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
⊢ (symmDiff {i} S).sum f = f i + S.sum f
Tactic:
by_cases h : i ∈ S
State after:
case pos
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∈ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f

case neg
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∉ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f

State before:
case pos
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∈ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f
Tactic:
rw [symmDiff_singleton_eq_erase h, ← S.add_sum_erase f h, CharTwo.add_add_cancel_left]
State after:
no goals

State before:
case neg
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∉ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f
Tactic:
rw [symmDiff_singleton_eq_insert h, Finset.sum_insert h]
State after:
no goals