-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem hasSum_log_one_add_inv {a : ℝ} (h : 0 < a) :
    HasSum (fun k : ℕ => (2 : ℝ) * (1 / (2 * k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1))
      (log (1 + a⁻¹))

Proof state:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))

Tactic:
rw [← log_div]

Result:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))

case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0

case h.e'_6.hy
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0

Proof state:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ HasSum (fun k => 2 * (1 / (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

Result:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))

Proof state:
case h.e'_6.hy
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:
field_simp

Result:
no goals

Proof state:
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1

Tactic:
linarith

Result:
no goals

Proof state:
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ 2 * a + 1 ≠ 0

Tactic:
linarith

Result:
no goals

Proof state:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))

Tactic:
congr

Result:
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))

Proof state:
a : ℝ
h : 0 < a
⊢ |1 / (2 * a + 1)| < 1

Tactic:
rw [abs_of_pos, div_lt_one]

Result:
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1

a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1

a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)

Proof state:
case h.e'_6.hx
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:
field_simp

Result:
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ ¬2 * a + 1 + 1 = 0

Proof state:
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (a + 1) * (2 * a) = (2 * a + 1 + 1) * a

Tactic:
linarith

Result:
no goals

Proof state:
a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)

Tactic:
exact div_pos one_pos (by linarith)

Result:
no goals

Proof state:
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1

Tactic:
linarith

Result:
no goals

Proof state:
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + a⁻¹ = (1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1))

Tactic:
field_simp

Result:
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (a + 1) * (2 * a) = (2 * a + 1 + 1) * a

Proof state:
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ ¬2 * a + 1 + 1 = 0

Tactic:
linarith

Result:
no goals

Proof state:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))

Tactic:
have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith

Result:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))

Proof state:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))

Tactic:
have h₃ := h.ne'

Result:
case h.e'_6
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))