Theorem: range_sym_prop (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 = m
Tactic:
simp only [Finset.mem_sym_iff] at hk
State after:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = m

State before:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = m
Tactic:
simp_rw [← k.prop]
State after:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = Multiset.card ↑k

State before:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = Multiset.card ↑k
Tactic:
rw [← Multiset.toFinset_sum_count_eq]
State after:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k

State before:
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k = ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k
Tactic:
apply symm
State after:
case a
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k = ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k

State before:
case a
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∑ a ∈ (↑k).toFinset, Multiset.count a ↑k = ∑ i ∈ Finset.range (n + 1), Multiset.count i ↑k
Tactic:
apply Finset.sum_subset_zero_on_sdiff
State after:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ (↑k).toFinset ⊆ Finset.range (n + 1)

case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ Finset.range (n + 1) \ (↑k).toFinset, Multiset.count x ↑k = 0

case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ (↑k).toFinset, Multiset.count x ↑k = Multiset.count x ↑k

State before:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ (↑k).toFinset ⊆ Finset.range (n + 1)
Tactic:
intro i hi
State after:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ (↑k).toFinset
⊢ i ∈ Finset.range (n + 1)

State before:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ (↑k).toFinset
⊢ i ∈ Finset.range (n + 1)
Tactic:
simp only [Sym.val_eq_coe, Multiset.mem_toFinset, Sym.mem_coe] at hi
State after:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ k
⊢ i ∈ Finset.range (n + 1)

State before:
case a.h
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
i : ℕ
hi : i ∈ k
⊢ i ∈ Finset.range (n + 1)
Tactic:
exact hk i hi
State after:
no goals

State before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ Finset.range (n + 1) \ (↑k).toFinset, Multiset.count x ↑k = 0
Tactic:
intro x hx
State after:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x ∈ Finset.range (n + 1) \ (↑k).toFinset
⊢ Multiset.count x ↑k = 0

State before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x ∈ Finset.range (n + 1) \ (↑k).toFinset
⊢ Multiset.count x ↑k = 0
Tactic:
simp only [Sym.val_eq_coe, Finset.mem_sdiff, Finset.mem_range, Multiset.mem_toFinset, Sym.mem_coe] at hx
State after:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ Multiset.count x ↑k = 0

State before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ Multiset.count x ↑k = 0
Tactic:
simp only [Multiset.count_eq_zero, Sym.mem_coe]
State after:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ x ∉ k

State before:
case a.hg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
hx : x < n + 1 ∧ x ∉ k
⊢ x ∉ k
Tactic:
exact hx.2
State after:
no goals

State before:
case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
⊢ ∀ x ∈ (↑k).toFinset, Multiset.count x ↑k = Multiset.count x ↑k
Tactic:
intro x _
State after:
case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
a✝ : x ∈ (↑k).toFinset
⊢ Multiset.count x ↑k = Multiset.count x ↑k

State before:
case a.hfg
m n : ℕ
k : Sym ℕ m
hk : ∀ a ∈ k, a ∈ Finset.range (n + 1)
x : ℕ
a✝ : x ∈ (↑k).toFinset
⊢ Multiset.count x ↑k = Multiset.count x ↑k
Tactic:
rfl
State after:
no goals