awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
rwa₂ rwa₃ rwa₄ 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)

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₁

Premises used: sub_nonneg_of_le, Real.sum_range_le_log_div, sub_le_iff_le_add', abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop (𝓝 (-log (1 - x)))
rw₁ : Summable (α := ℝ) fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ HasSum (fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (-log (1 - x))

Tactic:
rw [Summable.hasSum_iff_tendsto_nat]

Premises used: Summable.hasSum_iff_tendsto_nat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
rw :
  Tendsto (β := ℝ) (fun (e : ℕ) ↦ ‖∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - -log (1 - x)‖)
    atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) atTop (𝓝 (-log (1 - x)))

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]

Premises used: tendsto_iff_norm_sub_tendsto_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
simp :
  Tendsto (β := ℝ) (fun (e : ℕ) ↦ |∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)|)
    atTop (𝓝 0)
⊢ 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]

Premises used: sub_neg_eq_add, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ |∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)|)
    atTop (𝓝 0)

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

Premises used: squeeze_zero, HSub.hSub, HDiv.hDiv, Real.abs_log_sub_add_sum_range_le, Nat.cast, Real.log, Finset.range, HPow.hPow, HAdd.hAdd, OfNat.ofNat, abs_nonneg, Finset.sum
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
refine : Tendsto (β := ℝ) (fun (t : ℕ) ↦ |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (e : ℕ) ↦ |∑ i ∈ Finset.range e, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)|)
    atTop (𝓝 0)

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

Premises used: squeeze_zero, Real.abs_log_sub_add_sum_range_le, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
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
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
suffices : Tendsto (fun (t : ℕ) ↦ |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
simp : Tendsto (fun (t : ℕ) ↦ |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))
⊢ Tendsto (fun (t : ℕ) ↦ |x| ^ (t + 1) / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))

Tactic:
simp only [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun (t : ℕ) ↦ |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))

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

Premises used: tendsto_const_nhds, Filter.Tendsto.div_const, Filter.Tendsto.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
refine : Tendsto (α := ℕ) (HPow.hPow |x|) atTop (𝓝 0)
⊢ Tendsto (fun (t : ℕ) ↦ |x| * |x| ^ t / (1 - |x|)) atTop (𝓝 (|x| * 0 / (1 - |x|)))

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

Premises used: tendsto_const_nhds, Filter.Tendsto.div_const, Filter.Tendsto.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (α := ℕ) (HPow.hPow |x|) atTop (𝓝 0)

Tactic:
tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg _) h

Premises used: tendsto_pow_atTop_nhds_zero_of_lt_one, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
⊢ Tendsto (α := ℕ) (HPow.hPow |x|) atTop (𝓝 0)

Tactic:
exact tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg _) h

Premises used: tendsto_pow_atTop_nhds_zero_of_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

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

Premises used: Summable.of_norm_bounded, summable_geometric_of_lt_one, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
refine : ∀ (i : ℕ), ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1‖ ≤ |x| ^ i
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
refine .of_norm_bounded (summable_geometric_of_lt_one (abs_nonneg _) h) fun i => ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
i : ℕ
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
rw₃ 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

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

Premises used: abs_div, pow_abs, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
i : ℕ
hdb : LE.le (α := ℝ) 0 (↑i : ℝ)
⊢ |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ≤ |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) 0 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
i : ℕ
⊢ LE.le (α := ℝ) 0 (↑i : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
i : ℕ
⊢ 0 ≤ |x| ^ i

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
i : ℕ
⊢ |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) 0 1 ≤ |x| ^ i

Tactic:
simpa [pow_succ] using mul_le_of_le_one_right (by positivity) h.le

