awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : (↑n : ℝ) * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
h : (↑n : ℝ) * ‖Real.log |z.im|‖ ≤ ‖z.re‖
h₂ : (↑n : ℝ) * |Real.log |z.im|| ≤ ‖z.re‖
h₃ : (↑n : ℝ) * |Real.log |z.im|| ≤ |z.re|
h₄ : (↑n : ℝ) * Real.log |z.im| ≤ |z.re|
h₅ : Real.log (|z.im| ^ n) ≤ |z.re|
h₆ : |z.im| ^ n ≤ Real.exp |z.re|
h₇ h₈ h₉ h₁₀ : |z.im| ^ n ≤ Real.exp z.re
⊢ (↑n : ℝ) * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖

Tactic:
rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H),
              ← Real.log_pow, Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),
              abs_of_pos (one_pos.trans h₁)]

Premises used: pow_pos, Real.log_pos, Real.log_le_iff_le_exp, max_eq_right, LT.lt.trans, Real.log_pow, abs_of_pos, one_pos, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a z : ℂ
hz : z ≠ 0
⊢ Eq (α := ℝ) ((fun (z : ℂ) ↦ ‖z‖ ^ a.re) z) ((fun (z : ℂ) ↦ Real.exp (a.re * Real.log ‖z‖)) z)

Tactic:
simp
        [Real.rpow_def_of_pos, norm_pos_iff.mpr hz, mul_comm]

Premises used: Iff.mpr, norm_pos_iff, Real.rpow_def_of_pos, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ b * x.re - a.re * Real.log ‖x‖) l atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (z : ℂ) ↦ Real.exp (a.re * Real.log ‖z‖)) fun (x : ℂ) ↦ ‖cexp ((↑b : ℂ) * x)‖

Tactic:
simp only [norm_exp, re_ofReal_mul, Real.isLittleO_exp_comp_exp_comp]

Premises used: Real.isLittleO_exp_comp_exp_comp, Complex.norm_exp, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ b * x.re - a.re * Real.log ‖x‖) l atTop

Tactic:
(IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop
          (hl.tendsto_re.const_mul_atTop hb)

Premises used: Filter.Tendsto.const_mul_atTop, Complex.IsExpCmpFilter.tendsto_re, Asymptotics.IsEquivalent.tendsto_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
refine : IsLittleO (E := ℝ) (F := ℝ) l (fun (x : ℂ) ↦ a.re * Real.log ‖x‖) fun (x : ℂ) ↦ b * x.re
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ b * x.re - a.re * Real.log ‖x‖) l atTop

Tactic:
refine (IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop
          (hl.tendsto_re.const_mul_atTop hb)

Premises used: Filter.Tendsto.const_mul_atTop, Complex.IsExpCmpFilter.tendsto_re, Asymptotics.IsEquivalent.tendsto_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : ℂ) ↦ a.re * Real.log ‖x‖) fun (x : ℂ) ↦ b * x.re

Tactic:
(hl.isLittleO_log_norm_re.const_mul_left _).const_mul_right hb.ne'

Premises used: Asymptotics.IsLittleO.const_mul_left, LT.lt.ne', Complex.IsExpCmpFilter.isLittleO_log_norm_re, Asymptotics.IsLittleO.const_mul_right
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : ℂ) ↦ a.re * Real.log ‖x‖) fun (x : ℂ) ↦ b * x.re

Tactic:
exact (hl.isLittleO_log_norm_re.const_mul_left _).const_mul_right hb.ne'

Premises used: Asymptotics.IsLittleO.const_mul_left, LT.lt.ne', Complex.IsExpCmpFilter.isLittleO_log_norm_re, Asymptotics.IsLittleO.const_mul_right
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
rw : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * z ^ (a₁ - a₂) * cexp ((↑b₁ : ℂ) * z)
rw₁ : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ (a₂ + (a₁ - a₂)) * cexp ((↑b₁ : ℂ) * z)
rw₂ rw₃ : z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₁ * cexp ((↑b₁ : ℂ) * z)
⊢ z ^ a₁ * cexp ((↑b₁ : ℂ) * z) = z ^ a₂ * cexp ((↑b₁ : ℂ) * z) * z ^ (a₁ - a₂)

Tactic:
rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel]

Premises used: add_sub_cancel, mul_right_comm, Complex.cpow_add
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
simp : l.EventuallyEq (β := ℂ) (fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₂ : ℂ) * z)) fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₂ : ℂ) * z)
⊢ l.EventuallyEq (β := ℂ) (fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₁ : ℂ) * z) * cexp ((↑(b₂ - b₁) : ℂ) * z)) fun (z : ℂ) ↦
    z ^ a₂ * cexp ((↑b₂ : ℂ) * z)

