-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem hasSum_pow_div_log_of_abs_lt_one {x : ℝ} (h : |x| < 1) :
    HasSum (fun n : ℕ => x ^ (n + 1) / (n + 1)) (-log (1 - x))

Proof state:
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)

Tactic:
have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)

Result:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)

Proof state:
x : ℝ
h : |x| < 1
⊢ HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-log (1 - x))

Tactic:
rw [Summable.hasSum_iff_tendsto_nat]

Result:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))

x : ℝ
h : |x| < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)

Proof state:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]

Result:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => ‖∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)

Proof state:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))

Tactic:
refine (tendsto_const_nhds.mul ?_).div_const _

Result:
x : ℝ
h : |x| < 1
⊢ Tendsto (HPow.hPow |x|) atTop (𝓝 0)

Proof state:
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ ≤ |x| ^ i

Tactic:
calc
  ‖x ^ (i + 1) / (i + 1)‖ = |x| ^ (i + 1) / (i + 1) := by
    have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
    rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
  _ ≤ |x| ^ (i + 1) / (0 + 1) := by
    gcongr
    exact i.cast_nonneg
  _ ≤ |x| ^ i := by
    simpa [pow_succ] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)

Result:
no goals

Proof state:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))

Tactic:
simp only [pow_succ']

Result:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))

Proof state:
x : ℝ
h : |x| < 1
this : Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)

Tactic:
simpa

Result:
no goals

Proof state:
x : ℝ
h : |x| < 1
⊢ Tendsto (HPow.hPow |x|) atTop (𝓝 0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg _) h

Result:
no goals

Proof state:
x : ℝ
h : |x| < 1
⊢ Summable fun n => x ^ (n + 1) / (↑n + 1)

Tactic:
refine .of_norm_bounded _ (summable_geometric_of_lt_one (abs_nonneg _) h) fun i => ?_

Result:
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ ≤ |x| ^ i

Proof state:
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (↑i + 1) ≤ |x| ^ (i + 1) / (0 + 1)

Tactic:
gcongr

Result:
case h.bc
x : ℝ
h : |x| < 1
i : ℕ
⊢ 0 ≤ ↑i

Proof state:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => ‖∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) - -log (1 - x)‖) atTop (𝓝 0)

Tactic:
simp only [norm_eq_abs, sub_neg_eq_add]

Result:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => |∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) + log (1 - x)|) atTop (𝓝 0)

Proof state:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun e => |∑ i ∈ Finset.range e, x ^ (i + 1) / (↑i + 1) + log (1 - x)|) atTop (𝓝 0)

Tactic:
refine squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) ?_

Result:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)

Proof state:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)

Tactic:
suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by
  simpa

Result:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun t => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))

Proof state:
case h.bc
x : ℝ
h : |x| < 1
i : ℕ
⊢ 0 ≤ ↑i

Tactic:
exact i.cast_nonneg

Result:
no goals

Proof state:
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / (0 + 1) ≤ |x| ^ i

Tactic:
simpa [pow_succ] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)

Result:
no goals

Proof state:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ ↑i + 1
⊢ ‖x ^ (i + 1) / (↑i + 1)‖ = |x| ^ (i + 1) / (↑i + 1)

Tactic:
rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]

Result:
no goals