Premises used: pow_succ, mul_le_of_le_one_right, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
have₂ : |x| ^ (i + 1) / HAdd.hAdd (α := ℝ) 0 1 ≤ |x| ^ i
⊢ ‖x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑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
      positivity
    _ ≤ |x| ^ i := by
      simpa [pow_succ] using mul_le_of_le_one_right (by positivity) h.le

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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₁ : ∀ (n : ℕ), (term ∘ fun (x : ℕ) ↦ 2 * x) n = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)
⊢ Eq (α := ℕ → ℝ) (term ∘ fun (x : ℕ) ↦ 2 * x) fun (k : ℕ) ↦
    2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)

Tactic:
ext n
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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 : ℕ
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)
⊢ (term ∘ fun (x : ℕ) ↦ 2 * x) n = 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) * x ^ (2 * n + 1)

Tactic:
dsimp only [term, (· ∘ ·)]

Premises used: Function.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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 : ℕ
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)
⊢ -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]

Premises used: Odd.neg_pow, Exists.intro, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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 : ℕ
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)
⊢ -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:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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) / (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:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)

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
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
rw : HasSum term (log (1 + x) - log (1 - x))
rw₁ : ∀ x ∉ Set.range fun (x : ℕ) ↦ 2 * x, term x = 0
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))

Tactic:
rw [← h_term_eq_goal, (mul_right_injective₀ (two_ne_zero' ℕ)).hasSum_iff]

Premises used: mul_right_injective₀, two_ne_zero', Nat, Function.Injective.hasSum_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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 (i : ℕ) ↦ -1 * ((-x) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) (-1 * -log (1 - -x))

Tactic:
have h₁ := (hasSum_pow_div_log_of_abs_lt_one (Eq.trans_lt (abs_neg x) h)).mul_left (-1)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
h₁ : HasSum (fun (i : ℕ) ↦ -1 * ((-x) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) (-1 * -log (1 - -x))
⊢ HasSum
    (fun (b : ℕ) ↦ -1 * ((-x) ^ (b + 1) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1) + x ^ (b + 1) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1)
    (-1 * -log (1 - -x) + -log (1 - x))

Tactic:
h₁.add (hasSum_pow_div_log_of_abs_lt_one h)

Premises used: HasSum.add, Real.hasSum_pow_div_log_of_abs_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
h₁ : HasSum (fun (i : ℕ) ↦ -1 * ((-x) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) (-1 * -log (1 - -x))
h₂ : log (1 + x) - log (1 - x) = -1 * -log (1 - -x) + -log (1 - x)
⊢ HasSum term (log (1 + x) - log (1 - x))

Tactic:
convert! h₁.add (hasSum_pow_div_log_of_abs_lt_one h) using 1

Premises used: HasSum.add, Real.hasSum_pow_div_log_of_abs_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
h₁ : HasSum (fun (i : ℕ) ↦ -1 * ((-x) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) (-1 * -log (1 - -x))
⊢ log (1 + x) - log (1 - x) = -1 * -log (1 - -x) + -log (1 - x)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
m : ℕ
hm : m ∉ Set.range fun (x : ℕ) ↦ 2 * x
⊢ Even (m + 1)

Tactic:
rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm

Premises used: Nat.even_add_one, Set.mem_setOf_eq, range_two_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
m : ℕ
hm : Even (m + 1)
dsimp : -1 * ((-x) ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
⊢ term m = 0

Tactic:
dsimp [term]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
m : ℕ
hm : Even (m + 1)
rw : -1 * (x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
rw₁ : -(x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ -1 * ((-x) ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + x ^ (m + 1) / HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 = 0

Tactic:
rw [Even.neg_pow hm, neg_one_mul, neg_add_cancel]

Premises used: Even.neg_pow, neg_one_mul, neg_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
rw : 1 < 2 * a + 1
rw₁ : 0 < 2 * a + 1
rw₂ : 0 < 1 / (2 * a + 1)
⊢ |1 / (2 * a + 1)| < 1

Tactic:
rw [abs_of_pos, div_lt_one]

Premises used: div_lt_one, abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
linarith : 2 * a + 1 ≤ 1 → 2 * (0 - a) + (2 * a + 1 - 1) = 0
linarith₁ : 2 * a + 1 ≤ 1 → GT.gt (α := ℝ) 2 0
⊢ 1 < 2 * a + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
linarith : 2 * a + 1 ≤ 0 → -1 + 2 * (0 - a) + (2 * a + 1 - 0) = 0
linarith₁ : 2 * a + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 2 * a + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)

Tactic:
exact div_pos one_pos (by linarith)

Premises used: div_pos, one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
⊢ |1 / (2 * a + 1)| < 1

Tactic:
have h₁ : |1 / (2 * a + 1)| < 1 := by
    rw [abs_of_pos, div_lt_one]
    · linarith
    · linarith
    · exact div_pos one_pos (by linarith)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1))
    (log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1)))

Tactic:
hasSum_log_sub_log_of_abs_lt_one h₁

Premises used: Real.hasSum_log_sub_log_of_abs_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))

Tactic:
convert! hasSum_log_sub_log_of_abs_lt_one h₁ using 1

Premises used: Real.hasSum_log_sub_log_of_abs_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
linarith : 2 * a + 1 = 0 → -1 + 2 * (0 - a) + (2 * a + 1 - 0) = 0
linarith₁ : 2 * a + 1 = 0 → GT.gt (α := ℝ) 2 0
⊢ 2 * a + 1 ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ 2 * a + 1 ≠ 0

Tactic:
have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
⊢ a ≠ 0

Tactic:
have h₃ := h.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
h₄ : log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
h₅ : 1 + 1 / (2 * a + 1) ≠ 0
h₆ : 1 - 1 / (2 * a + 1) ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))

Tactic:
rw [← log_div]

Premises used: Real.log_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
h₄ : 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
h₄ : (a + 1) * 2 = a * 2 + 1 + 1
⊢ 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (a + 1) * 2 = a * 2 + 1 + 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
h₄ : (2 * a + 1 + 1) / (2 * a + 1) ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (2 * a + 1 + 1) / (2 * a + 1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0

Tactic:
simp [field, h₃]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 ≤ a
inl :
  ∀ (h : LE.le (α := ℝ) 0 0),
    HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (0 / HAdd.hAdd (α := ℝ) 0 2) ^ (2 * k + 1))
      (log (HAdd.hAdd (α := ℝ) 1 0))
inr :
  ∀ (ha0 : a ≠ 0),
    HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))

