book18/Series2.lean:204:31: error: unsolved goals
x : ℝ
hx : x ≠ 0
hne : ∀ (n : ℕ), x ^ n / ↑n.factorial ≠ 0
hlim : Tendsto (fun n => |x| / (↑n + 1)) atTop (𝓝 0)
n : ℕ
hx' : |x| ≠ 0
hf : ↑n.factorial ≠ 0
hn1 : ↑n + 1 ≠ 0
⊢ |x| ^ (n + 1) * (↑n + 1) * ↑n.factorial = |(↑n + 1) * ↑n.factorial| * |x| ^ n * |x|
'Book18Series2.dominated_by_geometric' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series2.terms_tend_to_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series2.ratio_test_converges' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series2.ratio_test_diverges' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series2.alternating_series_test' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series2.control_alternating_needs_limit_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series2.power_series_abel' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series2.exp_series_converges_of_ne_zero' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]