rw [Finset.prod_Ico_succ_top <| Nat.le_add_left 1 n]
case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ ∏ x ∈ Ico 1 (n + 1).succ, (↑x + 1) / ↑x = ↑(n + 1) + 1
case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ (∏ k ∈ Ico 1 (n + 1), (↑k + 1) / ↑k) * ((↑(n + 1) + 1) / ↑(n + 1)) = ↑(n + 1) + 1