awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
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
⊢ 2⁻¹ ≤ 1 - ‖z‖
have linarith₆ : 1 - ‖z‖ < 2⁻¹ → 2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 2 1 - 2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
have this : (1 - ‖z‖)⁻¹ ≤ 2
Tactic: have : (1 - ‖z‖)⁻¹ ≤ 2 := by rw [inv_le_comm₀ (sub_pos_of_lt hz1) two_pos]; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
have h : ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
Tactic: apply (norm_log_sub_logTaylor_le n hz1).trans
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z ^ (n + 1)‖
have h : (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1) ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1)
Tactic: rw [mul_div_assoc, mul_comm, norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1) ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1)
have h : 0 ≤ ‖z‖ ^ (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
h : 0 ≤ ‖z‖ ^ (n + 1)
⊢ (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1) ≤ 2 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖z‖ ^ (n + 1)
have h₁ : 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (z : ℂ) ↦ log (1 + z) - z) fun (z : ℂ) ↦ HPow.hPow (β := ℕ) z 2
have h : ∀ (x : ℂ), x = logTaylor (HAdd.hAdd (α := ℕ) 1 1) x
Tactic: convert! log_sub_logTaylor_isBigO 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z)‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖
have rw : ‖log (1 + z) - z + z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖
Tactic: rw [← sub_add_cancel (log (1 + z)) z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ ‖log (1 + z)‖ ≤ 3 / 2 * ‖z‖
have apply : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
Tactic: apply le_trans (norm_log_one_add_le (lt_of_le_of_lt hz one_half_lt_one))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ (1 - ‖z‖)⁻¹ ≤ 2
have rw : 1 ≤ 2 * (1 - ‖z‖)
Tactic: rw [inv_eq_one_div, div_le_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
rw : 1 ≤ 2 * (1 - ‖z‖)
⊢ (1 - ‖z‖)⁻¹ ≤ 2
have rw₁ : 0 < 1 - ‖z‖
Tactic: rw [inv_eq_one_div, div_le_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 ≤ 2 * (1 - ‖z‖)
have linarith : 2 * (1 - ‖z‖) < 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
linarith : 2 * (1 - ‖z‖) < 1 → 2 / 2 = 1
⊢ 1 ≤ 2 * (1 - ‖z‖)
have linarith₁ : 2 * (1 - ‖z‖) < 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
linarith : 2 * (1 - ‖z‖) < 1 → 2 / 2 = 1
linarith₁ : 2 * (1 - ‖z‖) < 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 ≤ 2 * (1 - ‖z‖)
have linarith₂ : 2 * (1 - ‖z‖) < 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
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
⊢ 1 ≤ 2 * (1 - ‖z‖)
have linarith₃ : 2 * (1 - ‖z‖) < 1 → 2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1 + (2 * (1 - ‖z‖) - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 0 < 1 - ‖z‖
have linarith : 1 - ‖z‖ ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
linarith : 1 - ‖z‖ ≤ 0 → 2 / 2 = 1
⊢ 0 < 1 - ‖z‖
have linarith₁ : 1 - ‖z‖ ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
linarith : 1 - ‖z‖ ≤ 0 → 2 / 2 = 1
linarith₁ : 1 - ‖z‖ ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < 1 - ‖z‖
have linarith₂ : 1 - ‖z‖ ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
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
⊢ 0 < 1 - ‖z‖
have linarith₃ : 1 - ‖z‖ ≤ 0 → -1 + (2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - ‖z‖ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have hz3 : (1 - ‖z‖)⁻¹ ≤ 2
Tactic: have hz3 : (1 - ‖z‖)⁻¹ ≤ 2 := by
    rw [inv_eq_one_div, div_le_iff₀]
    · linarith
    · linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2
have hab : 0 ≤ (1 - ‖z‖)⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hab : 0 ≤ (1 - ‖z‖)⁻¹
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2
have hab₁ : HPow.hPow (β := ℕ) ‖z‖ 2 ≤ ‖z‖ / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ (1 - ‖z‖)⁻¹
have hab : 0 ≤ 1 - ‖z‖
Tactic: rw [inv_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ 1 - ‖z‖
have linarith : 1 - ‖z‖ < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
linarith : 1 - ‖z‖ < 0 → 2 / 2 = 1
⊢ 0 ≤ 1 - ‖z‖
have linarith₁ : 1 - ‖z‖ < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
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
⊢ 0 ≤ 1 - ‖z‖
have linarith₂ : 1 - ‖z‖ < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
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
⊢ 0 ≤ 1 - ‖z‖
have linarith₃ : 1 - ‖z‖ < 0 → -1 + (2 * ‖z‖ - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - ‖z‖ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 ≤ ‖z‖ / 2
have hab : ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)
Tactic: rw [sq, div_eq_mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)
have hab : 0 ≤ ‖z‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have hz4 : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
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‖ ≤ 3 / 2 * ‖z‖
have hz4₁ : 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
Cleared hypotheses: hz4
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have linarith₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have linarith₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 2 1 = 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have linarith₃ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have linarith₄ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₄ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₆ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have linarith₇ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
linarith : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₄ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₆ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → GT.gt (α := ℝ) 2 0
linarith₈ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 1 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 1
linarith₉ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₀ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁₁ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₂ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁₃ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₄ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → GT.gt (α := ℝ) 2 0
linarith₁₅ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → 2 / 2 = 1
linarith₁₆ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₇ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ → GT.gt (α := ℝ) 2 0
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
have linarith₁₈ : 3 / 2 * ‖z‖ < HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ →
  1 * HPow.hPow (β := ℕ) (1 * ‖z‖) 2 * (1 * (1 - ‖z‖)⁻¹) - 1 * ‖z‖ +
      (HMul.hMul (α := ℝ) 1 3 * (1 * ‖z‖) - (1 * HPow.hPow (β := ℕ) (1 * ‖z‖) 2 * (1 * (1 - ‖z‖)⁻¹) + 2 * ‖z‖)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 - z)⁻¹ + logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rw : ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [sub_eq_add_neg,
    log_inv _ <| slitPlane_arg_ne_pi <| mem_slitPlane_of_norm_lt_one <| (norm_neg z).symm ▸ hz,
    ← sub_neg_eq_add, ← neg_sub', norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have h : ‖z‖ = ‖-z‖
Tactic: convert! norm_log_sub_logTaylor_le n <| (norm_neg z).symm ▸ hz using 4
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
h : ‖z‖ = ‖-z‖
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have h₁ : 1 - ‖z‖ = 1 - ‖-z‖
Tactic: convert! norm_log_sub_logTaylor_le n <| (norm_neg z).symm ▸ hz using 4
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖z‖ = ‖-z‖
have h : ‖z‖ = ‖z‖
Tactic: rw [norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ = 1 - ‖-z‖
have h : 1 - ‖z‖ = 1 - ‖z‖
Tactic: rw [norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 - z)⁻¹ - z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2
have h : log (1 - z)⁻¹ - z = log (1 - z)⁻¹ + logTaylor (HAdd.hAdd (α := ℕ) 1 1) (-z)
Tactic: convert! norm_log_one_sub_inv_add_logTaylor_neg_le 1 hz using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
h : log (1 - z)⁻¹ - z = log (1 - z)⁻¹ + logTaylor (HAdd.hAdd (α := ℕ) 1 1) (-z)
⊢ ‖log (1 - z)⁻¹ - z‖ ≤ HPow.hPow (β := ℕ) ‖z‖ 2 * (1 - ‖z‖)⁻¹ / 2
have h₁ : 2 = HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1
Tactic: convert! norm_log_one_sub_inv_add_logTaylor_neg_le 1 hz using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)) (log (1 + z))
have refine_1 : Summable (α := ℝ) fun (i : ℕ) ↦ ‖HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)‖
Tactic: refine (hasSum_iff_tendsto_nat_of_summable_norm ?_).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
refine_1 : Summable (α := ℝ) fun (i : ℕ) ↦ ‖HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)‖
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)) (log (1 + z))
have refine_2 : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)) atTop
  (nhds (log (1 + z)))
