awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
refine_1 : s ⊆ s ∪ {0}
⊢ s ⊆ insert 0 (cexp '' cexp ⁻¹' s)

Tactic:
rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.diff_eq, ← Set.union_singleton,
        Set.diff_union_self]

Premises used: Set.diff_eq, Set.diff_union_self, Set.image_preimage_eq_inter_range, Complex.range_exp, Set.union_singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s ∪ {0}

Tactic:
Set.subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s ∪ {0}

Tactic:
exact Set.subset_union_left

Premises used: Set.subset_union_left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
refine_2 : Set.Countable (α := ℂ) (⋃ y ∈ s, cexp ⁻¹' {y})
⊢ (cexp ⁻¹' s).Countable

Tactic:
rw [← Set.biUnion_preimage_singleton]

Premises used: Set.biUnion_preimage_singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
⊢ Set.Countable (α := ℂ) (⋃ y ∈ s, cexp ⁻¹' {y})

Tactic:
hs.biUnion fun z hz => ?_

Premises used: Set.Countable.biUnion
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
refine_2 : ∀ (z : ℂ) (hz : z ∈ s), (cexp ⁻¹' {z}).Countable
⊢ Set.Countable (α := ℂ) (⋃ y ∈ s, cexp ⁻¹' {y})

Tactic:
refine hs.biUnion fun z hz => ?_

Premises used: Set.Countable.biUnion
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
pos : ∀ (h : ∃ (w : ℂ), cexp w = z), (cexp ⁻¹' {z}).Countable
neg : ∀ (h : ∀ (w : ℂ), cexp w ≠ z), (cexp ⁻¹' {z}).Countable
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
by_cases! h : ∃ w, exp w = z
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∃ (w : ℂ), cexp w = z
pos : ∀ (w : ℂ) (hz : cexp w ∈ s), (cexp ⁻¹' {cexp w}).Countable
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
rcases h with ⟨w, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
pos : Set.Countable (α := ℂ) (⋃ (i : ℤ), {x : ℂ | x = w + (↑i : ℂ) * (2 * (↑π : ℂ) * I)})
⊢ (cexp ⁻¹' {cexp w}).Countable

Tactic:
simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.setOf_exists]

Premises used: Complex.exp_eq_exp_iff_exists_int, Set.setOf_exists, Set.mem_singleton_iff, Set.preimage
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ Set.Countable (α := ℂ) (⋃ (i : ℤ), {x : ℂ | x = w + (↑i : ℂ) * (2 * (↑π : ℂ) * I)})

Tactic:
Set.countable_iUnion fun m => Set.countable_singleton _

Premises used: Int.cast, Real.pi, HMul.hMul, Complex.ofReal, Set.countable_iUnion, HAdd.hAdd, Set.countable_singleton, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
w : ℂ
hz : cexp w ∈ s
⊢ Set.Countable (α := ℂ) (⋃ (i : ℤ), {x : ℂ | x = w + (↑i : ℂ) * (2 * (↑π : ℂ) * I)})

Tactic:
exact Set.countable_iUnion fun m => Set.countable_singleton _

Premises used: Set.countable_iUnion, Set.countable_singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∀ (w : ℂ), cexp w ≠ z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
simp [Set.preimage, h]

Premises used: Set.preimage
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto (fun (x : ℂ) ↦ (ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) x + (ofReal ∘ arg) x * I) (𝓝[{z : ℂ | z.im < 0}] z)
    (𝓝 ((ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) z + (↑(-π) : ℂ) * I))

Tactic:
(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)

Premises used: tendsto_const_nhds, Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, Continuous.continuousAt, Continuous.tendsto, Filter.Tendsto.mul, ContinuousWithinAt.log, Complex.continuous_ofReal, Filter.Tendsto.add, ContinuousAt.comp_continuousWithinAt, Filter.Tendsto.comp, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto, continuous_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
h : 𝓝 ((↑(Real.log ‖z‖) : ℂ) - (↑π : ℂ) * I) = 𝓝 ((ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) z + (↑(-π) : ℂ) * I)
convert_1 : ‖z‖ ≠ 0
⊢ Tendsto log (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 ((↑(Real.log ‖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

Premises used: tendsto_const_nhds, Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, Continuous.continuousAt, Continuous.tendsto, Filter.Tendsto.mul, ContinuousWithinAt.log, Complex.continuous_ofReal, Filter.Tendsto.add, ContinuousAt.comp_continuousWithinAt, Filter.Tendsto.comp, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto, continuous_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 ((↑(Real.log ‖z‖) : ℂ) - (↑π : ℂ) * I) = 𝓝 ((ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) z + (↑(-π) : ℂ) * I)

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ z.im = 0

Tactic:
him
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
convert_1 : ∀ (z : ℝ) (hre : (↑z : ℂ).re < 0), ‖(↑z : ℂ)‖ ≠ 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℝ
hre : (↑z : ℂ).re < 0
⊢ ‖(↑z : ℂ)‖ ≠ 0

Tactic:
simpa using hre.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto
    (fun (x : ℂ) ↦ (ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) x + HMul.hMul (β := ℂ → ℂ) (ofReal ∘ arg) (fun (x : ℂ) ↦ I) x)
    (𝓝[{z : ℂ | 0 ≤ z.im}] z)
    (𝓝 ((ofReal ∘ fun (x : ℂ) ↦ Real.log ‖x‖) z + HMul.hMul (β := ℂ → ℂ) (ofReal ∘ arg) (fun (x : ℂ) ↦ I) z))

Tactic:
(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)

Premises used: Complex.continuousWithinAt_arg_of_re_neg_of_im_zero, tendsto_const_nhds, Continuous.continuousAt, ContinuousWithinAt.log, Complex.continuous_ofReal, Filter.Tendsto.add, ContinuousAt.comp_continuousWithinAt, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto, continuous_norm, ContinuousWithinAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
convert_1 : ‖z‖ ≠ 0
⊢ ContinuousWithinAt log {z : ℂ | 0 ≤ z.im} z

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

Premises used: Complex.continuousWithinAt_arg_of_re_neg_of_im_zero, tendsto_const_nhds, Continuous.continuousAt, ContinuousWithinAt.log, Complex.continuous_ofReal, Filter.Tendsto.add, ContinuousAt.comp_continuousWithinAt, Continuous.continuousWithinAt, ContinuousWithinAt.tendsto, continuous_norm, ContinuousWithinAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z : ℂ | 0 ≤ z.im}] z) (𝓝 ((↑(Real.log ‖z‖) : ℂ) + (↑π : ℂ) * I))

Tactic:
simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩] using
    (continuousWithinAt_log_of_re_neg_of_im_zero hre him).tendsto

Premises used: Iff.mpr, Complex.log, Complex.continuousWithinAt_log_of_re_neg_of_im_zero, And.intro, ContinuousWithinAt.tendsto, Complex.arg_eq_pi_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
rw : map cexp (comap cexp (𝓝 0)) = 𝓝[≠] 0
rw₁ : 𝓝 0 ⊓ 𝓟 (range cexp) = 𝓝[≠] 0
rw₂ : Eq (α := Filter ℂ) (𝓝 0 ⊓ 𝓟 {0}ᶜ) (𝓝[≠] 0)
rw₃ rw₄ : Eq (α := Filter ℂ) (𝓝 0 ⊓ 𝓟 {0}ᶜ) (𝓝 0 ⊓ 𝓟 {0}ᶜ)
⊢ map cexp (comap re atBot) = 𝓝[≠] 0

Tactic:
rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]

Premises used: nhdsWithin, Filter.map_comap, Complex.comap_exp_nhds_zero, Complex.range_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
rw : {0}ᶜ ∈ cobounded ℂ
⊢ map cexp (comap re atTop) = cobounded ℂ

Tactic:
rw [← comap_exp_cobounded, map_comap, range_exp, inf_eq_left, le_principal_iff]

Premises used: Complex.comap_exp_cobounded, Filter.le_principal_iff, Filter.map_comap, inf_eq_left, Complex.range_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ {0}ᶜ ∈ cobounded ℂ

Tactic:
eventually_ne_cobounded _

Premises used: Bornology.eventually_ne_cobounded, Set.Mem, Filter.Eventually, setOf, Set.singleton
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ {0}ᶜ ∈ cobounded ℂ

Tactic:
exact eventually_ne_cobounded _

Premises used: Bornology.eventually_ne_cobounded
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt log x

Tactic:
ContinuousAt.add ?_ ?_

Premises used: Complex.log, ContinuousAt.add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
refine_1 : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑(Real.log ‖x‖) : ℂ)) x
refine_2 : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ) * I) x
⊢ ContinuousAt log x

Tactic:
refine ContinuousAt.add ?_ ?_

Premises used: ContinuousAt.add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑(Real.log ‖x‖) : ℂ)) x

Tactic:
continuous_ofReal.continuousAt.comp ?_

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
refine_1 : ContinuousAt (Y := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑(Real.log ‖x‖) : ℂ)) x

