awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
succ :
  HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * (z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
    (HPow.hPow (α := ℂ) (-1) n * z ^ n) z
⊢ HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
    (HPow.hPow (α := ℂ) (-1) n * z ^ n) z

Tactic:
simp only [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (n + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹)
    ((↑(n + 1) : ℂ) * z ^ (n + 1 - 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹) z

Tactic:
HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹)

Premises used: Nat.cast, Inv.inv, HAdd.hAdd, hasDerivAt_pow, OfNat.ofNat, HasDerivAt.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
h : z ^ n = (↑(n + 1) : ℂ) * z ^ (n + 1 - 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹
⊢ HasDerivAt (fun (x : ℂ) ↦ x ^ (n + 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹) (z ^ n) z

Tactic:
convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1

Premises used: Nat.cast, Inv.inv, HAdd.hAdd, hasDerivAt_pow, OfNat.ofNat, HasDerivAt.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ z ^ n = (↑(n + 1) : ℂ) * z ^ (n + 1 - 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt (fun (x : ℂ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) (z ^ n) z

Tactic:
have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z := by
      simp_rw [div_eq_mul_inv]
      convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
      simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
this : HasDerivAt (fun (x : ℂ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) (z ^ n) z
⊢ HasDerivAt (fun (y : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * (y ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
    (HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ n) z

Tactic:
HasDerivAt.const_mul _ this

Premises used: HasDerivAt.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
this : HasDerivAt (fun (x : ℂ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) (z ^ n) z
h : HPow.hPow (α := ℂ) (-1) n = HPow.hPow (α := ℂ) (-1) (n + 1 + 1)
⊢ HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * (z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
    (HPow.hPow (α := ℂ) (-1) n * z ^ n) z

Tactic:
convert! HasDerivAt.const_mul _ this using 2

Premises used: HasDerivAt.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
this : HasDerivAt (fun (x : ℂ) ↦ x ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) (z ^ n) z
⊢ HPow.hPow (α := ℂ) (-1) n = HPow.hPow (α := ℂ) (-1) (n + 1 + 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
zero : HasDerivAt (logTaylor (HAdd.hAdd (α := ℕ) 0 1)) (∑ j ∈ Finset.range 0, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
succ :
  ∀ (n : ℕ) (ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z),
    HasDerivAt (logTaylor (n + 1 + 1)) (∑ j ∈ Finset.range (n + 1), HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z

Tactic:
induction n with
  | zero => simp [logTaylor_succ, logTaylor_zero, Pi.add_def, hasDerivAt_const]
  | succ n ih =>
    rw [logTaylor_succ]
    simp only [Nat.cast_add, Nat.cast_one,
      Finset.sum_range_succ]
    refine HasDerivAt.add ih ?_
    simp only [mul_div_assoc]
    have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z := by
      simp_rw [div_eq_mul_inv]
      convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
      simp [field]
    convert! HasDerivAt.const_mul _ this using 2
    ring

Premises used: mul_div_assoc, hasDerivAt_const, Pi.add_def, Nat.cast_add, Complex.logTaylor_zero, Complex.logTaylor_succ, Nat.cast_one, Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ HasDerivAt ((fun (x : ℂ) ↦ log (1 + x)) - logTaylor (n + 1))
    ((1 + z)⁻¹ - ∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z

Tactic:
((hasDerivAt_log hz).comp_const_add 1 z).sub (hasDerivAt_logTaylor n z)

Premises used: HasDerivAt.sub, Complex.hasDerivAt_logTaylor, HasDerivAt.comp_const_add, OfNat.ofNat, Complex.hasDerivAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
h : (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j
⊢ HasDerivAt (fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z

Tactic:
convert! ((hasDerivAt_log hz).comp_const_add 1 z).sub (hasDerivAt_logTaylor n z) using 1

Premises used: HasDerivAt.sub, Complex.hasDerivAt_logTaylor, HasDerivAt.comp_const_add, OfNat.ofNat, Complex.hasDerivAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : -z = 1
⊢ z = -1

Tactic:
rw [neg_eq_iff_eq_neg] at H

Premises used: neg_eq_iff_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ 0 ∈ slitPlane

Tactic:
simp only [H, add_neg_cancel] at hz

Premises used: add_neg_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
H : z = -1
hz : 0 ∈ slitPlane
⊢ False

Tactic:
slitPlane_ne_zero hz rfl

Premises used: Complex.slitPlane_ne_zero, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
H : z = -1
hz : 0 ∈ slitPlane
⊢ False

Tactic:
exact slitPlane_ne_zero hz rfl

Premises used: Complex.slitPlane_ne_zero, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ -z ≠ 1

Tactic:
have hz' : -z ≠ 1 := by
    intro H
    rw [neg_eq_iff_eq_neg] at H
    simp only [H, add_neg_cancel] at hz
    exact slitPlane_ne_zero hz rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
h : (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (1 + z))
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j

Tactic:
simp_rw [← mul_pow, neg_one_mul, geom_sum_eq hz', ← neg_add', div_neg, add_comm z]

Premises used: neg_one_mul, geom_sum_eq, add_comm, neg_add', div_neg, mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (1 + z))

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
z : ℂ
hz : ‖z‖ < 1
rw : ∀ (ht : 0 ≤ t ∧ t ≤ 1) {z : ℂ} (hz : ‖z‖ < 1), ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
⊢ ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
rw [Set.mem_Icc] at ht

Premises used: Set.mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
rw : ‖1 + (↑t : ℂ) * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹
⊢ ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
rw [norm_inv]

Premises used: norm_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
linarith : 1 - ‖z‖ ≤ 0 → ‖z‖ - 1 + (1 - ‖z‖ - 0) = 0
⊢ 0 < 1 - ‖z‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
refine : 1 - ‖z‖ ≤ ‖1 + (↑t : ℂ) * z‖
⊢ ‖1 + (↑t : ℂ) * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹

Tactic:
refine inv_anti₀ (by linarith) ?_

Premises used: inv_anti₀
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
nlinarith : 1 - t * ‖z‖ < 1 - ‖z‖ → 1 - t * ‖z‖ - (1 - ‖z‖) + (0 - (t - 1) * (0 - ‖z‖)) = 0
⊢ 1 - ‖z‖ ≤ 1 - t * ‖z‖

Tactic:
nlinarith [norm_nonneg z]

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
rw : 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ)‖ * ‖z‖
rw₁ rw₂ : 1 - t * ‖z‖ = 1 - t * ‖z‖
⊢ 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ) * z‖

Tactic:
rw [norm_mul, Complex.norm_of_nonneg ht.1]

Premises used: norm_mul, Complex.norm_of_nonneg, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
rw : 1 - ‖-((↑t : ℂ) * z)‖ ≤ ‖1 - -((↑t : ℂ) * z)‖
⊢ 1 - ‖(↑t : ℂ) * z‖ ≤ ‖1 + (↑t : ℂ) * z‖

Tactic:
rw [← norm_neg (t * z), ← sub_neg_eq_add]

Premises used: HMul.hMul, Complex.ofReal, norm_neg, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ norm (E := ℂ) 1 - ‖-((↑t : ℂ) * z)‖ ≤ ‖1 - -((↑t : ℂ) * z)‖

Tactic:
norm_sub_norm_le 1 (-(t * z))

Premises used: HMul.hMul, Complex.ofReal, norm_sub_norm_le, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
h : 1 = norm (E := ℂ) 1
⊢ 1 - ‖-((↑t : ℂ) * z)‖ ≤ ‖1 - -((↑t : ℂ) * z)‖

Tactic:
convert! norm_sub_norm_le 1 (-(t * z))

Premises used: HMul.hMul, Complex.ofReal, norm_sub_norm_le, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 = norm (E := ℂ) 1

Tactic:
norm_one.symm

Premises used: NormOneClass.norm_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 = norm (E := ℂ) 1

Tactic:
exact norm_one.symm

Premises used: NormOneClass.norm_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
calc : 1 - ‖z‖ ≤ 1 - t * ‖z‖
calc₁ : 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ) * z‖
calc₂ : 1 - ‖(↑t : ℂ) * z‖ ≤ ‖1 + (↑t : ℂ) * z‖
⊢ 1 - ‖z‖ ≤ ‖1 + (↑t : ℂ) * z‖

Tactic:
calc 1 - ‖z‖
    _ ≤ 1 - t * ‖z‖ := by
      nlinarith [norm_nonneg z]
    _ = 1 - ‖t * z‖ := by
      rw [norm_mul, Complex.norm_of_nonneg ht.1]
    _ ≤ ‖1 + t * z‖ := by
      rw [← norm_neg (t * z), ← sub_neg_eq_add]
      convert! norm_sub_norm_le 1 (-(t * z))
      exact norm_one.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.Icc 0 1)

Tactic:
have := continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.Icc 0 1)
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.uIcc 0 1)

Tactic:
rw [← Set.uIcc_of_le zero_le_one] at this

Premises used: Set.uIcc_of_le, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.uIcc 0 1)
funProp : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.uIcc 0 1) x → 1 + (↑x : ℂ) * z ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖) (Set.uIcc 0 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (1 + t • z)⁻¹) (Set.uIcc 0 1)
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖) MeasureTheory.volume 0 1

Tactic:
exact ContinuousOn.intervalIntegrable (by fun_prop)

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ Continuous (Y := ℝ) fun (t : ℝ) ↦ t ^ n

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1

Tactic:
have help : IntervalIntegrable (fun t : ℝ ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1 :=
    IntervalIntegrable.mul_const (Continuous.intervalIntegrable (by fun_prop) 0 1) (1 - ‖z‖)⁻¹
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
rw : HasDerivAt f (f' ((↑t : ℂ) * z)) ((↑t : ℂ) * z)
⊢ HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
⊢ HasDerivAt f (f' ((↑t : ℂ) * z)) ((↑t : ℂ) * z)

Tactic:
hasDerivAt_log_sub_logTaylor n <|
      StarConvex.add_smul_mem starConvex_one_slitPlane (mem_slitPlane_of_norm_lt_one hz) ht.1 ht.2

Premises used: StarConvex.add_smul_mem, Complex.starConvex_one_slitPlane, Complex.mem_slitPlane_of_norm_lt_one, And.right, And.left, Complex.hasDerivAt_log_sub_logTaylor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
⊢ HasDerivAt f (f' ((↑t : ℂ) * z)) ((↑t : ℂ) * z)

Tactic:
exact hasDerivAt_log_sub_logTaylor n <|
      StarConvex.add_smul_mem starConvex_one_slitPlane (mem_slitPlane_of_norm_lt_one hz) ht.1 ht.2

Premises used: StarConvex.add_smul_mem, Complex.starConvex_one_slitPlane, Complex.mem_slitPlane_of_norm_lt_one, And.right, And.left, Complex.hasDerivAt_log_sub_logTaylor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
⊢ ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)

Tactic:
have hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (0 + t * z)) (0 + t * z) := by
    intro t ht
    rw [zero_add]
    exact hasDerivAt_log_sub_logTaylor n <|
      StarConvex.add_smul_mem starConvex_one_slitPlane (mem_slitPlane_of_norm_lt_one hz) ht.1 ht.2
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
simp : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' ((↑t : ℂ) * z)) (Set.Icc 0 1)
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)

Tactic:
simp only [zero_add]

Premises used: zero_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
⊢ Continuous (Y := ℂ) fun (t : ℝ) ↦ (-((↑t : ℂ) * z)) ^ n

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' ((↑t : ℂ) * z)) (Set.Icc 0 1)

Tactic:
exact (Continuous.continuousOn (by fun_prop)).mul <|
      continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz

Premises used: Continuous.continuousOn, Complex.mem_slitPlane_of_norm_lt_one, ContinuousOn.mul, Complex.continuousOn_one_add_mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)

Tactic:
have hcont : ContinuousOn (fun t : ℝ ↦ f' (0 + t * z)) (Set.Icc 0 1) := by
    simp only [zero_add]
    exact (Continuous.continuousOn (by fun_prop)).mul <|
      continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
⊢ f (0 + z) - f 0 = HSMul.hSMul (β := ℂ) z (∫ (t : ℝ) in 0..1, f' (0 + t • z))

Tactic:
(integral_unitInterval_deriv_eq_sub hcont hderiv).symm

Premises used: Eq.symm, intervalIntegral.integral_unitInterval_deriv_eq_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
h : f z = f (0 + z) - f 0
h₁ :
  z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹ =
    HSMul.hSMul (β := ℂ) z (∫ (t : ℝ) in 0..1, f' (0 + t • z))
⊢ f z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹

Tactic:
convert! (integral_unitInterval_deriv_eq_sub hcont hderiv).symm using 1

Premises used: Eq.symm, intervalIntegral.integral_unitInterval_deriv_eq_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
⊢ f z = f (0 + z) - f 0

Tactic:
simp only [f, zero_add, add_zero, log_one, logTaylor_at_zero, sub_self, sub_zero]

Premises used: Complex.log_one, sub_self, sub_zero, zero_add, Complex.logTaylor_at_zero, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
⊢ z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹ =
    HSMul.hSMul (β := ℂ) z (∫ (t : ℝ) in 0..1, f' (0 + t • z))

Tactic:
simp only [f', real_smul, zero_add,
        smul_eq_mul]

Premises used: Complex.real_smul, zero_add, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
⊢ f z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹

Tactic:
have H : f z = z * ∫ t in (0 : ℝ)..1, (-(t * z)) ^ n * (1 + t * z)⁻¹ := by
    convert! (integral_unitInterval_deriv_eq_sub hcont hderiv).symm using 1
    · simp only [f, zero_add, add_zero, log_one, logTaylor_at_zero, sub_self, sub_zero]
    · simp only [f', real_smul, zero_add,
        smul_eq_mul]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : (z : ℂ) → ℂ := fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z
f' : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (-z) ^ n * (1 + z)⁻¹
hderiv :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t → HasDerivAt f (f' (0 + (↑t : ℂ) * z)) (0 + (↑t : ℂ) * z)
hcont : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ f' (0 + (↑t : ℂ) * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹
simp :
  ‖z‖ * norm (E := ℂ) (∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤
    ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp only [H, norm_mul]

Premises used: norm_mul