Tactic:
simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel]

Premises used: Complex.exp_add, mul_assoc, sub_mul, add_sub_cancel, Complex.ofReal_sub
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ l.EventuallyEq (β := ℂ) (fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₂ : ℂ) * z)) fun (z : ℂ) ↦ z ^ a₂ * cexp ((↑b₂ : ℂ) * z)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : b < 0
⊢ IsLittleO (E := ℂ) (F := ℂ) l (fun (z : ℂ) ↦ cexp ((↑b : ℂ) * z)) fun (z : ℂ) ↦ z ^ a

Tactic:
simpa using hl.isLittleO_cpow_mul_exp hb 0 a

Premises used: OfNat.ofNat, Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℕ
⊢ IsLittleO (E := ℂ) (F := ℂ) l (fun (z : ℂ) ↦ z ^ m * cexp ((↑b₁ : ℂ) * z)) fun (z : ℂ) ↦ z ^ n * cexp ((↑b₂ : ℂ) * z)

Tactic:
simpa only [cpow_natCast] using hl.isLittleO_cpow_mul_exp hb m n

Premises used: Nat.cast, Complex.cpow_natCast, Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp
-- Module: Mathlib.Analysis.SpecialFunctions.CompareExp
Goal:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℤ
⊢ IsLittleO (E := ℂ) (F := ℂ) l (fun (z : ℂ) ↦ z ^ m * cexp ((↑b₁ : ℂ) * z)) fun (z : ℂ) ↦ z ^ n * cexp ((↑b₂ : ℂ) * z)

Tactic:
simpa only [cpow_intCast] using hl.isLittleO_cpow_mul_exp hb m n

Premises used: Complex.cpow_intCast, Int.cast, Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
z : ℂ
m : z ∈ slitPlane
rw : ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z
⊢ AnalyticAt ℂ log z

Tactic:
rw [analyticAt_iff_eventually_differentiableAt]

Premises used: Complex.analyticAt_iff_eventually_differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
z : ℂ
m : z ∈ slitPlane
h : ∀ a ∈ slitPlane, DifferentiableAt ℂ log a
⊢ ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z

Tactic:
filter_upwards [isOpen_slitPlane.eventually_mem m]

Premises used: Complex.isOpen_slitPlane, IsOpen.eventually_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
z_1 : ℂ
m_1 : z_1 ∈ slitPlane
z : ℂ
m : z ∈ slitPlane
⊢ DifferentiableAt ℂ log z

Tactic:
differentiableAt_id.clog m

Premises used: DifferentiableAt.clog, differentiableAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
z_1 : ℂ
m_1 : z_1 ∈ slitPlane
z : ℂ
m : z ∈ slitPlane
⊢ DifferentiableAt ℂ log z

Tactic:
exact differentiableAt_id.clog m

Premises used: DifferentiableAt.clog, differentiableAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
fa : AnalyticAt ℂ f x
m : f x ∈ slitPlane
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : E) ↦ log (f z)) x

Tactic:
(analyticAt_clog m).comp fa

Premises used: Complex.log, analyticAt_clog, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ log (f z)) s x

Tactic:
(analyticAt_clog m).comp_analyticWithinAt fa

Premises used: AnalyticAt.comp_analyticWithinAt, Complex.log, analyticAt_clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
fs : AnalyticOnNhd ℂ f s
m : ∀ z ∈ s, f z ∈ slitPlane
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : E) ↦ log (f z)) s

Tactic:
fun z n ↦ (analyticAt_clog (m z n)).comp (fs z n)

Premises used: Complex.log, AnalyticOnNhd, analyticAt_clog, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
fs : AnalyticOn ℂ f s
m : ∀ z ∈ s, f z ∈ slitPlane
⊢ AnalyticOn ℂ (F := ℂ) (fun (z : E) ↦ log (f z)) s

Tactic:
fun z n ↦ (analyticAt_clog (m z n)).analyticWithinAt.comp (fs z n) m

Premises used: Complex.log, AnalyticOn, AnalyticAt.analyticWithinAt, analyticAt_clog, AnalyticWithinAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
h : ∀ (a : E), f a ≠ 0 → f a ^ g a = cexp (log (f a) * g a)
⊢ (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)

Tactic:
filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]

Premises used: Filter.Tendsto.eventually_ne, AnalyticWithinAt.continuousWithinAt_insert, Complex.slitPlane_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
z : E
fz : f z ≠ 0
⊢ f z ^ g z = cexp (log (f z) * g z)

