awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
n₁ : ‖F' y‖ = HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2|
n₂ :
  HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2| = HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
n₃ :
  HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2) ≤ HPow.hPow (β := ℕ) x 2 ^ n / (1 - HPow.hPow (β := ℕ) x 2)
⊢ ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
have n₄ : HPow.hPow (β := ℕ) x 2 ^ n / (1 - HPow.hPow (β := ℕ) x 2) ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: calc
      ‖F' y‖ = (y ^ 2) ^ n / |1 - y ^ 2| := by simp [F']
      _ = (y ^ 2) ^ n / (1 - y ^ 2) := by rw [abs_of_pos (by simpa [abs_lt] using hI hy)]
      _ ≤ (x ^ 2) ^ n / (1 - x ^ 2) := by gcongr ?_ ^ n / (1 - ?_); simpa [abs_lt] using h
      _ ≤ |x| ^ (2 * n) / (1 - x ^ 2) := by simp [pow_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
⊢ |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
have B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: have B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - x ^ 2) := fun y hy ↦ by
    have : y ^ 2 ≤ x ^ 2 := sq_le_sq.2 (abs_le.2 hy)
    calc
      ‖F' y‖ = (y ^ 2) ^ n / |1 - y ^ 2| := by simp [F']
      _ = (y ^ 2) ^ n / (1 - y ^ 2) := by rw [abs_of_pos (by simpa [abs_lt] using hI hy)]
      _ ≤ (x ^ 2) ^ n / (1 - x ^ 2) := by gcongr ?_ ^ n / (1 - ?_); simpa [abs_lt] using h
      _ ≤ |x| ^ (2 * n) / (1 - x ^ 2) := by simp [pow_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
have C : ‖F x - F 0‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2) * ‖x - 0‖
Tactic: have C : ‖F x - F 0‖ ≤ |x| ^ (2 * n) / (1 - x ^ 2) * ‖x - 0‖ :=
    (convex_Icc (-|x|) |x|).norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ (hI hy)).hasDerivWithinAt) B
      (by simp) (by simp [le_abs_self, neg_le, neg_le_abs x])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
⊢ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤ 1 / 2 * log ((1 + x) / (1 - x))
have A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
Tactic: have A : ∀ y ∈ Icc 0 x, HasDerivAt F (F' y) y := by
    intro y hy
    exact hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range _ (by grind) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
⊢ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤ 1 / 2 * log ((1 + x) / (1 - x))
have suffices : MonotoneOn F (Set.Icc 0 x)
Tactic: suffices MonotoneOn F (Icc 0 x) by simpa [F] using this ⟨le_rfl, h₀⟩ ⟨h₀, le_rfl⟩ h₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
⊢ MonotoneOn F (Set.Icc 0 x)
have refine : ∀ x_1 ∈ interior (Set.Icc 0 x), 0 ≤ F' x_1
Tactic: refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc 0 x)
    (fun y hy ↦ (A y hy).continuousAt.continuousWithinAt)
    (fun y hy ↦ (A y (interior_subset hy)).hasDerivWithinAt) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ interior (Set.Icc 0 x)
⊢ 0 ≤ F' y
have hy₁ : 0 < y ∧ y < x
Tactic: simp only [interior_Icc, Set.mem_Ioo] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : 0 < y ∧ y < x
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) y 2
have x₁ : 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
Tactic: calc
    0 ≤ 1 - x ^ 2 := by simp [abs_of_nonneg h₀, h.le]
    _ ≤ 1 - y ^ 2 := sub_le_sub_left (pow_le_pow_left₀ hy.1.le hy.2.le 2) 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : 0 < y ∧ y < x
⊢ 0 ≤ F' y
have this : 0 ≤ 1 - HPow.hPow (β := ℕ) y 2
Tactic: have : 0 ≤ 1 - y ^ 2 := by calc
    0 ≤ 1 - x ^ 2 := by simp [abs_of_nonneg h₀, h.le]
    _ ≤ 1 - y ^ 2 := sub_le_sub_left (pow_le_pow_left₀ hy.1.le hy.2.le 2) 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
⊢ 1 / 2 * log ((1 + x) / (1 - x)) ≤
    ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
have h₁ : |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
  |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: have h₁ := sum_range_sub_log_div_le (by rwa [abs_of_nonneg h₀]) n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
h₁ :
  |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ 1 / 2 * log ((1 + x) / (1 - x)) ≤
    ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
have rwa : ∀
  (h₁ :
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤
      |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)),
  1 / 2 * log ((1 + x) / (1 - x)) ≤
    ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: rwa [abs_of_nonneg (sub_nonneg_of_le (sum_range_le_log_div h₀ h n)), abs_of_nonneg h₀,
    sub_le_iff_le_add'] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
h₁ :
  |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
rwa :
  ∀
    (h₁ :
      1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤
        |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)),
    1 / 2 * log ((1 + x) / (1 - x)) ≤
      ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
        x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ 1 / 2 * log ((1 + x) / (1 - x)) ≤
    ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
have rwa₁ : ∀
  (h₁ :
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)),
  1 / 2 * log ((1 + x) / (1 - x)) ≤
    ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: rwa [abs_of_nonneg (sub_nonneg_of_le (sum_range_le_log_div h₀ h n)), abs_of_nonneg h₀,
    sub_le_iff_le_add'] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
h₁ :
  |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
rwa :
  ∀
    (h₁ :
      1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤
        |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)),
    1 / 2 * log ((1 + x) / (1 - x)) ≤
      ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
        x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
