x✝ y x : ℝ
hx : 0 ≤ x
⊢ x ^ 2 / 2 = x ^ 2 / (1 + 1)
x✝ y x : ℝ
hx : 0 ≤ x
⊢ 1 + x + x ^ 2 / 2 = ∑ i in range 3, x ^ i / ↑i !
simp [Finset.sum_range_succ]
no goals
x✝ y x : ℝ
hx : 0 ≤ x
⊢ x ^ 2 / 2 = x ^ 2 / (1 + 1)
ring_nf