Theorem: range_sym_weighted_sum_le (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 * i ≤ m * n
Tactic:
suffices h : ∀ i ∈ Finset.range (n + 1), Multiset.count i k * i ≤ Multiset.count i k * n by
  apply le_trans (Finset.sum_le_sum h)
  rw [← Finset.sum_mul, range_sym_prop hk]
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
⊢ ∀ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ Multiset.count i ↑k * 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 * i ≤ Multiset.count i ↑k * n
Tactic:
intro i hi
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n

State before:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
Tactic:
apply Nat.mul_le_mul_left
State after:
case h
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i ≤ n

State before:
case h
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ i ≤ n
Tactic:
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
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 * i ≤ Multiset.count i ↑k * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ m * n
Tactic:
apply le_trans (Finset.sum_le_sum h)
State after:
m n : ℕ
k : Sym ℕ m
hk : k ∈ (Finset.range (n + 1)).sym m
h : ∀ i ∈ Finset.range (n + 1), Multiset.count i ↑k * i ≤ Multiset.count i ↑k * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * n ≤ m * n

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 * i ≤ Multiset.count i ↑k * n
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k * n ≤ m * n
Tactic:
rw [← Finset.sum_mul, range_sym_prop hk]
State after:
no goals