Theorem: prodRangePowFactorization (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
b n : ℕ
⊢ ∏ p in Finset.range b, p ^ ↑(Nat.factorization n) p = ∏ p in Finset.Ico 1 b, p ^ ↑(Nat.factorization n) p
Tactic:
cases b with
| zero => simp
| succ b =>
  rw [← Finset.prod_range_mul_prod_Ico _ (Nat.zero_lt_succ _)]
  simp
State after:
no goals

State before:
case zero
n : ℕ
⊢ ∏ p in Finset.range Nat.zero, p ^ ↑(Nat.factorization n) p =
    ∏ p in Finset.Ico 1 Nat.zero, p ^ ↑(Nat.factorization n) p
Tactic:
simp
State after:
no goals

State before:
case succ
n b : ℕ
⊢ ∏ p in Finset.range (Nat.succ b), p ^ ↑(Nat.factorization n) p =
    ∏ p in Finset.Ico 1 (Nat.succ b), p ^ ↑(Nat.factorization n) p
Tactic:
rw [← Finset.prod_range_mul_prod_Ico _ (Nat.zero_lt_succ _)]
State after:
case succ
n b : ℕ
⊢ (∏ k in Finset.range (Nat.succ 0), k ^ ↑(Nat.factorization n) k) *
      ∏ k in Finset.Ico (Nat.succ 0) (Nat.succ b), k ^ ↑(Nat.factorization n) k =
    ∏ p in Finset.Ico 1 (Nat.succ b), p ^ ↑(Nat.factorization n) p

State before:
case succ
n b : ℕ
⊢ (∏ k in Finset.range (Nat.succ 0), k ^ ↑(Nat.factorization n) k) *
      ∏ k in Finset.Ico (Nat.succ 0) (Nat.succ b), k ^ ↑(Nat.factorization n) k =
    ∏ p in Finset.Ico 1 (Nat.succ b), p ^ ↑(Nat.factorization n) p
Tactic:
simp
State after:
no goals