awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
refine_3 : ‖f ((↑(-x) : ℂ) * I)‖ ≤ C
⊢ ‖(f ∘ Neg.neg) ((↑x : ℂ) * I)‖ ≤ C

Tactic:
rw [comp_apply, ← neg_mul, ← ofReal_neg]

Premises used: Complex.ofReal_neg, Function.comp_apply, neg_mul
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 ((↑(-x) : ℂ) * I)‖ ≤ C

Tactic:
him (-x) (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos, Neg.neg
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 ((↑(-x) : ℂ) * I)‖ ≤ C

Tactic:
exact him (-x) (neg_nonpos.2 hx)

Premises used: Iff.mpr, neg_nonpos, Neg.neg
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
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 : ℂ) = 0
him : ∀ x ≤ 0, f ((↑x : ℂ) * I) = 0
⊢ EqOn f 0 {z : ℂ | 0 ≤ z.re ∧ z.im ≤ 0}

Tactic:
fun _z hz =>
  norm_le_zero_iff.1 <|
    quadrant_IV hd hB (fun x hx => norm_le_zero_iff.2 <| hre x hx)
      (fun x hx => norm_le_zero_iff.2 <| him x hx) hz.1 hz.2

Premises used: Iff.mpr, PhragmenLindelof.quadrant_IV, Set.EqOn, And.right, And.left, norm_le_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hdf : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hBf : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hdg : DiffContOnCl ℂ g (Ioi 0 ×ℂ Iio 0)
hBg : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → f (↑x : ℂ) = g (↑x : ℂ)
him : ∀ x ≤ 0, f ((↑x : ℂ) * I) = g ((↑x : ℂ) * I)
⊢ EqOn f g {z : ℂ | 0 ≤ z.re ∧ z.im ≤ 0}

Tactic:
fun _z hz =>
  sub_eq_zero.1 <| eq_zero_on_quadrant_IV (hdf.sub hdg) (isBigO_sub_exp_rpow hBf hBg)
    (fun x hx => sub_eq_zero.2 <| hre x hx) (fun x hx => sub_eq_zero.2 <| him x hx) hz

Premises used: Iff.mpr, sub_eq_zero, PhragmenLindelof.eq_zero_on_quadrant_IV, Set.EqOn, DiffContOnCl.sub, PhragmenLindelof.isBigO_sub_exp_rpow, Iff.mp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
revert : ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
revert z
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
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'
⊢ ‖f z‖ ≤ max C C'

Tactic:
rcases hexp with ⟨c, hc, B, hO⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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'
inr : ∀ (h : 0 ≤ z.im), ‖f z‖ ≤ max C C'
⊢ ‖f z‖ ≤ max C C'

Tactic:
rcases le_total z.im 0 with h | h

Premises used: Complex.im, le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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'

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

Premises used: le_max_right, DiffContOnCl.mono, PhragmenLindelof.quadrant_IV, And.left, And.intro, Exists.intro, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
inl : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖f z‖ ≤ max C 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

Premises used: le_max_right, DiffContOnCl.mono, PhragmenLindelof.quadrant_IV, And.left, And.intro, Exists.intro, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)

Premises used: Iff.mpr, Filter.principal_mono, inf_le_inf_left, And.left, Asymptotics.IsBigO.mono
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)

Premises used: Iff.mpr, Filter.principal_mono, inf_le_inf_left, And.left, Asymptotics.IsBigO.mono
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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'

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

Premises used: le_max_right, DiffContOnCl.mono, And.left, And.intro, PhragmenLindelof.quadrant_I, Exists.intro, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
inr : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ‖f z‖ ≤ max C 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

Premises used: le_max_right, DiffContOnCl.mono, And.left, And.intro, PhragmenLindelof.quadrant_I, Exists.intro, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)

Premises used: Iff.mpr, Filter.principal_mono, inf_le_inf_left, And.left, Asymptotics.IsBigO.mono
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
⊢ IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)

Premises used: Iff.mpr, Filter.principal_mono, inf_le_inf_left, And.left, Asymptotics.IsBigO.mono
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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' : ℝ), (∀ (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)
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)

Tactic:
hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_

Premises used: Continuous.continuousOn, ContinuousOn.comp, DiffContOnCl.continuousOn, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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'
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ici 0) x),
    Membership.mem (γ := Set ℂ) (closure {z : ℂ | 0 < z.re}) (↑x : ℂ)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)

Tactic:
refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_

Premises used: Continuous.continuousOn, ContinuousOn.comp, DiffContOnCl.continuousOn, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.re} (↑x : ℂ)
⊢ Membership.mem (γ := Set ℂ) (closure {z : ℂ | 0 < z.re}) (↑x : ℂ)

Tactic:
rwa [closure_setOf_lt_re]

Premises used: Complex.closure_setOf_lt_re
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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)

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]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℂ)‖
neg : ∀ (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 : ℂ)‖

Tactic:
by_cases! h₀ : ∀ x : ℝ, 0 ≤ x → f x = 0
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℂ)‖

Tactic:
⟨0, le_rfl, fun y hy => ?_⟩

Premises used: le_rfl, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
pos : ∀ (y : ℝ) (hy : 0 ≤ y), ‖f (↑y : ℂ)‖ ≤ ‖f (↑0 : ℂ)‖
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖

Tactic:
refine ⟨0, le_rfl, fun y hy => ?_⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℂ)‖
pos₁ pos₂ : norm.{u_1} (E := E) 0 ≤ norm.{u_1} (E := E) 0
⊢ ‖f (↑y : ℂ)‖ ≤ ‖f (↑0 : ℂ)‖

Tactic:
rw [h₀ y hy, h₀ 0 le_rfl]

Premises used: le_rfl, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
neg :
  ∀ (x₀ : ℝ) (hx₀ : 0 ≤ x₀) (hne : f (↑x₀ : ℂ) ≠ 0), ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖

Tactic:
rcases h₀ with ⟨x₀, hx₀, hne⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
rwa : 0 < ‖f (↑x₀ : ℂ)‖
rwa₁ rwa₂ rwa₃ rwa₄ : f (↑x₀ : ℂ) ≠ 0
⊢ norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖

Tactic:
rwa [norm_zero, norm_pos_iff]

Premises used: norm_pos_iff, norm_zero
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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₀ : ℂ)‖

Tactic:
have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_iff]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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₀ : ℂ)‖
this : ∀ᶠ (x : ℝ) in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x : ℂ)‖

Tactic:
simpa only [exists_prop] using hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this

Premises used: exists_prop, ContinuousOn.exists_isMaxOn', ContinuousOn.norm, isClosed_Ici
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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₀ : ℂ)‖
neg : ∀ᶠ (x : ℝ) in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
⊢ ∃ (x : ℝ), 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖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