Tactic:
simp only [fz, cpow_def, if_false]

Premises used: if_false, Complex.cpow_def
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
⊢ (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)

Tactic:
have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ exp (log (f z) * g z) := by
    filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))]
    intro z fz
    simp only [fz, cpow_def, if_false]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)
apply : AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ cexp (log (f z) * g z)) s x
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) s x

Tactic:
apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e

Premises used: AnalyticWithinAt.congr_of_eventuallyEq_insert
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ cexp (log (f z) * g z)) s x

Tactic:
((fa.clog m).mul ga).cexp

Premises used: AnalyticWithinAt.cexp, AnalyticWithinAt.clog, AnalyticWithinAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
fa : AnalyticWithinAt ℂ f s x
ga : AnalyticWithinAt ℂ g s x
m : f x ∈ slitPlane
e : (𝓝[insert x s] x).EventuallyEq (β := ℂ) (fun (z : E) ↦ f z ^ g z) fun (z : E) ↦ cexp (log (f z) * g z)
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ cexp (log (f z) * g z)) s x

Tactic:
exact ((fa.clog m).mul ga).cexp

Premises used: AnalyticWithinAt.cexp, AnalyticWithinAt.clog, AnalyticWithinAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticAt ℂ f x
ga : AnalyticAt ℂ g x
m : f x ∈ slitPlane
rw :
  ∀ (fa : AnalyticWithinAt ℂ f univ x) (ga : AnalyticWithinAt ℂ g univ x) (m : f x ∈ slitPlane),
    AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) univ x
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) x

Tactic:
rw [← analyticWithinAt_univ] at fa ga ⊢

Premises used: analyticWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticWithinAt ℂ f univ x
ga : AnalyticWithinAt ℂ g univ x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) univ x

Tactic:
fa.cpow ga m

Premises used: AnalyticWithinAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
fa : AnalyticWithinAt ℂ f univ x
ga : AnalyticWithinAt ℂ g univ x
m : f x ∈ slitPlane
⊢ AnalyticWithinAt ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) univ x

Tactic:
exact fa.cpow ga m

Premises used: AnalyticWithinAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
s : Set E
fs : AnalyticOn ℂ f s
gs : AnalyticOn ℂ g s
m : ∀ z ∈ s, f z ∈ slitPlane
⊢ AnalyticOn ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) s

Tactic:
fun z n ↦ (fs z n).cpow (gs z n) (m z n)

Premises used: AnalyticOn, AnalyticWithinAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
s : Set E
fs : AnalyticOnNhd ℂ f s
gs : AnalyticOnNhd ℂ g s
m : ∀ z ∈ s, f z ∈ slitPlane
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : E) ↦ f z ^ g z) s

Tactic:
fun z n ↦ (fs z n).cpow (gs z n) (m z n)

Premises used: AnalyticOnNhd, AnalyticAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
x : ℝ
hf : AnalyticAt ℂ f (↑x : ℂ)
⊢ AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).re) x

Tactic:
(Complex.reCLM.analyticAt _).comp (hf.restrictScalars.comp (Complex.ofRealCLM.analyticAt _))

Premises used: ContinuousLinearMap.analyticAt, Complex.ofRealCLM, AnalyticAt.restrictScalars, Complex.reCLM, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
x : ℝ
hf : AnalyticAt ℂ f (↑x : ℂ)
⊢ AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).im) x

Tactic:
(Complex.imCLM.analyticAt _).comp (hf.restrictScalars.comp (Complex.ofRealCLM.analyticAt _))

Premises used: ContinuousLinearMap.analyticAt, Complex.ofRealCLM, AnalyticAt.restrictScalars, AnalyticAt.comp, Complex.imCLM
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
s : Set ℝ
x : ℝ
hf : AnalyticWithinAt ℂ f (ofReal '' s) (↑x : ℂ)
⊢ AnalyticWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).re) s x

Tactic:
((Complex.reCLM.analyticWithinAt _ _).comp hf.restrictScalars (mapsTo_image f _)).comp
    (Complex.ofRealCLM.analyticWithinAt _ _) (mapsTo_image ofReal s)

Premises used: ContinuousLinearMap.analyticWithinAt, AnalyticWithinAt.restrictScalars, Set.mapsTo_image, Complex.ofRealCLM, Complex.ofReal, Complex.reCLM, AnalyticWithinAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
s : Set ℝ
x : ℝ
hf : AnalyticWithinAt ℂ f (ofReal '' s) (↑x : ℂ)
⊢ AnalyticWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).im) s x