Tactic: refine (hasSum_iff_tendsto_nat_of_summable_norm ?_).mpr ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)‖
have refine_1 : ∀ (b : ℕ), ‖HPow.hPow (α := ℂ) (-1) (b + 1) * z ^ b / (↑b : ℂ)‖ ≤ ‖z ^ b‖
Tactic: refine (summable_geometric_of_norm_lt_one hz).norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)‖ ≤ ‖z ^ n‖
have refine_1 : ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
Tactic: simp only [norm_div, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul, norm_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
have refine_1 : HPow.hPow (β := ℕ) ‖z‖ 0 / (↑0 : ℝ) ≤ HPow.hPow (β := ℕ) ‖z‖ 0
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
refine_1 : HPow.hPow (β := ℕ) ‖z‖ 0 / (↑0 : ℝ) ≤ HPow.hPow (β := ℕ) ‖z‖ 0
⊢ ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
have refine_1₁ : ∀ (hn : n > 0), ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
| ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
have enter : ‖z‖ ^ n
Tactic: enter [2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
| ‖z‖ ^ n
have rw : ‖z‖ ^ n / 1
Tactic: rw [← div_one (‖z‖ ^ n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
| ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
have enter : ‖z‖ ^ n / 1
Tactic: enter [2]; rw [← div_one (‖z‖ ^ n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n
have refine_1 : ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n / 1
Tactic: conv => enter [2]; rw [← div_one (‖z‖ ^ n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / (↑n : ℝ) ≤ ‖z‖ ^ n / 1
have refine_1 : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)
have refine_1 : 1 ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ)) atTop
    (nhds (log (1 + z)))
have refine_2 : Tendsto (β := ℂ) (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z))
  atTop (nhds 0)
Tactic: rw [← tendsto_sub_nhds_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
| Tendsto (β := ℂ)
    (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)) atTop
    (nhds 0)
have h : ∀ (x : ℕ), ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)
Tactic: enter [1, x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
x : ℕ
| ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)
have h : (logTaylor x z - log (1 + z)) / 1
Tactic: rw [← div_one (_ - _), ← logTaylor]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
| Tendsto (β := ℂ)
    (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)) atTop
    (nhds 0)
have h : ∀ (x : ℕ), (logTaylor x z - log (1 + z)) / 1
Tactic: enter [1, x]; rw [← div_one (_ - _), ← logTaylor]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (β := ℂ)
    (fun (x : ℕ) ↦ ∑ i ∈ Finset.range x, HPow.hPow (α := ℂ) (-1) (i + 1) * z ^ i / (↑i : ℂ) - log (1 + z)) atTop
    (nhds 0)
have refine_2 : Tendsto (β := ℂ) (fun (x : ℕ) ↦ (logTaylor x z - log (1 + z)) / 1) atTop (nhds 0)
Tactic: conv => enter [1, x]; rw [← div_one (_ - _), ← logTaylor]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (β := ℂ) (fun (x : ℕ) ↦ (logTaylor x z - log (1 + z)) / 1) atTop (nhds 0)
have refine_2 : IsLittleO (E := ℂ) (F := ℂ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (x : ℕ) ↦ 1
Tactic: rw [← isLittleO_iff_tendsto fun _ h ↦ (one_ne_zero h).elim]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ IsLittleO (E := ℂ) (F := ℂ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (x : ℕ) ↦ 1
have refine_2 : IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (_x : ℕ) ↦ 1
Tactic: refine IsLittleO.trans_isBigO ?_ <| isBigO_const_one ℂ (1 : ℝ) atTop