rwa₁ :
  ∀
    (h₁ :
      1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤
        x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)),
    1 / 2 * log ((1 + x) / (1 - x)) ≤
      ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
        x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ 1 / 2 * log ((1 + x) / (1 - x)) ≤
    ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
have rwa₂ : ∀
  (h₁ :
    1 / 2 * log ((1 + x) / (1 - x)) ≤
      ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
        x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)),
  1 / 2 * log ((1 + x) / (1 - x)) ≤
    ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) +
      x ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)
Tactic: rwa [abs_of_nonneg (sub_nonneg_of_le (sum_range_le_log_div h₀ h n)), abs_of_nonneg h₀,
    sub_le_iff_le_add'] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ HasSum (fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (-log (1 - x))
have rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop (𝓝 (-log (1 - x)))
Tactic: rw [Summable.hasSum_iff_tendsto_nat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop (𝓝 (-log (1 - x)))
⊢ HasSum (fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (-log (1 - x))
have rw₁ : Summable (α := ℝ) fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [Summable.hasSum_iff_tendsto_nat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop (𝓝 (-log (1 - x)))
have rw : Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - -log (1 - x)‖)
  atTop (𝓝 0)
Tactic: rw [tendsto_iff_norm_sub_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - -log (1 - x)‖)
    atTop (𝓝 0)
have simp : Tendsto (β := ℝ) (fun (e : ℕ) ↦ |∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)|) atTop
  (𝓝 0)
Tactic: simp only [norm_eq_abs, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ |∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)|)
    atTop (𝓝 0)
have refine : Tendsto (β := ℝ) (fun (t : ℕ) ↦ |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)
Tactic: refine squeeze_zero (fun n => abs_nonneg _) (abs_log_sub_add_sum_range_le h) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (β := ℝ) (fun (t : ℕ) ↦ |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)
have suffices : Tendsto (fun (t : ℕ) ↦ |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
Tactic: suffices Tendsto (fun t : ℕ => |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|))) by
      simpa
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun (t : ℕ) ↦ |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
have simp : Tendsto (fun (t : ℕ) ↦ |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
Tactic: simp only [pow_succ']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun (t : ℕ) ↦ |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
have refine : Tendsto (α := ℕ) (HPow.hPow |x|) atTop (𝓝 0)
Tactic: refine (tendsto_const_nhds.mul ?_).div_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have refine : ∀ (i : ℕ), ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ ≤ |x| ^ i
Tactic: refine .of_norm_bounded (summable_geometric_of_lt_one (abs_nonneg _) h) fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have this : 0 ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have rw : |x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
rw : |x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have rw₁ : |x ^ (i + 1)| / |HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
rw : |x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
rw₁ : |x ^ (i + 1)| / |HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have rw₂ : |x| ^ (i + 1) / |HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
this : 0 ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
rw : |x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
rw₁ : |x ^ (i + 1)| / |HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
rw₂ : |x| ^ (i + 1) / |HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have rw₃ : |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) 0 1
have hdb : LE.le (α := ℝ) 0 (↑i : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ ≤ |x| ^ i
have have : ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
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
      positivity
    _ ≤ |x| ^ i := by
      simpa [pow_succ] using mul_le_of_le_one_right (by positivity) h.le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
have : ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ ≤ |x| ^ i
have have₁ : |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) 0 1
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
      positivity
    _ ≤ |x| ^ i := by
      simpa [pow_succ] using mul_le_of_le_one_right (by positivity) h.le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
i : ℕ
have : ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ = |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have₁ : |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) 0 1
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ ≤ |x| ^ i
have have₂ : |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) 0 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
      positivity
    _ ≤ |x| ^ i := by
      simpa [pow_succ] using mul_le_of_le_one_right (by positivity) h.le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
have h₁ : ∀ (n : ℕ), (term ∘ fun (x : ℕ) ↦ 2 * x) n = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
n : ℕ
⊢ (term ∘ fun (x : ℕ) ↦ 2 * x) n = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
have h₁ : -1 * ((-x) ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1) +
    x ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 =
  2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
Tactic: dsimp only [term, (· ∘ ·)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
n : ℕ
⊢ -1 * ((-x) ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1) +
      x ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 =
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
have h₁ : -1 * (-x ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1) + x ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 =
  2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
Tactic: rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1) +
      x ^ (2 * n + 1) / HAdd.hAdd (α := ℝ) (↑(2 * n) : ℝ) 1 =
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
have h₁ : -1 * (-x ^ (2 * n + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) + x ^ (2 * n + 1) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) =
  2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
have h_term_eq_goal : Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
  2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
Tactic: have h_term_eq_goal :
      term ∘ (2 * ·) = fun k : ℕ => 2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1) := by
    ext n
    dsimp only [term, (· ∘ ·)]
    rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]
    push_cast
    ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
term : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦ -1 * ((-x) ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) + x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h_term_eq_goal :
  Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
have rw : HasSum term (log (1 + x) - log (1 - x))
Tactic: rw [← h_term_eq_goal, (mul_right_injective₀ (two_ne_zero' ℕ)).hasSum_iff]