Tactic:
refine continuous_ofReal.continuousAt.comp ?_

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt (Y := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) x

Tactic:
(Real.continuousAt_log ?_).comp continuous_norm.continuousAt

Premises used: Real.log, dite, Continuous.continuousAt, ContinuousAt.comp, Real.continuousAt_log, continuous_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
refine_1 : ‖x‖ ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) x

Tactic:
refine (Real.continuousAt_log ?_).comp continuous_norm.continuousAt

Premises used: Continuous.continuousAt, ContinuousAt.comp, Real.continuousAt_log, continuous_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Tactic:
norm_ne_zero_iff.mpr <| slitPlane_ne_zero h

Premises used: Iff.mpr, norm_ne_zero_iff, Complex.slitPlane_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Tactic:
exact norm_ne_zero_iff.mpr <| slitPlane_ne_zero h

Premises used: Iff.mpr, norm_ne_zero_iff, Complex.slitPlane_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I

Tactic:
have h_cont_mul : Continuous fun x : ℂ => x * I := by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ) * I) x

Tactic:
h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I
refine_2 : ContinuousAt arg x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ (↑x.arg : ℂ) * I) x

Tactic:
refine h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp ?_)

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I
⊢ ContinuousAt arg x

Tactic:
continuousAt_arg h

Premises used: Complex.continuousAt_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x ∈ slitPlane
h_cont_mul : Continuous (Y := ℂ) fun (x : ℂ) ↦ x * I
⊢ ContinuousAt arg x

