Theorem: sum_range_sym_mul_compl (DividedPowers/BasicLemmas.lean)

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) =
    m * n - ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i
Tactic:
suffices h : (((Finset.range (n + 1)).sum fun i => Multiset.count i k * (n - i)) +
      (Finset.range (n + 1)).sum fun i => Multiset.count i k * i) = m * n by
  rw [← h, Nat.add_sub_cancel]
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) + ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i =
    m * n

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) + ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i =
    m * n
Tactic:
rw [← Finset.sum_add_distrib]
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), (Multiset.count x ↑k * (n - x) + Multiset.count x ↑k * x) = m * n

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), (Multiset.count x ↑k * (n - x) + Multiset.count x ↑k * x) = m * n
Tactic:
simp_rw [← mul_add]
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n
Tactic:
have :
  ∀ x ∈ Finset.range (n + 1),
    Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n := by
  intro x hx
  rw [Nat.sub_add_cancel (Nat.lt_succ_iff.mp (Finset.mem_range.mp hx))]
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
this : ∀ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
this : ∀ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
⊢ ∑ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = m * n
Tactic:
rw [Finset.sum_congr rfl this, ← Finset.sum_mul, range_sym_prop hk]
State after:
no goals

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
h :
  ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) + ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i =
    m * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * (n - i) =
    m * n - ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i
Tactic:
rw [← h, Nat.add_sub_cancel]
State after:
no goals

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∀ x ∈ Finset.range (n + 1), Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
Tactic:
intro x hx
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ Multiset.count x ↑k * (n - x + x) = Multiset.count x ↑k * n
Tactic:
rw [Nat.sub_add_cancel (Nat.lt_succ_iff.mp (Finset.mem_range.mp hx))]
State after:
no goals