Theorem: finset_sum_partition (Ray/Misc/Bounds.lean)

State before:
A B : Finset ℕ
f : ℕ → ℂ
⊢ A.sum f = (A \ B).sum f + (A ∩ B).sum f
Tactic:
have ha : A = A \ B ∪ A ∩ B := finset_partition A B
State after:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ A.sum f = (A \ B).sum f + (A ∩ B).sum f

State before:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ A.sum f = (A \ B).sum f + (A ∩ B).sum f
Tactic:
nth_rw 1 [ha]
State after:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ (A \ B ∪ A ∩ B).sum f = (A \ B).sum f + (A ∩ B).sum f

State before:
A B : Finset ℕ
f : ℕ → ℂ
ha : A = A \ B ∪ A ∩ B
⊢ (A \ B ∪ A ∩ B).sum f = (A \ B).sum f + (A ∩ B).sum f
Tactic:
exact Finset.sum_union (Finset.disjoint_sdiff_inter A B)
State after:
no goals