awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖
have rw : ‖log (1 + z) - logTaylor n z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ n
Tactic: rw [norm_sub_rev, norm_pow, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)
have succ : ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)
Tactic: refine (norm_log_sub_logTaylor_le n hz).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)
have succ : (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / 1
Tactic: rw [mul_comm, ← div_one ((max _ _) * _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / 1
have succ : (1 - ‖z‖)⁻¹ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
succ : (1 - ‖z‖)⁻¹ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹
⊢ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1) / 1
have succ₁ : 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ 1 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < 1 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖log (1 + z) - logTaylor n z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ n
have zero : ‖log (1 + z) - logTaylor 0 z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * HPow.hPow (β := ℕ) ‖z‖ 0
Tactic: cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
zero : ‖log (1 + z) - logTaylor 0 z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * HPow.hPow (β := ℕ) ‖z‖ 0
⊢ ‖log (1 + z) - logTaylor n z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ n
have succ : ∀ (n : ℕ), ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ (n + 1)
Tactic: cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
have this : ∀ (n : ℕ), ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖
Tactic: have (n : ℕ) : ‖logTaylor n z - log (1 + z)‖
          ≤ (max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹) * ‖(‖z‖ ^ n)‖ := by
        rw [norm_sub_rev, norm_pow, norm_norm]
        cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (_x : ℕ) ↦ 1
have H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
Tactic: have H : (fun n ↦ logTaylor n z - log (1 + z)) =O[atTop] (fun n : ℕ ↦ ‖z‖ ^ n) := by
      have (n : ℕ) : ‖logTaylor n z - log (1 + z)‖
          ≤ (max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹) * ‖(‖z‖ ^ n)‖ := by
        rw [norm_sub_rev, norm_pow, norm_norm]
        cases n with
        | zero => simp [logTaylor_zero]
        | succ n =>
            refine (norm_log_sub_logTaylor_le n hz).trans ?_
            rw [mul_comm, ← div_one ((max _ _) * _)]
            gcongr
            · exact le_max_right ..
            · linarith
      exact (isBigOWith_of_le' atTop this).isBigO
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
⊢ IsLittleO (E := ℂ) (F := ℝ) atTop (fun (x : ℕ) ↦ logTaylor x z - log (1 + z)) fun (_x : ℕ) ↦ 1
have refine_2 : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖z‖ ^ n) fun (_x : ℕ) ↦ 1
Tactic: refine IsBigO.trans_isLittleO H ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
H : IsBigO (E := ℂ) (F := ℝ) atTop (fun (n : ℕ) ↦ logTaylor n z - log (1 + z)) fun (n : ℕ) ↦ ‖z‖ ^ n
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ ‖z‖ ^ n) fun (_x : ℕ) ↦ 1
have h : ∀ (x : ℕ), 1 = HPow.hPow (α := ℝ) 1 x
Tactic: convert! isLittleO_pow_pow_of_lt_left (norm_nonneg z) hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
| HasSum (fun (n : ℕ) ↦ z ^ n / (↑n : ℂ)) (-log (1 - z))
have h : ∀ (n : ℕ), z ^ n / (↑n : ℂ)
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
| z ^ n / (↑n : ℂ)
have h : - -(z ^ n / (↑n : ℂ))
Tactic: rw [← neg_neg (z ^ n / n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
| HasSum (fun (n : ℕ) ↦ z ^ n / (↑n : ℂ)) (-log (1 - z))
have h : ∀ (n : ℕ), - -(z ^ n / (↑n : ℂ))
Tactic: enter [1, n]; rw [← neg_neg (z ^ n / n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ z ^ n / (↑n : ℂ)) (-log (1 - z))
have conv : HasSum (fun (n : ℕ) ↦ - -(z ^ n / (↑n : ℂ))) (-log (1 - z))
Tactic: conv => enter [1, n]; rw [← neg_neg (z ^ n / n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ - -(z ^ n / (↑n : ℂ))) (-log (1 - z))
have refine : HasSum (fun (n : ℕ) ↦ -(z ^ n / (↑n : ℂ))) (log (1 - z))
Tactic: refine HasSum.neg ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
⊢ HasSum (fun (n : ℕ) ↦ -(z ^ n / (↑n : ℂ))) (log (1 - z))
have h : ∀ (n : ℕ), -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)
Tactic: convert! hasSum_taylorSeries_log (z := -z) (norm_neg z ▸ hz) using 2 with n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)
have h : -(HPow.hPow (β := ℕ) z 0 / (↑0 : ℂ)) =
  HPow.hPow (α := ℂ) (-1) (HAdd.hAdd (α := ℕ) 0 1) * HPow.hPow (β := ℕ) (-z) 0 / (↑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 : ℕ
h :
  -(HPow.hPow (β := ℕ) z 0 / (↑0 : ℂ)) =
    HPow.hPow (α := ℂ) (-1) (HAdd.hAdd (α := ℕ) 0 1) * HPow.hPow (β := ℕ) (-z) 0 / (↑0 : ℂ)
⊢ -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)
have h₁ : ∀ (hn : n > 0), -(z ^ n / (↑n : ℂ)) = HPow.hPow (α := ℂ) (-1) (n + 1) * (-z) ^ n / (↑n : ℂ)
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) atTop (𝓝 t)
have apply : Tendsto (β := ℝ) (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) atTop (𝓝 0)
Tactic: apply hg.congr_dist
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) atTop (𝓝 0)
have refine : IsBigO (E := ℝ) (F := ℂ) atTop (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) fun (x : ℝ) ↦ (↑x⁻¹ : ℂ)
Tactic: refine IsBigO.trans_tendsto ?_ tendsto_inv_atTop_zero.ofReal
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ IsBigO (E := ℝ) (F := ℂ) atTop (fun (x : ℝ) ↦ dist ((↑x : ℂ) * g x) ((↑x : ℂ) * log (1 + g x))) fun (x : ℝ) ↦
    (↑x⁻¹ : ℂ)
have simp_rw : IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦ (↑x⁻¹ : ℂ)
Tactic: simp_rw [dist_comm (_ * g _), dist_eq, ← mul_sub, isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦
    (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2
have hg0 : Tendsto g atTop (𝓝 0)
Tactic: have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
        (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)
have h : ∀ (x : ℝ) (hx0 : x ≠ 0), (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2 = HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)
Tactic: filter_upwards [eventually_ne_atTop 0] with x hx0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
x : ℝ
hx0 : x ≠ 0
⊢ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2 = HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)
have h : (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2 * (↑x : ℂ) = HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2
Tactic: rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦ (↑x⁻¹ : ℂ)
have _ : IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦
  (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2
Tactic: calc
    _ =O[atTop] fun x ↦ x * g x ^ 2 := by
      have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
        (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
      exact (isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)
    _ =ᶠ[atTop] fun x ↦ (x * g x) ^ 2 * x⁻¹ := by
      filter_upwards [eventually_ne_atTop 0] with x hx0
      rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]
      ring
    _ =O[atTop] _ := by
      simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
_ :
  IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦
    (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦ (↑x⁻¹ : ℂ)
have _₁ : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2) fun (x : ℝ) ↦
  HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)
Tactic: calc
    _ =O[atTop] fun x ↦ x * g x ^ 2 := by
      have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
        (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
      exact (isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)
    _ =ᶠ[atTop] fun x ↦ (x * g x) ^ 2 * x⁻¹ := by
      filter_upwards [eventually_ne_atTop 0] with x hx0
      rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]
      ring
    _ =O[atTop] _ := by
      simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
_ :
  IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦
    (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2
_₁ :
  EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * HPow.hPow (β := ℕ) (g x) 2) fun (x : ℝ) ↦
    HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)
⊢ IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * (log (1 + g x) - g x)) fun (x : ℝ) ↦ (↑x⁻¹ : ℂ)
have _₂ : IsBigO (E := ℂ) (F := ℂ) atTop (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) ((↑x : ℂ) * g x) 2 * (↑x⁻¹ : ℂ)) fun (x : ℝ) ↦
  (↑x⁻¹ : ℂ)
