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

State before:
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
⊢ ∏ 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 ℕ
hs : n = 0 → s = ∅
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n

State before:
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
intro x hx
State after:
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
x : ℕ
hx : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n

State before:
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
x : ℕ
hx : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
cases n with
| zero => simp at hs; rw [hs] at hx; contradiction
| succ n => apply Nat.pow_factorization_choose_le; simp
State after:
no goals

State before:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ s
hs : Nat.zero = 0 → s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Tactic:
simp at hs
State after:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ s
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero

State before:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ s
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Tactic:
rw [hs] at hx
State after:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ ∅
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero

State before:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ ∅
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Tactic:
contradiction
State after:
no goals

State before:
case h.succ
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom (Nat.succ n))) x ≤ 2 * Nat.succ n
Tactic:
apply Nat.pow_factorization_choose_le
State after:
case h.succ.hn
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ 0 < 2 * Nat.succ n

State before:
case h.succ.hn
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ 0 < 2 * Nat.succ n
Tactic:
simp
State after:
no goals