Theorem: FactorizationCentralBinom.prodIcoPowLePow (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
n : ℕ
s : Finset ℕ
hn : 0 < n
⊢ ∏ p in s, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ (2 * n) ^ Finset.card s
Tactic:
apply Finset.prod_le_pow_card
State after:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n

State before:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
intro x _
State after:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n

State before:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
apply Nat.pow_factorization_choose_le
State after:
case h.hn
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ 0 < 2 * n

State before:
case h.hn
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ 0 < 2 * n
Tactic:
linarith
State after:
no goals