Tactic:
((Complex.imCLM.analyticWithinAt _ _).comp hf.restrictScalars (mapsTo_image f _)).comp
    (Complex.ofRealCLM.analyticWithinAt _ _) (mapsTo_image ofReal s)

Premises used: ContinuousLinearMap.analyticWithinAt, AnalyticWithinAt.restrictScalars, Set.mapsTo_image, Complex.ofRealCLM, Complex.ofReal, AnalyticWithinAt.comp, Complex.imCLM
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
s : Set ℝ
hf : AnalyticOn ℂ f (ofReal '' s)
⊢ AnalyticOn ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).re) s

Tactic:
((Complex.reCLM.analyticOn _).comp hf.restrictScalars (mapsTo_image f _)).comp
    (Complex.ofRealCLM.analyticOn _) (mapsTo_image ofReal s)

Premises used: Set.mapsTo_image, Complex.ofRealCLM, Complex.ofReal, AnalyticOn.restrictScalars, ContinuousLinearMap.analyticOn, AnalyticOn.comp, Complex.reCLM
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
s : Set ℝ
hf : AnalyticOn ℂ f (ofReal '' s)
⊢ AnalyticOn ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).im) s

Tactic:
((Complex.imCLM.analyticOn _).comp hf.restrictScalars (mapsTo_image f _)).comp
    (Complex.ofRealCLM.analyticOn _) (mapsTo_image ofReal s)

Premises used: Set.mapsTo_image, Complex.ofRealCLM, Complex.ofReal, AnalyticOn.restrictScalars, ContinuousLinearMap.analyticOn, AnalyticOn.comp, Complex.imCLM
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
s : Set ℝ
hf : AnalyticOnNhd ℂ f (ofReal '' s)
⊢ AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).re) s

Tactic:
((Complex.reCLM.analyticOnNhd _).comp hf.restrictScalars (mapsTo_image f _)).comp
    (Complex.ofRealCLM.analyticOnNhd _) (mapsTo_image ofReal s)

Premises used: Set.mapsTo_image, Complex.ofRealCLM, Complex.ofReal, AnalyticOnNhd.comp, Complex.reCLM, AnalyticOnNhd.restrictScalars, ContinuousLinearMap.analyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℂ → ℂ
s : Set ℝ
hf : AnalyticOnNhd ℂ f (ofReal '' s)
⊢ AnalyticOnNhd ℝ (F := ℝ) (fun (x : ℝ) ↦ (f (↑x : ℂ)).im) s

Tactic:
((Complex.imCLM.analyticOnNhd _).comp hf.restrictScalars (mapsTo_image f _)).comp
    (Complex.ofRealCLM.analyticOnNhd _) (mapsTo_image ofReal s)

Premises used: Set.mapsTo_image, Complex.ofRealCLM, Complex.ofReal, AnalyticOnNhd.comp, AnalyticOnNhd.restrictScalars, ContinuousLinearMap.analyticOnNhd, Complex.imCLM
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x : ℝ
hx : 0 < x
h : ∀ (x : ℝ), Real.log x = (log (↑x : ℂ)).re
⊢ Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x_1 : ℝ
hx : 0 < x_1
x : ℝ
⊢ Real.log x = (log (↑x : ℂ)).re

Tactic:
(Complex.log_ofReal_re x).symm

Premises used: Eq.symm, Complex.log_ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x_1 : ℝ
hx : 0 < x_1
x : ℝ
⊢ Real.log x = (log (↑x : ℂ)).re

Tactic:
exact (Complex.log_ofReal_re x).symm

Premises used: Eq.symm, Complex.log_ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x : ℝ
hx : 0 < x
⊢ Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re

Tactic:
have : Real.log = fun x : ℝ ↦ (Complex.log x).re := by ext x; exact (Complex.log_ofReal_re x).symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x : ℝ
hx : 0 < x
this : Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
rw : AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (log (↑x : ℂ)).re) x
⊢ AnalyticAt ℝ Real.log x

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x : ℝ
hx : 0 < x
this : Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
⊢ AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (log (↑x : ℂ)).re) x

Tactic:
AnalyticAt.re_ofReal <| analyticAt_clog ?_

Premises used: AnalyticAt.re_ofReal, analyticAt_clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x : ℝ
hx : 0 < x
this : Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
refine : (↑x : ℂ) ∈ slitPlane
⊢ AnalyticAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (log (↑x : ℂ)).re) x

Tactic:
refine AnalyticAt.re_ofReal <| analyticAt_clog ?_

Premises used: AnalyticAt.re_ofReal, analyticAt_clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
x : ℝ
hx : 0 < x
this : Real.log = fun (x : ℝ) ↦ (log (↑x : ℂ)).re
⊢ (↑x : ℂ) ∈ slitPlane

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
⊢ AnalyticOnNhd ℝ Real.log (Ioi 0)

