awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_rw :
  ‖z‖ ^ (n + 1) * norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤
    ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ‖z‖ * norm (E := ℂ) (∫ (t : ℝ) in 0..1, (-((↑t : ℂ) * z)) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤
    ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp_rw [neg_pow (_ * z) n, mul_assoc, intervalIntegral.integral_const_mul, mul_pow,
    mul_comm _ (z ^ n), mul_assoc, intervalIntegral.integral_const_mul, norm_mul, norm_pow,
    norm_neg, norm_one, one_pow, one_mul, ← mul_assoc, ← pow_succ', mul_div_assoc]

Premises used: one_pow, HMul.hMul, norm_pow, mul_assoc, mul_div_assoc, NormOneClass.norm_one, norm_mul, HPow.hPow, norm_neg, neg_pow, mul_comm, mul_pow, pow_succ', one_mul, intervalIntegral.integral_const_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)⁻¹
hbc :
  norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ‖z‖ ^ (n + 1) * norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤
    ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
gcongr _ * ?_
-- 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)⁻¹
⊢ norm (E := ℂ) (∫ (t : ℝ) in 0..1, (↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹

Tactic:
intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help

Premises used: zero_le_one, intervalIntegral.norm_integral_le_of_norm_le
-- 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)⁻¹
refine :
  ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) t → ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
⊢ norm (E := ℂ) (∫ (t : ℝ) in 0..1, (↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹

Tactic:
refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help

Premises used: zero_le_one, intervalIntegral.norm_integral_le_of_norm_le
-- 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)⁻¹
t : ℝ
h : ∀ (ht₀ : 0 < t) (ht₁ : t ≤ 1), ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
⊢ Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) t → ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹

Tactic:
⟨ht₀, ht₁⟩
-- 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)⁻¹
h : ∀ (t : ℝ) (ht₀ : 0 < t) (ht₁ : t ≤ 1), ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
⊢ ∀ᵐ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioc 0 1) t → ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹

Tactic:
filter_upwards with t ⟨ht₀, ht₁⟩
-- 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)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
h : t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
⊢ ‖(↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹

Tactic:
rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]

Premises used: norm_pow, LT.lt.le, norm_mul, Complex.norm_of_nonneg
-- 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)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
h : ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
⊢ t ^ n * ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹

Tactic:
gcongr
-- 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)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz

Premises used: Complex.norm_one_add_mul_inv_le, LT.lt.le, And.intro
-- 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)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
exact norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz

Premises used: Complex.norm_one_add_mul_inv_le, LT.lt.le, And.intro
-- 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)⁻¹
rw :
  (1 - ‖z‖)⁻¹ * ((HPow.hPow (α := ℝ) 1 (n + 1) - HPow.hPow (α := ℝ) 0 (n + 1)) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹ = (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]

Premises used: integral_pow, mul_comm, intervalIntegral.integral_mul_const
-- 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)⁻¹
⊢ (1 - ‖z‖)⁻¹ * ((HPow.hPow (α := ℝ) 1 (n + 1) - HPow.hPow (α := ℝ) 0 (n + 1)) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) =
    (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp [field]
-- 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)⁻¹
calc : norm (E := ℂ) (∫ (t : ℝ) in 0..1, (↑t : ℂ) ^ n * (1 + (↑t : ℂ) * z)⁻¹) ≤ ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹
calc₁ : ∫ (t : ℝ) in 0..1, t ^ n * (1 - ‖z‖)⁻¹ = (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ norm (E := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ n * (1 + (↑x : ℂ) * z)⁻¹) ≤ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
calc ‖∫ t in (0 : ℝ)..1, (t : ℂ) ^ n * (1 + t * z)⁻¹‖
    _ ≤ ∫ t in (0 : ℝ)..1, t ^ n * (1 - ‖z‖)⁻¹ := by
      refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help
      filter_upwards with t ⟨ht₀, ht₁⟩
      rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]
      gcongr
      exact norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz
    _ = (1 - ‖z‖)⁻¹ / (n + 1) := by
      rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]
      simp [field]

