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 : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
i : ℕ
e_a : y ^ i = HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ y ^ i = (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
have e_a₁ : y ^ i = y ^ i
Tactic: rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
⊢ F' y = ∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)
have n₁ : -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y)
Tactic: calc
      -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) := by
        simp [field, geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
        ring
      _ = ∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) := by
        congr with i
        rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
this : HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y
n₁ : -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y)
⊢ F' y = ∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)
have n₂ : ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) =
  ∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)
Tactic: calc
      -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) := by
        simp [field, geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
        ring
      _ = ∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) := by
        congr with i
        rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
have A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
Tactic: have A : ∀ y ∈ Ioo (-1 : ℝ) 1, HasDerivAt F (F' y) y := fun y hy ↦ by
    have : HasDerivAt F ((∑ i ∈ range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
      .add (.fun_sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
        (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
    convert! this using 1
    calc
      -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) := by
        simp [field, geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
        ring
      _ = ∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) := by
        congr with i
        rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
have this : |y| ≤ |x|
Tactic: have : |y| ≤ |x| := abs_le.2 hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : |y| ≤ |x|
⊢ 1 - |x| ≤ 1 - y
have linarith : 1 - y < 1 - |x| → 1 - y - (1 - |x|) + (y - |x|) = 0
Tactic: linarith [hy.2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : |y| ≤ |x|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
have this₁ : 1 - |x| ≤ |1 - y|
Tactic: have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this_1 : |y| ≤ |x|
this : 1 - |x| ≤ |1 - y|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
have hc : 0 ≤ |x| ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this_1 : |y| ≤ |x|
this : 1 - |x| ≤ |1 - y|
hc : 0 ≤ |x| ^ n
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
have hd : 0 < 1 - |x|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this_1 : |y| ≤ |x|
this : 1 - |x| ≤ |1 - y|
hc : 0 ≤ |x| ^ n
hd : 0 < 1 - |x|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)
have hac : 0 ≤ |y|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
have B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
Tactic: have B : ∀ y ∈ Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|) := fun y hy ↦
    calc
      |F' y| = |y| ^ n / |1 - y| := by simp [F', abs_div]
      _ ≤ |x| ^ n / (1 - |x|) := by
        have : |y| ≤ |x| := abs_le.2 hy
        have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
        gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
have refine_1 : ∀ (y : ℝ) (hy : y ∈ Set.Icc (-|x|) |x|), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
Tactic: refine Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
refine_1 : ∀ (y : ℝ) (hy : y ∈ Set.Icc (-|x|) |x|), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
⊢ ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
have refine_2 : 0 ∈ Set.Icc (-|x|) |x|
Tactic: refine Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
refine_1 : ∀ (y : ℝ) (hy : y ∈ Set.Icc (-|x|) |x|), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
refine_2 : 0 ∈ Set.Icc (-|x|) |x|
⊢ ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
have refine_3 : x ∈ Set.Icc (-|x|) |x|
Tactic: refine Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun (x : ℝ) ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)
F' : ℝ → ℝ := fun (x : ℝ) ↦ -x ^ n / (1 - x)
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
Tactic: have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖ := by
    refine Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
    · exact Icc_subset_Ioo (neg_lt_neg h) h hy
    · simp
    · simp [le_abs_self x, neg_le.mp (neg_le_abs x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ HasDerivAt
    (fun (x : ℝ) ↦
      1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)) y
have refine_1 : HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y ≠ 0
Tactic: refine ((((((hasDerivAt_id _).const_add _).div ((hasDerivAt_id _).const_sub _) (by grind)).log
          ?_).const_mul _).sub (HasDerivAt.fun_sum fun i hi ↦ (hasDerivAt_pow _ _).div_const _))
        |>.congr_deriv ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
refine_1 : HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y ≠ 0
⊢ HasDerivAt
    (fun (x : ℝ) ↦
      1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)) y
have refine_2 : 1 / 2 *
      ((1 * (1 - y) - (1 + y) * -1) / HPow.hPow (β := ℕ) (1 - y) 2 /
        HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y) -
    ∑ i ∈ Finset.range n, (↑(2 * i + 1) : ℝ) * y ^ (2 * i + 1 - 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) =
  HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
Tactic: refine ((((((hasDerivAt_id _).const_add _).div ((hasDerivAt_id _).const_sub _) (by grind)).log
          ?_).const_mul _).sub (HasDerivAt.fun_sum fun i hi ↦ (hasDerivAt_pow _ _).div_const _))
        |>.congr_deriv ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y ≠ 0
have refine_1 : 1 + y ≠ 0 ∧ 1 - y ≠ 0
Tactic: simp only [id_eq, div_ne_zero_iff, Pi.div_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ Eq (α := ℝ)
    (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
have e_f : ∀ (i : ℕ),
  (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) = HPow.hPow (β := ℕ) y 2 ^ i
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 / 2 *
        ((1 * (1 - y) - (1 + y) * -1) / HPow.hPow (β := ℕ) (1 - y) 2 /
          HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y) -
      ∑ i ∈ Finset.range n, (↑(2 * i + 1) : ℝ) * y ^ (2 * i + 1 - 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) =
    HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
have this : Eq (α := ℝ)
  (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
  (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
Tactic: have : (∑ i ∈ range n, (2 * i + 1) * y ^ (2 * i) / (2 * i + 1)) =
      (∑ i ∈ range n, (y ^ 2) ^ i) := by
    congr with i
    simp [field, mul_comm, ← pow_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
⊢ 1 / 2 *
        ((1 * (1 - y) - (1 + y) * -1) / HPow.hPow (β := ℕ) (1 - y) 2 /
          HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y) -
      ∑ i ∈ Finset.range n, (↑(2 * i + 1) : ℝ) * y ^ (2 * i + 1 - 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) =
    HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
have hy₃ : HPow.hPow (β := ℕ) y 2 ≠ 1
Tactic: have hy₃ : y ^ 2 ≠ 1 := by simp [hy₁.ne', hy₂.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (hypothesis)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
hy₃ : HPow.hPow (β := ℕ) y 2 ≠ 1
⊢ 1 / 2 *
        ((1 * (1 - y) - (1 + y) * -1) / HPow.hPow (β := ℕ) (1 - y) 2 /
          HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y) -
      ∑ i ∈ Finset.range n, (↑(2 * i + 1) : ℝ) * y ^ (2 * i + 1 - 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) =
    HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
have hy₄ : (1 - y) * (1 + y) = 1 - HPow.hPow (β := ℕ) y 2
Tactic: have hy₄ : (1 - y) * (1 + y) = 1 - y ^ 2 := by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Deriv (goal)
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
hy₃ : HPow.hPow (β := ℕ) y 2 ≠ 1
hy₄ : (1 - y) * (1 + y) = 1 - HPow.hPow (β := ℕ) y 2
⊢ 1 / 2 *
        ((1 * (1 - y) - (1 + y) * -1) / HPow.hPow (β := ℕ) (1 - y) 2 /
          HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y) -
      ∑ i ∈ Finset.range n, (↑(2 * i + 1) : ℝ) * y ^ (2 * i + 1 - 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) =
    HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
have refine_2 : (1 - y - (-y + -1)) * (HPow.hPow (β := ℕ) y 2 - 1) -
    (1 - HPow.hPow (β := ℕ) y 2) * 2 * (HPow.hPow (β := ℕ) y 2 ^ n - 1) =
  (HPow.hPow (β := ℕ) y 2 - 1) * 2 * HPow.hPow (β := ℕ) y 2 ^ n
Tactic: simp [this, field, geom_sum_eq hy₃, hy₄, sub_ne_zero_of_ne, hy₃.symm]
-- 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)
⊢ |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 hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
Tactic: have hI : Icc (-|x|) |x| ⊆ Ioo (-1 : ℝ) 1 := Icc_subset_Ioo (by simp [h]) h
-- 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
⊢ |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 A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
Tactic: have A : ∀ y ∈ Ioo (-1 : ℝ) 1, 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 (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
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
have this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
Tactic: have : y ^ 2 ≤ x ^ 2 := sq_le_sq.2 (abs_le.2 hy)
-- 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
⊢ HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2| = HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
have rw : HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2) = HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
Tactic: rw [abs_of_pos (by simpa [abs_lt] using hI hy)]
-- 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
⊢ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2) ≤ HPow.hPow (β := ℕ) x 2 ^ n / (1 - HPow.hPow (β := ℕ) x 2)
have hd : 0 < 1 - HPow.hPow (β := ℕ) x 2
Tactic: gcongr ?_ ^ n / (1 - ?_)
-- 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
⊢ ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
have n₁ : ‖F' y‖ = HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 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 (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|
⊢ ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
have n₂ : HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2| = HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 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 (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)
⊢ ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
have n₃ : HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2) ≤ HPow.hPow (β := ℕ) 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]