Tactic:
obtain (rfl | ha0) := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
h : LE.le (α := ℝ) 0 0
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (0 / HAdd.hAdd (α := ℝ) 0 2) ^ (2 * k + 1))
    (log (HAdd.hAdd (α := ℝ) 1 0))

Tactic:
simp [hasSum_zero]

Premises used: hasSum_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * a⁻¹ + 1)) ^ (2 * k + 1))
    (log (1 + a⁻¹⁻¹))

Tactic:
hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm))

Premises used: Iff.mpr, Real.hasSum_log_one_add_inv, inv_pos, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
h₁ : ∀ (x : ℕ), a / (a + 2) = 1 / (2 * a⁻¹ + 1)
h₂ : a = a⁻¹⁻¹
⊢ HasSum (fun (k : ℕ) ↦ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))

Tactic:
convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4

Premises used: Iff.mpr, Real.hasSum_log_one_add_inv, inv_pos, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
x : ℕ
⊢ a / (a + 2) = 1 / (2 * a⁻¹ + 1)

Tactic:
simp [field, add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ a = a⁻¹⁻¹

Tactic:
simp [field, add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
hx : 0 ≤ x
j : ℕ
h : j ≠ 0
⊢ 0 ≤ 2 * (1 / (HMul.hMul (α := ℝ) 2 (↑j : ℝ) + 1)) * (x / (x + 2)) ^ (2 * j + 1)

Tactic:
positivity