Tactic:
fun _ hx ↦ analyticAt_log hx

Premises used: AnalyticOnNhd, analyticAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
⊢ AnalyticOn ℝ Real.log (Ioi 0)

Tactic:
analyticOnNhd_log.analyticOn

Premises used: analyticOnNhd_log, AnalyticOnNhd.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℝ → ℝ
x : ℝ
fa : AnalyticAt ℝ f x
m : 0 < f x
⊢ AnalyticAt ℝ (F := ℝ) (fun (z : ℝ) ↦ Real.log (f z)) x

Tactic:
(analyticAt_log m).comp fa

Premises used: Real.log, dite, analyticAt_log, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℝ → ℝ
s : Set ℝ
x : ℝ
fa : AnalyticWithinAt ℝ f s x
m : 0 < f x
⊢ AnalyticWithinAt ℝ (F := ℝ) (fun (z : ℝ) ↦ Real.log (f z)) s x

Tactic:
(analyticAt_log m).comp_analyticWithinAt fa

Premises used: AnalyticAt.comp_analyticWithinAt, Real.log, dite, analyticAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℝ → ℝ
s : Set ℝ
fs : AnalyticOnNhd ℝ f s
m : ∀ x ∈ s, 0 < f x
⊢ AnalyticOnNhd ℝ (F := ℝ) (fun (z : ℝ) ↦ Real.log (f z)) s

Tactic:
fun z n ↦ (analyticAt_log (m z n)).comp (fs z n)

Premises used: AnalyticOnNhd, Real.log, dite, analyticAt_log, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Analytic
Goal:
f : ℝ → ℝ
s : Set ℝ
fs : AnalyticOn ℝ f s
m : ∀ x ∈ s, 0 < f x
⊢ AnalyticOn ℝ (F := ℝ) (fun (z : ℝ) ↦ Real.log (f z)) s

Tactic:
fun z n ↦ (analyticAt_log (m z n)).analyticWithinAt.comp (fs z n) m

Premises used: AnalyticOn, Real.log, dite, AnalyticAt.analyticWithinAt, analyticAt_log, AnalyticWithinAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
rw : (1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
⊢ (cexp (-z.arctan * I) - cexp (z.arctan * I)) * I / 2 / ((cexp (z.arctan * I) + cexp (-z.arctan * I)) / 2) = z

Tactic:
rw [div_div_eq_mul_div, div_mul_cancel₀ _ two_ne_zero, ← div_mul_eq_mul_div,
    -- multiply top and bottom by `exp (arctan z * I)`
    ← mul_div_mul_right _ _ (exp_ne_zero (arctan z * I)), sub_mul, add_mul,
    ← exp_add, neg_mul, neg_add_cancel, exp_zero, ← exp_add, ← two_mul]

Premises used: add_mul, mul_div_mul_right, div_mul_cancel₀, HMul.hMul, Complex.exp_ne_zero, Complex.exp_add, Complex.exp_zero, div_div_eq_mul_div, two_mul, div_mul_eq_mul_div, Complex.arctan, sub_mul, two_ne_zero, neg_add_cancel, neg_mul, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
contrapose : ∀ (h₁ : 1 + z * I = 0), z = I
⊢ 1 + z * I ≠ 0

Tactic:
contrapose h₁
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₂ : z ≠ -I
h₁ : 1 + z * I = 0
⊢ I = z

Tactic:
rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁

Premises used: neg_one_mul, neg_neg, Complex.I_ne_zero, div_eq_iff, add_eq_zero_iff_neg_eq, Complex.div_I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₂ : z ≠ -I
h₁ : I = z
⊢ z = I

Tactic:
h₁.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₂ : z ≠ -I
h₁ : I = z
⊢ z = I

Tactic:
exact h₁.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ 1 + z * I ≠ 0

Tactic:
have z₁ : 1 + z * I ≠ 0 := by
    contrapose h₁
    rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁
    exact h₁.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
contrapose : ∀ (h₂ : 1 - z * I = 0), z = -I
⊢ 1 - z * I ≠ 0

Tactic:
contrapose h₂
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : 1 - z * I = 0
⊢ -I = z

Tactic:
rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂

Premises used: sub_eq_zero, Complex.I_ne_zero, div_eq_iff, Complex.div_I, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : -I = z
⊢ z = -I

Tactic:
h₂.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan
Goal:
z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : -I = z
⊢ z = -I

Tactic:
exact h₂.symm

Premises used: Eq.symm