Premises used: Norm.norm, HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - logTaylor (HAdd.hAdd (α := ℕ) 1 1) z‖ ≤
    ‖z‖ ^ HAdd.hAdd (α := ℕ) 1 1 * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1

Tactic:
norm_log_sub_logTaylor_le 1 hz

Premises used: Complex.norm_log_sub_logTaylor_le, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
h : log (1 + z) - z = log (1 + z) - logTaylor (HAdd.hAdd (α := ℕ) 1 1) z
h₁ : 2 = HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1
⊢ ‖log (1 + z) - z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2

Tactic:
convert! norm_log_sub_logTaylor_le 1 hz using 2

Premises used: Complex.norm_log_sub_logTaylor_le, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ log (1 + z) - z = log (1 + z) - logTaylor (HAdd.hAdd (α := ℕ) 1 1) z

Tactic:
simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Complex.logTaylor_zero, Complex.logTaylor_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ 2 = HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
rw : ∃ (c : ℝ), ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ c * ‖x ^ (n + 1)‖
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z) fun (z : ℂ) ↦ z ^ (n + 1)

Tactic:
rw [Asymptotics.isBigO_iff]

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
h : ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ (n + 1)‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ c * ‖x ^ (n + 1)‖

Tactic:
use 2 / (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
h :
  ∀ (z : ℂ) (hz1 : ‖z - 0‖ < 1) (hz12 : ‖z - 0‖ < 1 / 2),
    ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ (n + 1)‖

Tactic:
filter_upwards [
    eventually_norm_sub_lt 0 one_pos,
    eventually_norm_sub_lt 0 (show 0 < 1 / 2 by simp)] with z hz1 hz12

Premises used: eventually_norm_sub_lt, OfNat.ofNat, one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z - 0‖ < 1
hz12 : ‖z - 0‖ < 1 / 2
⊢ ‖z‖ < 1

Tactic:
rw [sub_zero] at hz1 hz12

Premises used: sub_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z - 0‖ < 1
hz12 : ‖z - 0‖ < 1 / 2
hz1₁ : ‖z‖ < 1
⊢ ‖z‖ < 1 / 2

Tactic:
rw [sub_zero] at hz1 hz12

Premises used: sub_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
rw : 2⁻¹ ≤ 1 - ‖z‖
⊢ (1 - ‖z‖)⁻¹ ≤ 2

Tactic:
rw [inv_le_comm₀ (sub_pos_of_lt hz1) two_pos]

Premises used: two_pos, inv_le_comm₀, sub_pos_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
linarith : 1 - ‖z‖ < 2⁻¹ → 2 / 2 = 1
linarith₁ : 1 - ‖z‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - ‖z‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - ‖z‖ < 2⁻¹ → 2 / 2 = 1
linarith₄ : 1 - ‖z‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 - ‖z‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
linarith₆ :
  1 - ‖z‖ < 2⁻¹ → 2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 2 1 - 2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1) = 0
⊢ 2⁻¹ ≤ 1 - ‖z‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ (1 - ‖z‖)⁻¹ ≤ 2

Tactic:
have : (1 - ‖z‖)⁻¹ ≤ 2 := by rw [inv_le_comm₀ (sub_pos_of_lt hz1) two_pos]; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
h : ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖

Tactic:
apply (norm_log_sub_logTaylor_le n hz1).trans

Premises used: Complex.norm_log_sub_logTaylor_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
h : (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1) ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1)
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖

Tactic:
rw [mul_div_assoc, mul_comm, norm_pow]

Premises used: norm_pow, mul_div_assoc, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
h : 0 ≤ ‖z‖ ^ (n + 1)
h₁ : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1) ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 + z) - logTaylor (HAdd.hAdd (α := ℕ) 1 1) z)
    fun (z : ℂ) ↦ z ^ HAdd.hAdd (α := ℕ) 1 1

Tactic:
log_sub_logTaylor_isBigO 1

Premises used: Complex.log_sub_logTaylor_isBigO, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
h : ∀ (x : ℂ), x = logTaylor (HAdd.hAdd (α := ℕ) 1 1) x
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 + z) - z) fun (z : ℂ) ↦ HPow.hPow (β := ℕ) z 2

