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

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : m ∉ Set.range fun x => 2 * x
⊢ term m = 0

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

Result:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ term m = 0

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
⊢ (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)

Tactic:
ext n

Result:
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ (term ∘ fun x => 2 * x) n = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Proof state:
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Tactic:
push_cast

Result:
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (2 * ↑n + 1)) + x ^ (2 * n + 1) / (2 * ↑n + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ term m = 0

Tactic:
dsimp [term]

Result:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ -1 * ((-x) ^ (m + 1) / (↑m + 1)) + x ^ (m + 1) / (↑m + 1) = 0

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : Even (m + 1)
⊢ -1 * ((-x) ^ (m + 1) / (↑m + 1)) + x ^ (m + 1) / (↑m + 1) = 0

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

Result:
no goals

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ x ∉ Set.range fun x => 2 * x, term x = 0

Tactic:
intro m hm

Result:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
m : ℕ
hm : m ∉ Set.range fun x => 2 * x
⊢ term m = 0

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

Tactic:
set term := fun n : ℕ => -1 * ((-x) ^ (n + 1) / ((n : ℝ) + 1)) + x ^ (n + 1) / (n + 1)

Result:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))

Proof state:
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * ((-x) ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) =
    2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Tactic:
rw [Odd.neg_pow (⟨n, rfl⟩ : Odd (2 * n + 1)) x]

Result:
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (↑(2 * n) + 1)) + x ^ (2 * n + 1) / (↑(2 * n) + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Proof state:
case h.e'_6
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -log (1 - -x))
⊢ log (1 + x) - log (1 - x) = -1 * -log (1 - -x) + -log (1 - x)

Tactic:
ring_nf

Result:
no goals

Proof state:
case h
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
n : ℕ
⊢ -1 * (-x ^ (2 * n + 1) / (2 * ↑n + 1)) + x ^ (2 * n + 1) / (2 * ↑n + 1) = 2 * (1 / (2 * ↑n + 1)) * x ^ (2 * n + 1)

Tactic:
ring_nf

Result:
no goals

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -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

Result:
case h.e'_6
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -log (1 - -x))
⊢ log (1 + x) - log (1 - x) = -1 * -log (1 - -x) + -log (1 - x)

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum (fun k => 2 * (1 / (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]

Result:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))

x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ ∀ x ∉ Set.range fun x => 2 * x, term x = 0

Proof state:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
⊢ HasSum term (log (1 + x) - log (1 - x))

Tactic:
have h₁ := (hasSum_pow_div_log_of_abs_lt_one (Eq.trans_lt (abs_neg x) h)).mul_left (-1)

Result:
x : ℝ
h : |x| < 1
term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)
h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)
h₁ : HasSum (fun i => -1 * ((-x) ^ (i + 1) / (↑i + 1))) (-1 * -log (1 - -x))
⊢ HasSum term (log (1 + x) - log (1 - x))