awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
f : ℝ → ℝ
x : ℝ
h₁ : DifferentiableAt ℝ f x
h₂ : f x ≠ 0
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
simp only [logDeriv, Pi.div_apply, ← deriv.log h₁ h₂, Function.comp_def]

Premises used: logDeriv, deriv.log, Pi.div_apply, Function.comp_def
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
f' : StrongDual ℝ E
s : Set E
hf : HasFDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ Real.log (f x)) ((f x)⁻¹ • f') s x

Tactic:
(hasDerivAt_log hx).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Real.log, dite, Real.hasDerivAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
f' : StrongDual ℝ E
hf : HasFDerivAt f f' x
hx : f x ≠ 0
⊢ HasFDerivAt (fun (x : E) ↦ Real.log (f x)) ((f x)⁻¹ • f') x

Tactic:
(hasDerivAt_log hx).comp_hasFDerivAt x hf

Premises used: Real.log, dite, Real.hasDerivAt_log, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
f' : StrongDual ℝ E
hf : HasStrictFDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictFDerivAt (fun (x : E) ↦ Real.log (f x)) ((f x)⁻¹ • f') x

Tactic:
(hasStrictDerivAt_log hx).comp_hasStrictFDerivAt x hf

Premises used: Real.hasStrictDerivAt_log, Real.log, dite, HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
hx : f x ≠ 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ Real.log (f x)) s x

Tactic:
(hf.hasFDerivWithinAt.log hx).differentiableWithinAt

Premises used: HasFDerivWithinAt.log, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
hx : f x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ Real.log (f x)) x

Tactic:
(hf.hasFDerivAt.log hx).differentiableAt

Premises used: HasFDerivAt.log, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
n : ℕ∞ω
hf : ContDiffAt ℝ n f x
hx : f x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ Real.log (f x)) x

Tactic:
(contDiffAt_log.2 hx).comp x hf

Premises used: Iff.mpr, Real.contDiffAt_log, Real.log, dite, ContDiffAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
n : ℕ∞ω
hf : ContDiffWithinAt ℝ n f s x
hx : f x ≠ 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x : E) ↦ Real.log (f x)) s x

Tactic:
(contDiffAt_log.2 hx).comp_contDiffWithinAt x hf

Premises used: Iff.mpr, Real.contDiffAt_log, Real.log, dite, ContDiffAt.comp_contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
n : ℕ∞ω
hf : ContDiffOn ℝ n f s
hs : ∀ x ∈ s, f x ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) n (fun (x : E) ↦ Real.log (f x)) s

Tactic:
fun x hx => (hf x hx).log (hs x hx)

Premises used: ContDiffOn, ContDiffWithinAt.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : ℕ∞ω
hf : ContDiff ℝ n f
h : ∀ (x : E), f x ≠ 0
⊢ ContDiff ℝ (F := ℝ) n fun (x : E) ↦ Real.log (f x)

Tactic:
contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.log (h x)

Premises used: Iff.mpr, ContDiffAt.log, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
hf : DifferentiableOn ℝ f s
hx : ∀ x ∈ s, f x ≠ 0
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : E) ↦ Real.log (f x)) s

Tactic:
fun x h => (hf x h).log (hx x h)

Premises used: DifferentiableWithinAt.log, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hf : Differentiable ℝ f
hx : ∀ (x : E), f x ≠ 0
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ Real.log (f x)

Tactic:
fun x => (hf x).log (hx x)

Premises used: Differentiable, DifferentiableAt.log
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
hx : f x ≠ 0
hxs : UniqueDiffWithinAt ℝ s x
⊢ fderivWithin ℝ (fun (x : E) ↦ Real.log (f x)) s x = HSMul.hSMul (β := E →L[ℝ] ℝ) (f x)⁻¹ (fderivWithin ℝ f s x)

Tactic:
(hf.hasFDerivWithinAt.log hx).fderivWithin hxs

Premises used: HasFDerivWithinAt.log, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
hx : f x ≠ 0
⊢ fderiv ℝ (fun (x : E) ↦ Real.log (f x)) x = HSMul.hSMul (β := E →L[ℝ] ℝ) (f x)⁻¹ (fderiv ℝ f x)

Tactic:
(hf.hasFDerivAt.log hx).fderiv

Premises used: HasFDerivAt.log, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
⊢ HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y