Tactic:
exact continuousAt_arg h

Premises used: Complex.continuousAt_arg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
x : ℂ
h : Tendsto f l (𝓝 x)
hx : x ∈ slitPlane
⊢ Tendsto (fun (t : α) ↦ log (f t)) l (𝓝 (log x))

Tactic:
(continuousAt_clog hx).tendsto.comp h

Premises used: Complex.log, continuousAt_clog, ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
x : α
h₁ : ContinuousAt f x
h₂ : f x ∈ slitPlane
⊢ ContinuousAt (Y := ℂ) (fun (t : α) ↦ log (f t)) x

Tactic:
h₁.clog h₂

Premises used: ContinuousAt, Filter.Tendsto.clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
s : Set α
x : α
h₁ : ContinuousWithinAt f s x
h₂ : f x ∈ slitPlane
⊢ ContinuousWithinAt (Y := ℂ) (fun (t : α) ↦ log (f t)) s x

Tactic:
h₁.clog h₂

Premises used: ContinuousWithinAt, Filter.Tendsto.clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
s : Set α
h₁ : ContinuousOn f s
h₂ : ∀ x ∈ s, f x ∈ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (t : α) ↦ log (f t)) s

Tactic:
fun x hx =>
  (h₁ x hx).clog (h₂ x hx)

