awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℤ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
this : 0 ≤ (↑n : ℝ) * (2 * π)
⊢ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have lift : ∀ (n : ℕ) (hn : x = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)) (this : 0 ≤ (↑(↑n : ℤ) : ℝ) * (2 * π)),
  ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: lift n to ℕ using by exact_mod_cast nonneg_of_mul_nonneg_left this (by positivity)
Cleared hypotheses: n, hn, this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
k N : ℕ
hN : N ≠ 0
⊢ cexp (2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ)) = 1 ↔ N ∣ k
have rw : (∃ (n : ℤ), 2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ) = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ N ∣ k
Tactic: rw [exp_eq_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
k N : ℕ
hN : N ≠ 0
n : ℤ
| 2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ) = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have rw : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑N : ℂ) = (↑n : ℂ)
Tactic: rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
k N : ℕ
hN : N ≠ 0
⊢ (∃ (n : ℤ), 2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ) = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ N ∣ k
have conv : (∃ (n : ℤ), HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑N : ℂ) = (↑n : ℂ)) ↔ N ∣ k
Tactic: conv in _ = _ => rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
k N : ℕ
hN : N ≠ 0
⊢ (∃ (n : ℤ), HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑N : ℂ) = (↑n : ℂ)) ↔ N ∣ k
have field_simp : (∃ (n : ℤ), (↑k : ℂ) = HMul.hMul (α := ℂ) (↑N : ℂ) (↑n : ℂ)) ↔ N ∣ k
Tactic: field_simp [Nat.cast_ne_zero.mpr hN]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
k N : ℕ
hN : N ≠ 0
⊢ (∃ (n : ℤ), (↑k : ℂ) = HMul.hMul (α := ℂ) (↑N : ℂ) (↑n : ℂ)) ↔ N ∣ k
have norm_cast : (∃ (n : ℤ), (↑k : ℤ) = (↑N : ℤ) * n) ↔ N ∣ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
⊢ cexp x = cexp y ↔ cexp (x - y) = 1
have rw : cexp x = cexp y ↔ cexp x / cexp y = 1
Tactic: rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
rw : cexp x = cexp y ↔ cexp x / cexp y = 1
⊢ cexp x = cexp y ↔ cexp (x - y) = 1
have rw₁ : cexp x = cexp y ↔ cexp x = cexp y
Tactic: rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
h : cexp x = cexp y
⊢ x.re = y.re
have obtain : ∀ (n : ℤ) (hn : x = y + (↑n : ℂ) * (2 * (↑π : ℂ) * I)), x.re = y.re
Tactic: obtain ⟨n, hn⟩ := exp_eq_exp_iff_exists_int.1 h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
z : ℂ
⊢ ∃ (n : ℤ), log (cexp z) = z + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have rw : cexp z ≠ 0
Tactic: rw [← exp_eq_exp_iff_exists_int, exp_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable
have refine_1 : ∀ (hs : (cexp ⁻¹' s).Countable), s.Countable
Tactic: refine ⟨fun hs => ?_, fun hs => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
refine_1 : ∀ (hs : (cexp ⁻¹' s).Countable), s.Countable
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable
have refine_2 : ∀ (hs : s.Countable), (cexp ⁻¹' s).Countable
Tactic: refine ⟨fun hs => ?_, fun hs => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s.Countable
have refine_1 : s ⊆ insert 0 (cexp '' cexp ⁻¹' s)
Tactic: refine ((hs.image exp).insert 0).mono ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (cexp '' cexp ⁻¹' s)
have refine_1 : s ⊆ s ∪ {0}
Tactic: rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.diff_eq, ← Set.union_singleton,
        Set.diff_union_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : s.Countable
⊢ (cexp ⁻¹' s).Countable
have refine_2 : Set.Countable (α := ℂ) (⋃ y ∈ s, cexp ⁻¹' {y})
Tactic: rw [← Set.biUnion_preimage_singleton]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : s.Countable
⊢ Set.Countable (α := ℂ) (⋃ y ∈ s, cexp ⁻¹' {y})
have refine_2 : ∀ (z : ℂ) (hz : z ∈ s), (cexp ⁻¹' {z}).Countable
Tactic: refine hs.biUnion fun z hz => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
⊢ (cexp ⁻¹' {z}).Countable
have pos : ∀ (h : ∃ (w : ℂ), cexp w = z), (cexp ⁻¹' {z}).Countable
Tactic: by_cases! h : ∃ w, exp w = z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
pos : ∀ (h : ∃ (w : ℂ), cexp w = z), (cexp ⁻¹' {z}).Countable
⊢ (cexp ⁻¹' {z}).Countable
have neg : ∀ (h : ∀ (w : ℂ), cexp w ≠ z), (cexp ⁻¹' {z}).Countable
Tactic: by_cases! h : ∃ w, exp w = z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∃ (w : ℂ), cexp w = z
⊢ (cexp ⁻¹' {z}).Countable
have pos : ∀ (w : ℂ) (hz : cexp w ∈ s), (cexp ⁻¹' {cexp w}).Countable
Tactic: rcases h with ⟨w, rfl⟩
Cleared hypotheses: z, hz, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ (cexp ⁻¹' {cexp w}).Countable
have pos : Set.Countable (α := ℂ) (⋃ (i : ℤ), {x : ℂ | x = w + (↑i : ℂ) * (2 * (↑π : ℂ) * I)})
Tactic: simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.setOf_exists]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 ((↑(Real.log ‖z‖) : ℂ) - (↑π : ℂ) * I))
have h : 𝓝 ((↑(Real.log ‖z‖) : ℂ) - (↑π : ℂ) * I) = 𝓝 ((ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) z + (↑(-π) : ℂ) * I)
Tactic: convert!
    (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
      (((continuous_ofReal.tendsto _).comp <|
            tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
h : 𝓝 ((↑(Real.log ‖z‖) : ℂ) - (↑π : ℂ) * I) = 𝓝 ((ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) z + (↑(-π) : ℂ) * I)
⊢ Tendsto log (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 ((↑(Real.log ‖z‖) : ℂ) - (↑π : ℂ) * I))
have convert_1 : ‖z‖ ≠ 0
Tactic: convert!
    (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
      (((continuous_ofReal.tendsto _).comp <|
            tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
have convert_1 : ∀ (z : ℝ) (hre : (↑z : ℂ).re < 0), ‖(↑z : ℂ)‖ ≠ 0
Tactic: lift z to ℝ using him
Cleared hypotheses: z, hre, him
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt log {z : ℂ | 0 ≤ z.im} z
have convert_1 : ‖z‖ ≠ 0
Tactic: convert!
    (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
      ((continuous_ofReal.continuousAt.comp_continuousWithinAt <|
            continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
⊢ map cexp (comap re atBot) = 𝓝[≠] 0
have rw : map cexp (comap cexp (𝓝 0)) = 𝓝[≠] 0
Tactic: rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
rw : map cexp (comap cexp (𝓝 0)) = 𝓝[≠] 0
⊢ map cexp (comap re atBot) = 𝓝[≠] 0
have rw₁ : 𝓝 0 ⊓ 𝓟 (range cexp) = 𝓝[≠] 0
Tactic: rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
rw : map cexp (comap cexp (𝓝 0)) = 𝓝[≠] 0
rw₁ : 𝓝 0 ⊓ 𝓟 (range cexp) = 𝓝[≠] 0
⊢ map cexp (comap re atBot) = 𝓝[≠] 0
have rw₂ : Eq (α := Filter ℂ) (𝓝 0 ⊓ 𝓟 {0}ᶜ) (𝓝[≠] 0)
Tactic: rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
rw : map cexp (comap cexp (𝓝 0)) = 𝓝[≠] 0
rw₁ : 𝓝 0 ⊓ 𝓟 (range cexp) = 𝓝[≠] 0
rw₂ : Eq (α := Filter ℂ) (𝓝 0 ⊓ 𝓟 {0}ᶜ) (𝓝[≠] 0)
⊢ map cexp (comap re atBot) = 𝓝[≠] 0
have rw₃ : Eq (α := Filter ℂ) (𝓝 0 ⊓ 𝓟 {0}ᶜ) (𝓝 0 ⊓ 𝓟 {0}ᶜ)
Tactic: rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
⊢ map cexp (comap re atTop) = cobounded ℂ
have rw : {0}ᶜ ∈ cobounded ℂ
Tactic: rw [← comap_exp_cobounded, map_comap, range_exp, inf_eq_left, le_principal_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt log x
have refine_1 : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑(Real.log ‖x‖) : ℂ)) x
Tactic: refine ContinuousAt.add ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : x ∈ slitPlane
refine_1 : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑(Real.log ‖x‖) : ℂ)) x
⊢ ContinuousAt log x
have refine_2 : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ) * I) x
Tactic: refine ContinuousAt.add ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑(Real.log ‖x‖) : ℂ)) x
have refine_1 : ContinuousAt (Y := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) x
Tactic: refine continuous_ofReal.continuousAt.comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (Y := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) x
have refine_1 : ‖x‖ ≠ 0
Tactic: refine (Real.continuousAt_log ?_).comp continuous_norm.continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (hypothesis)
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ) * I) x
have h_cont_mul : Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I
Tactic: have h_cont_mul : Continuous fun x : ℂ => x * I := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ) * I) x
have refine_2 : ContinuousAt arg x
Tactic: refine h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
z : ℂ
h : z ∈ slitPlane
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | z.im ∈ Ioo (-π) π} (log z)
have simp : 0 ≤ z.re ∨ z.im ≠ 0
Tactic: simp only [mem_setOf, log_im, mem_Ioo, neg_pi_lt_arg, arg_lt_pi_iff, true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ log (1 + z) = z * ∫ (t : ℝ) in 0..1, (1 + t • z)⁻¹
have h : log (1 + z) = log (1 + z) - log 1
Tactic: convert!
    (integral_unitInterval_deriv_eq_sub (continuousOn_one_add_mul_inv hz)
        (fun _ ht ↦
          hasDerivAt_log <|
            StarConvex.add_smul_mem starConvex_one_slitPlane hz ht.1 ht.2)).symm using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
z : ℂ
hz : 1 - z ∈ slitPlane
⊢ log (1 - z)⁻¹ = z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹
have hz₁ : 1 + -z ∈ slitPlane
Tactic: rw [sub_eq_add_neg 1 z] at hz ⊢
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z)⁻¹ = z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹
have rw : log (1 + -z) = -z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹
Tactic: rw [log_inv _ <| slitPlane_arg_ne_pi hz, neg_eq_iff_eq_neg, ← neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z) = -z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹
have h : ∀ (x : ℝ), 1 - x • z = 1 + x • -z
Tactic: convert! log_eq_integral hz using 5
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
x : ℝ
⊢ 1 - x • z = 1 + x • -z
have h : 1 + -(x • z) = 1 + x • -z
Tactic: rw [sub_eq_add_neg, smul_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
x : ℝ
h : 1 + -(x • z) = 1 + x • -z
⊢ 1 - x • z = 1 + x • -z
have h₁ : 1 + -(x • z) = 1 + -(x • z)
Tactic: rw [sub_eq_add_neg, smul_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
⊢ logTaylor 0 = fun (x : ℂ) ↦ 0
have h : ∀ (x : ℂ), logTaylor 0 x = 0
Tactic: funext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
⊢ logTaylor (n + 1) = logTaylor n + fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)
have h : ∀ (x : ℂ),
  logTaylor (n + 1) x =
    HAdd.hAdd (β := (z : ℂ) → ℂ) (logTaylor n) (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)) x
Tactic: funext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
⊢ logTaylor n 0 = 0
have zero : logTaylor 0 0 = 0
Tactic: induction n with
  | zero => simp [logTaylor_zero]
  | succ n ih => simpa [logTaylor_succ, ih] using ne_or_eq n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
zero : logTaylor 0 0 = 0
⊢ logTaylor n 0 = 0
have succ : ∀ (n : ℕ) (ih : logTaylor n 0 = 0), logTaylor (n + 1) 0 = 0
Tactic: induction n with
  | zero => simp [logTaylor_zero]
  | succ n ih => simpa [logTaylor_succ, ih] using ne_or_eq n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
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
have succ : HasDerivAt (logTaylor (n + 1) + fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / (↑(n + 1) : ℂ))
  (∑ j ∈ Finset.range (n + 1), HPow.hPow (α := ℂ) (-1) j * z ^ j) z
Tactic: rw [logTaylor_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / (↑(n + 1) : ℂ))
    (∑ j ∈ Finset.range (n + 1), HPow.hPow (α := ℂ) (-1) j * z ^ j) z
have succ : HasDerivAt
  (logTaylor (n + 1) + fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
  (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j + HPow.hPow (α := ℂ) (-1) n * z ^ n) z
Tactic: simp only [Nat.cast_add, Nat.cast_one,
      Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt
    (logTaylor (n + 1) + fun (z : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
    (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j + HPow.hPow (α := ℂ) (-1) n * z ^ n) z
have succ : HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
  (HPow.hPow (α := ℂ) (-1) n * z ^ n) z
Tactic: refine HasDerivAt.add ih ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
    (HPow.hPow (α := ℂ) (-1) n * z ^ n) z
have succ : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
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
have h : z ^ n = (↑(n + 1) : ℂ) * z ^ (n + 1 - 1) * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹
Tactic: convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * (z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
    (HPow.hPow (α := ℂ) (-1) n * z ^ n) z
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
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 (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * (z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
    (HPow.hPow (α := ℂ) (-1) n * z ^ n) z
have h : HPow.hPow (α := ℂ) (-1) n = HPow.hPow (α := ℂ) (-1) (n + 1 + 1)
Tactic: convert! HasDerivAt.const_mul _ this using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
⊢ HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
have zero : HasDerivAt (logTaylor (HAdd.hAdd (α := ℕ) 0 1)) (∑ j ∈ Finset.range 0, 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
zero : HasDerivAt (logTaylor (HAdd.hAdd (α := ℕ) 0 1)) (∑ j ∈ Finset.range 0, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
have 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
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ HasDerivAt (fun (z : ℂ) ↦ log (1 + z) - logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z
have h : (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j
Tactic: convert! ((hasDerivAt_log hz).comp_const_add 1 z).sub (hasDerivAt_logTaylor n z) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : -z = 1
⊢ False
have H₁ : z = -1
Tactic: rw [neg_eq_iff_eq_neg] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ False
have hz₁ : 0 ∈ slitPlane
Tactic: simp only [H, add_neg_cancel] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j
have hz' : -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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
hz' : -z ≠ 1
⊢ (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - ∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j
have h : (-z) ^ n * (1 + z)⁻¹ = (1 + z)⁻¹ - -(((-z) ^ n - 1) / (1 + z))
Tactic: simp_rw [← mul_pow, neg_one_mul, geom_sum_eq hz', ← neg_add', div_neg, add_comm z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
have rw : ∀ (ht : 0 ≤ t ∧ t ≤ 1) {z : ℂ} (hz : ‖z‖ < 1), ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
Tactic: rw [Set.mem_Icc] at ht
Cleared hypotheses: ht, z, hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + (↑t : ℂ) * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
have rw : ‖1 + (↑t : ℂ) * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹
Tactic: rw [norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 0 < 1 - ‖z‖
have linarith : 1 - ‖z‖ ≤ 0 → ‖z‖ - 1 + (1 - ‖z‖ - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖1 + (↑t : ℂ) * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹
have refine : 1 - ‖z‖ ≤ ‖1 + (↑t : ℂ) * z‖
Tactic: refine inv_anti₀ (by linarith) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ 1 - t * ‖z‖
have nlinarith : 1 - t * ‖z‖ < 1 - ‖z‖ → 1 - t * ‖z‖ - (1 - ‖z‖) + (0 - (t - 1) * (0 - ‖z‖)) = 0
Tactic: nlinarith [norm_nonneg z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ) * z‖
have rw : 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ)‖ * ‖z‖
Tactic: rw [norm_mul, Complex.norm_of_nonneg ht.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
rw : 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ)‖ * ‖z‖
⊢ 1 - t * ‖z‖ = 1 - ‖(↑t : ℂ) * z‖
have rw₁ : 1 - t * ‖z‖ = 1 - t * ‖z‖
Tactic: rw [norm_mul, Complex.norm_of_nonneg ht.1]