rw [← Finset.prod_range_mul_prod_Ico _ (Nat.zero_lt_succ _)]
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
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