awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
have refine : 0 ∈ closure (Ioi 0 ×ℂ Ioi 0)
Tactic: refine (hd.continuousOn _ ?_).mono subset_closure
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ IsBigO (F := ℝ) (comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
    expR (max B 0 * expR (c * |z.re|))
have hc₁ : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
Tactic: have hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0 := by
        refine (hd.continuousOn _ ?_).mono subset_closure
        simp [closure_reProdIm, mem_reProdIm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc_1 : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
⊢ IsBigO (F := ℝ) (comap re atBot ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))) (f ∘ cexp) fun (z : ℂ) ↦
    expR (max B 0 * expR (c * |z.re|))
have inr : ∀ (w : ℂ), norm (E := ℝ) 1 ≤ ‖expR (max B 0 * expR (c * |w.re|))‖
Tactic: refine ((hc.tendsto.comp <| tendsto_exp_comap_re_atBot.inf H.tendsto).isBigO_one ℝ).trans
        (isBigO_of_le _ fun w => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc_1 : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hc : ContinuousWithinAt f (Ioi 0 ×ℂ Ioi 0) 0
w : ℂ
⊢ norm (E := ℝ) 1 ≤ ‖expR (max B 0 * expR (c * |w.re|))‖
have inr : 0 ≤ max B 0 * expR (c * |w.re|)
Tactic: rw [norm_one, Real.norm_of_nonneg (Real.exp_pos _).le, Real.one_le_exp_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ (comap re atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))).EventuallyLE (β := ℝ)
    (fun (x : ℂ) ↦ norm (E := ℝ) (((fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)) ∘ cexp) x)) fun (z : ℂ) ↦
    expR (max B 0 * expR (c * |z.re|))
have inr : ∀ᶠ (b : ℝ) in atTop, ∀ (a : ℂ), a.re = b → a ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (a.re * c) ≤ max B 0 * expR (c * |a.re|)
Tactic: simp only [EventuallyLE, eventually_inf_principal, eventually_comap, comp_apply,
        Real.norm_of_nonneg (Real.exp_pos _).le, norm_exp, ← Real.exp_mul, Real.exp_le_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∀ᶠ (b : ℝ) in atTop,
    ∀ (a : ℂ), a.re = b → a ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (a.re * c) ≤ max B 0 * expR (c * |a.re|)
have h : ∀ (x : ℝ) (hx : 0 ≤ x) (z : ℂ) (hz : z.re = x),
  z ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)
