case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
⊢ HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
convert hasSum_log_sub_log_of_abs_lt_1 h₁ using 1
case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (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))
case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
⊢ log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
have h₂ : (2 : ℝ) * a + 1 ≠ 0 := by linarith
case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (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))
case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (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))
have h₃ := h.ne'
case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (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₁ : abs (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₁ : abs (1 / (2 * a + 1)) < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0
case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (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))
rw [← log_div]
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)
a : ℝ
h : 0 < a
⊢ abs (1 / (2 * a + 1)) < 1
rw [abs_of_pos, div_lt_one]
no goals
a : ℝ
h : 0 < a
⊢ 1 < 2 * a + 1
linarith
no goals
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1
linarith
no goals
a : ℝ
h : 0 < a
⊢ 0 < 1 / (2 * a + 1)
exact div_pos one_pos (by linarith)
no goals
a : ℝ
h : 0 < a
⊢ 0 < 2 * a + 1
linarith
no goals
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
⊢ 2 * a + 1 ≠ 0
linarith
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : abs (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))
case h.e'_6
a : ℝ
h : 0 < a
h₁ : abs (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)))
congr
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (a + 1) * (2 * a) = (2 * a + 1 + 1) * a
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : abs (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))
field_simp
no goals
case h.e'_6.e_x
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ (a + 1) * (2 * a) = (2 * a + 1 + 1) * a
linarith
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ ¬2 * a + 1 + 1 = 0
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0
field_simp
no goals
case h.e'_6.hx
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ ¬2 * a + 1 + 1 = 0
linarith
no goals
case h.e'_6.hy
a : ℝ
h : 0 < a
h₁ : abs (1 / (2 * a + 1)) < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0
field_simp