Tactic: calc
    _ =O[atTop] fun x ↦ x * g x ^ 2 := by
      have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hg.norm.isBoundedUnder_le
        (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
      exact (isBigO_refl _ _).mul (log_sub_self_isBigO.comp_tendsto hg0)
    _ =ᶠ[atTop] fun x ↦ (x * g x) ^ 2 * x⁻¹ := by
      filter_upwards [eventually_ne_atTop 0] with x hx0
      rw [ofReal_inv, eq_mul_inv_iff_mul_eq₀ (mod_cast hx0)]
      ring
    _ =O[atTop] _ := by
      simpa using isBigO_const_of_tendsto hg (one_ne_zero (α := ℂ))
        |>.pow 2 |>.mul (isBigO_refl _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ Tendsto (fun (x : ℝ) ↦ (1 + g x) ^ (↑x : ℂ)) atTop (𝓝 (cexp t))
have apply : (cexp ∘ fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) =ᶠ[atTop] fun (x : ℝ) ↦ (1 + g x) ^ (↑x : ℂ)
Tactic: apply ((continuous_exp.tendsto _).comp (tendsto_mul_log_one_add_of_tendsto hg)).congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
⊢ (cexp ∘ fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) =ᶠ[atTop] fun (x : ℝ) ↦ (1 + g x) ^ (↑x : ℂ)
have hg0 : Tendsto g atTop (𝓝 0)
Tactic: have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ (cexp ∘ fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) =ᶠ[atTop] fun (x : ℝ) ↦ (1 + g x) ^ (↑x : ℂ)
have h : ∀ (x : ℝ) (hg1 : g x ≠ -1), (cexp ∘ fun (x : ℝ) ↦ (↑x : ℂ) * log (1 + g x)) x = (1 + g x) ^ (↑x : ℂ)
Tactic: filter_upwards [hg0.eventually_ne (show 0 ≠ -1 by simp)] with x hg1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
x : ℝ
hg1 : g x ≠ -1
⊢ cexp ((↑x : ℂ) * log (1 + g x)) = (1 + g x) ^ (↑x : ℂ)
have h : 1 + g x ≠ 0
Tactic: rw [cpow_def_of_ne_zero, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * g x) atTop (𝓝 t)
hg0_1 : Tendsto g atTop (𝓝 0)
x : ℝ
hg1 : g x ≠ -1
hg0 : 1 + g x = 0
⊢ False
have hg1₁ : Ne (α := ℂ) (-1) (-1)
Tactic: rw [← add_eq_zero_iff_neg_eq.mp hg0] at hg1
Cleared hypotheses: hg1, hg0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℂ
⊢ Tendsto (fun (x : ℝ) ↦ (1 + t / (↑x : ℂ)) ^ (↑x : ℂ)) atTop (𝓝 (cexp t))
have hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (t / (↑x : ℂ))) atTop (𝓝 t)
Tactic: apply tendsto_one_add_cpow_exp_of_tendsto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℂ
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (t / (↑x : ℂ))) atTop (𝓝 t)
have hg : ∀ᶠ (x' : ℝ) in atTop, (↑x' : ℂ) * (t / (↑x' : ℂ)) = t
Tactic: apply tendsto_nhds_of_eventually_eq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℂ
⊢ ∀ᶠ (x' : ℝ) in atTop, (↑x' : ℂ) * (t / (↑x' : ℂ)) = t
have h : ∀ (x : ℝ) (hx0 : x ≠ 0), (↑x : ℂ) * (t / (↑x : ℂ)) = t
Tactic: filter_upwards [eventually_ne_atTop 0] with x hx0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ Eq (α := (n : ℕ) → ℂ) (fun (n : ℕ) ↦ f n ^ n) fun (n : ℕ) ↦ (1 + (f n - 1)) ^ n
have h : ∀ (x : ℕ), f x ^ x = (1 + (f x - 1)) ^ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ f n ^ n) atTop (𝓝 (cexp t))
have rw : Tendsto (fun (n : ℕ) ↦ (1 + (f n - 1)) ^ n) atTop (𝓝 (cexp t))
Tactic: rw [show (fun n ↦ f n ^ n) = (fun n ↦ (1 + (f n - 1)) ^ n) by ext; simp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ (1 + (f n - 1)) ^ n) atTop (𝓝 (cexp t))
have refine : Tendsto (β := ℂ) (fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t) atTop (𝓝 0)
Tactic: refine tendsto_one_add_pow_exp_of_tendsto (tendsto_sub_nhds_zero_iff.1 ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ Tendsto (β := ℂ) (fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t) atTop (𝓝 0)
have convert_2 : EventuallyEq (β := ℂ) atTop (fun (x : ℕ) ↦ (HDiv.hDiv (α := ℂ) 1 (↑x : ℂ))⁻¹ • (f x - (1 + t / (↑x : ℂ)))) fun (x : ℕ) ↦
  (↑x : ℂ) * (f x - 1) - t
Tactic: convert! hf.tendsto_inv_smul_nhds_zero.congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℕ) ↦ (HDiv.hDiv (α := ℂ) 1 (↑x : ℂ))⁻¹ • (f x - (1 + t / (↑x : ℂ))))
    fun (x : ℕ) ↦ (↑x : ℂ) * (f x - 1) - t
have h : ∀ (n : ℕ) (h0 : n ≠ 0), (HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))⁻¹ • (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t
Tactic: filter_upwards [eventually_ne_atTop 0] with n h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
n : ℕ
h0 : n ≠ 0
⊢ (HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))⁻¹ • (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t
have h : (↑n : ℂ) * (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
f : ℕ → ℂ
t : ℂ
hf :
  IsLittleO (E := ℂ) (F := ℂ) atTop (fun (n : ℕ) ↦ f n - (1 + t / (↑n : ℂ))) fun (n : ℕ) ↦ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)
n : ℕ
h0 : n ≠ 0
⊢ (↑n : ℂ) * (f n - (1 + t / (↑n : ℂ))) = (↑n : ℂ) * (f n - 1) - t
have h : (↑n : ℂ) * f n - ((↑n : ℂ) + t) = (↑n : ℂ) * (f n - 1) - t
Tactic: field_simp [n.cast_ne_zero.2 h0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
⊢ Tendsto (fun (x : ℝ) ↦ x * log (1 + g x)) atTop (𝓝 t)
have hg0 : Tendsto g atTop (𝓝 0)
Tactic: have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (tendsto_id'.mpr (by simp))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ x * log (1 + g x)) atTop (𝓝 t)
have rw : ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))) (hg0 : Tendsto g atTop (𝓝 0)),
  Tendsto (fun (x : ℝ) ↦ (↑(x * log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))
Tactic: rw [← tendsto_ofReal_iff] at hg ⊢
Cleared hypotheses: hg, hg0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ (↑(x * log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))
have push_cast : ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))),
  Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))
Tactic: push_cast at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)) atTop (𝓝 (↑t : ℂ))
have apply : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ))) fun (x : ℝ) ↦
  (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
Tactic: apply (Complex.tendsto_mul_log_one_add_of_tendsto hg).congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ))) fun (x : ℝ) ↦
    (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
have h : ∀ (x : ℝ) (hg1 : -1 ≤ g x), (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
Tactic: filter_upwards [hg0.eventually_const_le (show (-1 : ℝ) < 0 by simp)] with x hg1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
⊢ 0 ≤ 1 + g x
have linarith : 1 + g x < 0 → -1 - g x + (1 + g x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
⊢ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
have h : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log (↑(1 + g x) : ℂ)
Tactic: rw [Complex.ofReal_log (by linarith), Complex.ofReal_add, Complex.ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
h : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log (↑(1 + g x) : ℂ)
⊢ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
have h₁ : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log ((↑1 : ℂ) + (↑(g x) : ℂ))
Tactic: rw [Complex.ofReal_log (by linarith), Complex.ofReal_add, Complex.ofReal_one]