Tactic: filter_upwards [eventually_ge_atTop 0] with x hx z hz _
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
h : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)
have h : B * expR (c * x) ≤ max B 0 * expR (c * x)
Tactic: rw [hz, abs_of_nonneg hx, mul_comm _ c]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
h : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ B * expR (c * x) ≤ max B 0 * expR (c * x)
have h : B ≤ max B 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ_1 : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = 0
⊢ ‖(f ∘ cexp) ζ‖ ≤ C
have inr : ∀ (ζ : ℝ), ‖(f ∘ cexp) (↑ζ : ℂ)‖ ≤ C
Tactic: lift ζ to ℝ using hζ
Cleared hypotheses: ζ, hζ
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℝ
⊢ ‖(f ∘ cexp) (↑ζ : ℂ)‖ ≤ C
have inr : ‖f (↑(expR ζ) : ℂ)‖ ≤ C
Tactic: rw [comp_apply, ← ofReal_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
ζ_1 : ℂ
hζ_1 : ζ_1.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ_1).re
hz_im : 0 ≤ (cexp ζ_1).im
hzne : cexp ζ_1 ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖(f ∘ cexp) ζ‖ ≤ C
have inr : ‖f ((↑(expR ζ.re) : ℂ) * I)‖ ≤ C
Tactic: rw [← re_add_im ζ, hζ, comp_apply, exp_add_mul_I, ← ofReal_cos, ← ofReal_sin,
      Real.cos_pi_div_two, Real.sin_pi_div_two, ofReal_zero, ofReal_one, one_mul, zero_add, ←
      ofReal_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ‖f z‖ ≤ C
have obtain : ∀ (z : ℂ) (hz_re : (z * I).re ≤ 0) (hz_im : 0 ≤ (z * I).im), ‖f (z * I)‖ ≤ C
Tactic: obtain ⟨z, rfl⟩ : ∃ z', z' * I = z := ⟨z / I, div_mul_cancel₀ _ I_ne_zero⟩
Cleared hypotheses: z, hz_re, hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
⊢ ‖f (z * I)‖ ≤ C
have hz_re₁ : 0 ≤ z.im
Tactic: simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im
Cleared hypotheses: hz_re, hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : (z * I).re ≤ 0
hz_im : 0 ≤ (z * I).im
hz_re₁ : 0 ≤ z.im
⊢ ‖f (z * I)‖ ≤ C
have hz_im₁ : 0 ≤ z.re
Tactic: simp only [mul_I_re, mul_I_im, neg_nonpos] at hz_re hz_im
Cleared hypotheses: hz_re, hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
⊢ ‖f (z * I)‖ ≤ C
have change : ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
Tactic: change ‖(f ∘ (· * I)) z‖ ≤ C
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
have H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
Tactic: have H : MapsTo (· * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using hw.symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
have rcases : ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
  (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
  ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
Tactic: rcases hB with ⟨c, hc, B, hO⟩
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
have refine_1 : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ fun (x : ℂ) ↦ x * I) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him
    (fun x hx => ?_) hz_im hz_re
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_1 : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ fun (x : ℂ) ↦ x * I) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) z‖ ≤ C
have refine_2 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ fun (x : ℂ) ↦ x * I) ((↑x : ℂ) * I)‖ ≤ C
Tactic: refine quadrant_I (hd.comp (differentiable_id.mul_const _).diffContOnCl H) ⟨c, hc, B, ?_⟩ him
    (fun x hx => ?_) hz_im hz_re
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
H : MapsTo (fun (x : ℂ) ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ fun (x : ℂ) ↦ x * I) ((↑x : ℂ) * I)‖ ≤ C
have refine_2 : ‖f (↑(-x) : ℂ)‖ ≤ C
Tactic: rw [comp_apply, mul_assoc, I_mul_I, mul_neg_one, ← ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : z.im ≤ 0
⊢ ‖f z‖ ≤ C
have obtain : ∀ (z : ℂ) (hz_re : (-z).re ≤ 0) (hz_im : (-z).im ≤ 0), ‖f (-z)‖ ≤ C
Tactic: obtain ⟨z, rfl⟩ : ∃ z', -z' = z := ⟨-z, neg_neg z⟩
Cleared hypotheses: z, hz_re, hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : (-z).re ≤ 0
hz_im : (-z).im ≤ 0
⊢ ‖f (-z)‖ ≤ C
have hz_re₁ : 0 ≤ z.re
Tactic: simp only [neg_re, neg_im, neg_nonpos] at hz_re hz_im
Cleared hypotheses: hz_re, hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : (-z).re ≤ 0
hz_im : (-z).im ≤ 0
hz_re₁ : 0 ≤ z.re
⊢ ‖f (-z)‖ ≤ C
have hz_im₁ : 0 ≤ z.im
Tactic: simp only [neg_re, neg_im, neg_nonpos] at hz_re hz_im
Cleared hypotheses: hz_re, hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
⊢ ‖f (-z)‖ ≤ C
have change : ‖(f ∘ Neg.neg) z‖ ≤ C
Tactic: change ‖(f ∘ Neg.neg) z‖ ≤ C
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
have H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
Tactic: have H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0) := by
    intro w hw
    simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, mem_Iio] using hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
have refine_1 : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine
    quadrant_I (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_)
      hz_re hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
have refine_2 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C
Tactic: refine
    quadrant_I (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_)
      hz_re hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_2 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
have refine_3 : ∀ (x : ℝ) (hx : 0 ≤ x), ‖(f ∘ Neg.neg) ((↑x : ℂ) * I)‖ ≤ C
Tactic: refine
    quadrant_I (hd.comp differentiable_neg.diffContOnCl H) ?_ (fun x hx => ?_) (fun x hx => ?_)
      hz_re hz_im
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have refine_1 : ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
  (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: rcases hB with ⟨c, hc, B, hO⟩
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have refine_1 : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine ⟨c, hc, B, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C
have refine_2 : ‖f (↑(-x) : ℂ)‖ ≤ C
Tactic: rw [comp_apply, ← ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ Neg.neg) ((↑x : ℂ) * I)‖ ≤ C
have refine_3 : ‖f ((↑(-x) : ℂ) * I)‖ ≤ C
Tactic: rw [comp_apply, ← neg_mul, ← ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_re : 0 ≤ z.re
hz_im : z.im ≤ 0
⊢ ‖f z‖ ≤ C
have obtain : ∀ (z : ℂ) (hz_re : 0 ≤ (-z).re) (hz_im : (-z).im ≤ 0), ‖f (-z)‖ ≤ C
Tactic: obtain ⟨z, rfl⟩ : ∃ z', -z' = z := ⟨-z, neg_neg z⟩
Cleared hypotheses: z, hz_re, hz_im