awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ×ℂ 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
z : ℂ
hz_re : 0 ≤ (-z).re
hz_im : (-z).im ≤ 0
⊢ ‖f (-z)‖ ≤ C
have hz_re₁ : z.re ≤ 0
Tactic: simp only [neg_re, neg_im, neg_nonpos, neg_nonneg] 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 (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
z : ℂ
hz_re : 0 ≤ (-z).re
hz_im : (-z).im ≤ 0
hz_re₁ : z.re ≤ 0
⊢ ‖f (-z)‖ ≤ C
have hz_im₁ : 0 ≤ z.im
Tactic: simp only [neg_re, neg_im, neg_nonpos, neg_nonneg] 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 (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
z : ℂ
hz_re : z.re ≤ 0
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 (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
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
have H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
Tactic: have H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, neg_pos, mem_Ioi, 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 (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
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
have refine_1 : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine quadrant_II
    (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 (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
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
have refine_2 : ∀ (x : ℝ) (hx : x ≤ 0), ‖(f ∘ Neg.neg) (↑x : ℂ)‖ ≤ C
Tactic: refine quadrant_II
    (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 (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
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
refine_1 :
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
refine_2 : ∀ (x : ℝ) (hx : x ≤ 0), ‖(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_II
    (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 (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
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have refine_1 : ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
  (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
  ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 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 (Ioi 0 ×ℂ Iio 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C
him : ∀ x ≤ 0, ‖f ((↑x : ℂ) * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)) (f ∘ Neg.neg) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
have refine_1 : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Iio 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 (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
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : x ≤ 0
⊢ ‖(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 (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
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ C
have revert : ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
Tactic: revert z
Cleared hypotheses: 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ max C C'
have rcases : ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
  (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)), ‖f z‖ ≤ max C C'
Tactic: rcases hexp with ⟨c, hc, B, hO⟩
Cleared hypotheses: hexp
-- 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 {z : ℂ | 0 < z.re}
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖f z‖ ≤ max C C'
have inl : ∀ (h : z.im ≤ 0), ‖f z‖ ≤ max C C'
Tactic: rcases le_total z.im 0 with h | 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 {z : ℂ | 0 < z.re}
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
inl : ∀ (h : z.im ≤ 0), ‖f z‖ ≤ max C C'
⊢ ‖f z‖ ≤ max C C'
have inr : ∀ (h : 0 ≤ z.im), ‖f z‖ ≤ max C C'
Tactic: rcases le_total z.im 0 with h | 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 {z : ℂ | 0 < z.re}
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
h : z.im ≤ 0
⊢ ‖f z‖ ≤ max C C'
have inl : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine quadrant_IV (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz 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 {z : ℂ | 0 < z.re}
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
h : 0 ≤ z.im
⊢ ‖f z‖ ≤ max C C'
have inr : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
Tactic: refine quadrant_I (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz h
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
have hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
Tactic: have hle : ∀ C', (∀ x : ℝ, 0 ≤ x → ‖f x‖ ≤ C') →
      ∀ z : ℂ, 0 ≤ z.re → ‖f z‖ ≤ max C C' := fun C' hC' z hz ↦ by
    rcases hexp with ⟨c, hc, B, hO⟩
    rcases le_total z.im 0 with h | h
    · refine quadrant_IV (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz h
      exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)
    · refine quadrant_I (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz h
      exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
  Membership.mem (γ := Set ℂ) (closure {z : ℂ | 0 < z.re}) (↑x : ℂ)
Tactic: refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
⊢ Membership.mem (γ := Set ℂ) (closure {z : ℂ | 0 < z.re}) (↑x : ℂ)
have rwa : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.re} (↑x : ℂ)
Tactic: rwa [closure_setOf_lt_re]
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
have hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
Tactic: have hfc : ContinuousOn (fun x : ℝ => f x) (Ici 0) := by
      refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_
      rwa [closure_setOf_lt_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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
have pos : ∀ (h₀ : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = 0), ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
Tactic: by_cases! h₀ : ∀ x : ℝ, 0 ≤ x → f x = 0
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
pos : ∀ (h₀ : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = 0), ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
have neg : ∀ (h₀ : ∃ (x : ℝ), 0 ≤ x ∧ f (↑x : ℂ) ≠ 0), ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
Tactic: by_cases! h₀ : ∀ x : ℝ, 0 ≤ x → f x = 0
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
h₀ : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = 0
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
have pos : ∀ (y : ℝ) (hy : 0 ≤ y), ‖f (↑y : ℂ)‖ ≤ ‖f (↑0 : ℂ)‖
Tactic: refine ⟨0, le_rfl, fun y hy => ?_⟩
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
h₀ : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = 0
y : ℝ
hy : 0 ≤ y
⊢ ‖f (↑y : ℂ)‖ ≤ ‖f (↑0 : ℂ)‖
have pos : norm.{u_1} (E := E) 0 ≤ ‖f (↑0 : ℂ)‖
Tactic: rw [h₀ y hy, h₀ 0 le_rfl]
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
h₀ : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = 0
y : ℝ
hy : 0 ≤ y
pos : norm.{u_1} (E := E) 0 ≤ ‖f (↑0 : ℂ)‖
⊢ ‖f (↑y : ℂ)‖ ≤ ‖f (↑0 : ℂ)‖
have pos₁ : norm.{u_1} (E := E) 0 ≤ norm.{u_1} (E := E) 0
Tactic: rw [h₀ y hy, h₀ 0 le_rfl]
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
h₀ : ∃ (x : ℝ), 0 ≤ x ∧ f (↑x : ℂ) ≠ 0
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
have neg : ∀ (x₀ : ℝ) (hx₀ : 0 ≤ x₀) (hne : f (↑x₀ : ℂ) ≠ 0), ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
Tactic: rcases h₀ with ⟨x₀, hx₀, hne⟩
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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f (↑x₀ : ℂ) ≠ 0
⊢ norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖
have rwa : 0 < ‖f (↑x₀ : ℂ)‖
Tactic: rwa [norm_zero, norm_pos_iff]
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f (↑x₀ : ℂ) ≠ 0
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
have hlt : norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖
Tactic: have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f (↑x₀ : ℂ) ≠ 0
hlt : norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
have neg : ∀ᶠ (x : ℝ) in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
Tactic: suffices ∀ᶠ x : ℝ in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f x‖ ≤ ‖f x₀‖ by
      simpa only [exists_prop] using hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this
-- 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 {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f (↑x₀ : ℂ) ≠ 0
hlt : norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖
⊢ ∀ᶠ (x : ℝ) in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
have neg : ∀ᶠ (x : ℝ) in atTop ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
Tactic: rw [cocompact_eq_atBot_atTop, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot,
      bot_sup_eq]