case zero

⊢ 0 < W Nat.zero

case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (Nat.succ k)
k : ℕ
⊢ 0 < W k
induction' k with k hk
case zero

⊢ 0 < ∏ i in range Nat.zero, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
case zero

⊢ 0 < W Nat.zero
unfold W
no goals
case zero

⊢ 0 < ∏ i in range Nat.zero, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
simp
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (Nat.succ k)
rw [W_succ]
no goals
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))
refine' mul_pos hk (mul_pos (div_pos _ _) (div_pos _ _)) <;> positivity