Premises used: ContinuousOn, ContinuousWithinAt.clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
h₁ : Continuous[inst, _] f
h₂ : ∀ (x : α), f x ∈ slitPlane
⊢ Continuous[inst, _] fun (t : α) ↦ log (f t)

Tactic:
continuous_iff_continuousAt.2 fun x => h₁.continuousAt.clog (h₂ x)

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.clog, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℝ
h₁ : -π < y
h₂ : y < π
⊢ y ≤ -π + 2 * π

Tactic:
simpa [two_mul] using h₂.le

Premises used: two_mul, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℝ
h₁ : -π < y
h₂ : y < π
⊢ cexp { re := x, im := y : ℂ } ∈ slitPlane

Tactic:
simp [exp_mem_slitPlane, h₂.ne,
      (toIocMod_eq_self Real.two_pi_pos).mpr ⟨h₁, by simpa [two_mul] using h₂.le⟩]

Premises used: Iff.mpr, toIocMod_eq_self, Real.two_pi_pos, And.intro, Complex.exp_mem_slitPlane, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
h : z ∈ slitPlane
simp : 0 ≤ z.re ∨ z.im ≠ 0
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | z.im ∈ Ioo (-π) π} (log z)

Tactic:
simp only [mem_setOf, log_im, mem_Ioo, neg_pi_lt_arg, arg_lt_pi_iff, true_and]

Premises used: Set.mem_Ioo, Complex.neg_pi_lt_arg, Complex.arg_lt_pi_iff, Set.mem_setOf, Complex.log_im, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
h : z ∈ slitPlane
⊢ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
h.imp_left le_of_lt

Premises used: Or.imp_left, le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
h : z ∈ slitPlane
⊢ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
exact h.imp_left le_of_lt

Premises used: Or.imp_left, le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ ContinuousOn cexp {z : ℂ | z.im ∈ Ioo (-π) π}

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ 1 + t • z) (Set.Icc 0 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ log (1 + z) - log 1 = HSMul.hSMul (β := ℂ) z (∫ (t : ℝ) in 0..1, (1 + t • z)⁻¹)

Tactic:
(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

Premises used: StarConvex.add_smul_mem, Complex.starConvex_one_slitPlane, And.right, And.left, Eq.symm, intervalIntegral.integral_unitInterval_deriv_eq_sub, Complex.hasDerivAt_log, Complex.continuousOn_one_add_mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + z ∈ slitPlane
h : log (1 + z) = log (1 + z) - log 1
⊢ log (1 + z) = z * ∫ (t : ℝ) in 0..1, (1 + t • z)⁻¹

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

Premises used: StarConvex.add_smul_mem, Complex.starConvex_one_slitPlane, And.right, And.left, Eq.symm, intervalIntegral.integral_unitInterval_deriv_eq_sub, Complex.hasDerivAt_log, Complex.continuousOn_one_add_mul_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ log (1 + z) = log (1 + z) - log 1

Tactic:
simp only [log_one, sub_zero]

Premises used: Complex.log_one, sub_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 - z ∈ slitPlane
⊢ 1 + -z ∈ slitPlane

Tactic:
rw [sub_eq_add_neg 1 z] at hz ⊢

Premises used: sub_eq_add_neg, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
rw : log (1 + -z) = -z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹
⊢ 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]

Premises used: Complex.log_inv, neg_eq_iff_eq_neg, Complex.slitPlane_arg_ne_pi, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z) = -z * ∫ (t : ℝ) in 0..1, (1 + t • -z)⁻¹

Tactic:
log_eq_integral hz

Premises used: Complex.log_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
h : ∀ (x : ℝ), 1 - x • z = 1 + x • -z
⊢ log (1 + -z) = -z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹

Tactic:
convert! log_eq_integral hz using 5

