Theorem: IMOSL.Extra.CharTwo.symmDiff_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
S T : Finset ι
⊢ (symmDiff S T).sum f = S.sum f + T.sum f
Tactic:
revert T
State after:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ (T : Finset ι), (symmDiff S T).sum f = S.sum f + T.sum f

State before:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ (T : Finset ι), (symmDiff S T).sum f = S.sum f + T.sum f
Tactic:
apply Finset.induction
State after:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f

case insert
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s → (symmDiff S s).sum f = S.sum f + s.sum f → (symmDiff S (insert a s)).sum f = S.sum f + (insert a s).sum f

State before:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f
Tactic:
have h : symmDiff S ∅ = S := by exact symmDiff_bot _
State after:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
h : symmDiff S ∅ = S
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f

State before:
case empty
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
h : symmDiff S ∅ = S
⊢ (symmDiff S ∅).sum f = S.sum f + ∅.sum f
Tactic:
rw [Finset.sum_empty, add_zero, h]
State after:
no goals

State before:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ symmDiff S ∅ = S
Tactic:
exact symmDiff_bot _
State after:
no goals

State before:
case insert
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s → (symmDiff S s).sum f = S.sum f + s.sum f → (symmDiff S (insert a s)).sum f = S.sum f + (insert a s).sum f
Tactic:
intro i T h h0
State after:
case insert
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
S : Finset ι
i : ι
T : Finset ι
h : i ∉ T
h0 : (symmDiff S T).sum f = S.sum f + T.sum f
⊢ (symmDiff S (insert i T)).sum f = S.sum f + (insert i T).sum f

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