Tactic:
convert! log_sub_logTaylor_isBigO 1

Premises used: Complex.log_sub_logTaylor_isBigO, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
x : ℂ
⊢ x = logTaylor (HAdd.hAdd (α := ℕ) 1 1) x

Tactic:
simp [logTaylor_succ, logTaylor_zero]

Premises used: Complex.logTaylor_zero, Complex.logTaylor_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
rw : ‖log (1 + z) - z + z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖
⊢ ‖log (1 + z)‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Tactic:
rw [← sub_add_cancel (log (1 + z)) z]

Premises used: Complex.log, HAdd.hAdd, OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z + z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Tactic:
norm_add_le_of_le (Complex.norm_log_one_add_sub_self_le hz) le_rfl

Premises used: le_rfl, Complex.norm_log_one_add_sub_self_le, norm_add_le_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z + z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Tactic:
exact norm_add_le_of_le (Complex.norm_log_one_add_sub_self_le hz) le_rfl

Premises used: le_rfl, Complex.norm_log_one_add_sub_self_le, norm_add_le_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
apply : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
⊢ ‖log (1 + z)‖ ≤ 3 / 2 * ‖z‖

Tactic:
apply le_trans (norm_log_one_add_le (lt_of_le_of_lt hz one_half_lt_one))

Premises used: lt_of_le_of_lt, Complex.norm_log_one_add_le, one_half_lt_one, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
rw : 1 ≤ 2 * (1 - ‖z‖)
rw₁ : 0 < 1 - ‖z‖
⊢ (1 - ‖z‖)⁻¹ ≤ 2

Tactic:
rw [inv_eq_one_div, div_le_iff₀]

Premises used: div_le_iff₀, inv_eq_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
linarith : 2 * (1 - ‖z‖) < 1 → 2 / 2 = 1
linarith₁ : 2 * (1 - ‖z‖) < 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 2 * (1 - ‖z‖) < 1 → GT.gt (α := ℝ) 2 0
linarith₃ : 2 * (1 - ‖z‖) < 1 → 2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1 + (2 * (1 - ‖z‖) - 1) = 0
⊢ 1 ≤ 2 * (1 - ‖z‖)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
linarith : 1 - ‖z‖ ≤ 0 → 2 / 2 = 1
linarith₁ : 1 - ‖z‖ ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - ‖z‖ ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - ‖z‖ ≤ 0 → -1 + (2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - ‖z‖ - 0) = 0
linarith₄ : 1 - ‖z‖ ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 1 - ‖z‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ (1 - ‖z‖)⁻¹ ≤ 2

Tactic:
have hz3 : (1 - ‖z‖)⁻¹ ≤ 2 := by
    rw [inv_eq_one_div, div_le_iff₀]
    · linarith
    · linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hab : 0 ≤ (1 - ‖z‖)⁻¹
hab₁ : HPow.hPow (β := ℕ) ‖z‖ 2 ≤ ‖z‖ / 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hab : 0 ≤ 1 - ‖z‖
⊢ 0 ≤ (1 - ‖z‖)⁻¹

Tactic:
rw [inv_nonneg]

Premises used: inv_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
linarith : 1 - ‖z‖ < 0 → 2 / 2 = 1
linarith₁ : 1 - ‖z‖ < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - ‖z‖ < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - ‖z‖ < 0 → -1 + (2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - ‖z‖ - 0) = 0
linarith₄ : 1 - ‖z‖ < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ 1 - ‖z‖

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hab : ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 ≤ ‖z‖ / 2

Tactic:
rw [sq, div_eq_mul_one_div]

Premises used: sq, div_eq_mul_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hab : 0 ≤ ‖z‖
⊢ ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2

Tactic:
have hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2 := by
    gcongr
    · rw [inv_nonneg]
      linarith
    · rw [sq, div_eq_mul_one_div]
      gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2

Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
    IsUnit.div_mul_cancel] at hz4

Premises used: OfNat.ofNat_ne_zero, isUnit_iff_ne_zero, ne_eq, IsUnit.div_mul_cancel, not_false_eq_true