Premises used: Complex.log_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
hz : 1 + -z ∈ slitPlane
x : ℝ
h : 1 + -(x • z) = 1 + x • -z
h₁ h₂ : 1 + -(x • z) = 1 + -(x • z)
⊢ 1 - x • z = 1 + x • -z

Tactic:
rw [sub_eq_add_neg, smul_neg]

Premises used: sub_eq_add_neg, smul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
h : ∀ (x : ℂ), logTaylor 0 x = 0
⊢ logTaylor 0 = fun (x : ℂ) ↦ 0

Tactic:
funext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
x : ℂ
⊢ logTaylor 0 x = 0

Tactic:
simp only [logTaylor, Finset.range_zero,
    Finset.sum_empty]

Premises used: Finset.sum_empty, Finset.range_zero, Complex.logTaylor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
h :
  ∀ (x : ℂ),
    logTaylor (n + 1) x =
      HAdd.hAdd (β := (z : ℂ) → ℂ) (logTaylor n) (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)) x
⊢ logTaylor (n + 1) = logTaylor n + fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)

Tactic:
funext
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
x : ℂ
⊢ logTaylor (n + 1) x =
    HAdd.hAdd (β := (z : ℂ) → ℂ) (logTaylor n) (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1) * z ^ n / (↑n : ℂ)) x

Tactic:
simpa only [logTaylor] using Finset.sum_range_succ ..

Premises used: Finset.sum_range_succ, Complex.logTaylor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
⊢ logTaylor 0 0 = 0

Tactic:
simp [logTaylor_zero]

Premises used: Complex.logTaylor_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
ih : logTaylor n 0 = 0
⊢ logTaylor (n + 1) 0 = 0

Tactic:
simpa [logTaylor_succ, ih] using ne_or_eq n 0

Premises used: ne_or_eq, OfNat.ofNat, Complex.logTaylor_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
n : ℕ
zero : logTaylor 0 0 = 0
succ : ∀ (n : ℕ) (ih : logTaylor n 0 = 0), logTaylor (n + 1) 0 = 0
⊢ logTaylor n 0 = 0

Tactic:
induction n with
  | zero => simp [logTaylor_zero]
  | succ n ih => simpa [logTaylor_succ, ih] using ne_or_eq n 0

Premises used: ne_or_eq, Complex.logTaylor_zero, OfNat.ofNat, Complex.logTaylor_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
⊢ HasDerivAt (logTaylor (HAdd.hAdd (α := ℕ) 0 1)) (∑ j ∈ Finset.range 0, HPow.hPow (α := ℂ) (-1) j * z ^ j) z

Tactic:
simp [logTaylor_succ, logTaylor_zero, Pi.add_def, hasDerivAt_const]

Premises used: hasDerivAt_const, Pi.add_def, Complex.logTaylor_zero, Complex.logTaylor_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
succ :
  HasDerivAt (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
⊢ HasDerivAt (logTaylor (n + 1 + 1)) (∑ j ∈ Finset.range (n + 1), HPow.hPow (α := ℂ) (-1) j * z ^ j) z

Tactic:
rw [logTaylor_succ]

Premises used: Complex.logTaylor_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
succ :
  HasDerivAt
    (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
⊢ 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:
simp only [Nat.cast_add, Nat.cast_one,
      Finset.sum_range_succ]

Premises used: Nat.cast_add, Nat.cast_one, Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
⊢ HasDerivAt
    (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:
HasDerivAt.add ih ?_

Premises used: HasDerivAt.add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
Goal:
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, HPow.hPow (α := ℂ) (-1) j * z ^ j) z
succ :
  HasDerivAt (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) (-1) (n + 1 + 1) * z ^ (n + 1) / HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
    (HPow.hPow (α := ℂ) (-1) n * z ^ n) z
⊢ HasDerivAt
    (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:
refine HasDerivAt.add ih ?_

Premises used: HasDerivAt.add