p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p =
    Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
conv => rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1) =
    ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p =
    Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1
rw [eq_comm]
case h
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (factorization (choose n k)).support ⊆ Finset.range (n + 1)

case hf
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      ¬x ∈ (factorization (choose n k)).support → (fun x x_1 => x ^ x_1) x (↑(factorization (choose n k)) x) = 1
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1) =
    ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p
apply Finset.prod_subset
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p ∈ Finset.range (n + 1)
case h
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (factorization (choose n k)).support ⊆ Finset.range (n + 1)
intro p hp
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p < n + 1
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p ∈ Finset.range (n + 1)
rw [Finset.mem_range]
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ ¬p ∈ (factorization (choose n k)).support
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p < n + 1
contrapose! hp
no goals
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ ¬p ∈ (factorization (choose n k)).support
rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
case hf
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : ¬p ∈ (factorization (choose n k)).support
⊢ (fun x x_1 => x ^ x_1) p (↑(factorization (choose n k)) p) = 1
case hf
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      ¬x ∈ (factorization (choose n k)).support → (fun x x_1 => x ^ x_1) x (↑(factorization (choose n k)) x) = 1
intro p _ h2
no goals
case hf
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : ¬p ∈ (factorization (choose n k)).support
⊢ (fun x x_1 => x ^ x_1) p (↑(factorization (choose n k)) p) = 1
simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]