Tactic:
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')
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
⊢ HasDerivAt F (∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)) y

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
h₁ : F' y = ∑ i ∈ Finset.range n, (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + -1 / (1 - y)
⊢ HasDerivAt F (F' y) y

Tactic:
convert! this using 1
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
simp : -(y ^ n * (y - 1)) = y ^ n * (1 - y)
⊢ -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y)

Tactic:
simp [field, geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']

Premises used: Iff.mpr, sub_ne_zero, geom_sum_eq, LT.lt.ne', And.right, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
⊢ -(y ^ n * (y - 1)) = y ^ n * (1 - y)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
e_a : ∀ (i : ℕ), y ^ i = (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ ∑ 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:
congr with i
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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
e_a₁ e_a₂ : y ^ i = y ^ i
⊢ y ^ i = (↑(i + 1) : ℝ) * y ^ i / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']

Premises used: Nat.cast_succ, mul_div_cancel_left₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
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)
⊢ F' 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']

Premises used: HSub.hSub, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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 : ℝ), 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']
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|
⊢ |F' y| = |y| ^ n / |1 - y|

Tactic:
simp [F', abs_div]

Premises used: abs_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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| ≤ |x|

Tactic:
have : |y| ≤ |x| := abs_le.2 hy
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|
linarith : 1 - y < 1 - |x| → 1 - y - (1 - |x|) + (y - |x|) = 0
⊢ 1 - |x| ≤ 1 - y

Tactic:
linarith [hy.2]

Premises used: And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|

Tactic:
have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|
hac : 0 ≤ |y|
⊢ |y| ^ n / |1 - y| ≤ |x| ^ n / (1 - |x|)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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 ∈ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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‖

Tactic:
Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_

Premises used: HasDerivAt.hasDerivWithinAt, Convex.norm_image_sub_le_of_norm_hasDerivWithin_le, convex_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|
refine_3 : x ∈ Set.Icc (-|x|) |x|
⊢ ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖

Tactic:
refine Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_

Premises used: HasDerivAt.hasDerivWithinAt, Convex.norm_image_sub_le_of_norm_hasDerivWithin_le, convex_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|)
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y

Tactic:
Icc_subset_Ioo (neg_lt_neg h) h hy

Premises used: Set.Mem, neg_lt_neg, Set.Icc_subset_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|)
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y

Tactic:
exact Icc_subset_Ioo (neg_lt_neg h) h hy

Premises used: neg_lt_neg, Set.Icc_subset_Ioo
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|)
⊢ 0 ∈ Set.Icc (-|x|) |x|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|)
⊢ x ∈ Set.Icc (-|x|) |x|

Tactic:
simp [le_abs_self x, neg_le.mp (neg_le_abs x)]

Premises used: neg_le, le_abs_self, neg_le_abs, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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‖

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)]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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|)
C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)

Tactic:
simpa [F, div_mul_eq_mul_div, pow_succ] using C

Premises used: pow_succ, div_mul_eq_mul_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 - y ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
refine_1 : HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y ≠ 0
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)
⊢ 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

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 ?_

Premises used: HasDerivAt.log, HasDerivAt.sub, HasDerivAt.fun_sum, HasDerivAt.const_mul, HasDerivAt.div_const, HasDerivAt.div, HasDerivAt.congr_deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
refine_1 : 1 + y ≠ 0 ∧ 1 - y ≠ 0
⊢ HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y ≠ 0

Tactic:
simp only [id_eq, div_ne_zero_iff, Pi.div_apply]

Premises used: div_ne_zero_iff, Pi.div_apply, id_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 + y ≠ 0 ∧ 1 - y ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
e_f :
  ∀ (i : ℕ),
    (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) = HPow.hPow (β := ℕ) y 2 ^ i
⊢ 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:
congr with i
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
i : ℕ
⊢ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) = HPow.hPow (β := ℕ) y 2 ^ i

Tactic:
simp [field, mul_comm, ← pow_mul]

Premises used: pow_mul, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
⊢ HPow.hPow (β := ℕ) y 2 ≠ 1

Tactic:
simp [hy₁.ne', hy₂.ne]

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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)
⊢ HPow.hPow (β := ℕ) y 2 ≠ 1

Tactic:
have hy₃ : y ^ 2 ≠ 1 := by simp [hy₁.ne', hy₂.ne]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
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 - y) * (1 + y) = 1 - HPow.hPow (β := ℕ) y 2

Tactic:
ring