-- Mathlib/Analysis/Complex/PhragmenLindelof.lean
theorem right_half_plane_of_tendsto_zero_on_real (hd : DiffContOnCl ℂ f {z | 0 < z.re})
    (hexp : ∃ c < (2 : ℝ), ∃ B,
      f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c))
    (hre : Tendsto (fun x : ℝ => f x) atTop (𝓝 0)) (him : ∀ x : ℝ, ‖f (x * I)‖ ≤ C)
    (hz : 0 ≤ z.re) : ‖f z‖ ≤ C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
⊢ ContinuousOn (fun x => f ↑x) (Ici 0)

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

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x : ℝ
hx : x ∈ Ici 0
⊢ ↑x ∈ closure {z | 0 < z.re}

Proof state:
case intro.intro.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
this : ‖f 0‖ = ‖f ↑x₀‖
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

Tactic:
refine (h.not_le <| this ▸ ?_).elim

Result:
case intro.intro.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
this : ‖f 0‖ = ‖f ↑x₀‖
⊢ ‖f 0‖ ≤ C

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

Tactic:
rcases le_or_lt ‖f x₀‖ C with h | h

Result:
case intro.intro.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖
h : ‖f ↑x₀‖ ≤ C
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

case intro.intro.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖
h : C < ‖f ↑x₀‖
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x : ℝ
hx : x ∈ Ici 0
⊢ ↑x ∈ closure {z | 0 < z.re}

Tactic:
rwa [closure_setOf_lt_re]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x => f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
⊢ ‖f z‖ ≤ C

Tactic:
revert z

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x => f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

Proof state:
case intro.intro.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x₀‖
h : ‖f ↑x₀‖ ≤ C
⊢ ∀ {z : ℂ}, 0 ≤ z.re → ‖f z‖ ≤ C

Tactic:
simpa only [max_eq_left h] using hle _ hmax

Result:
no goals

Proof state:
case neg.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
hfc : ContinuousOn (fun x => f ↑x) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f ↑x₀ ≠ 0
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

Tactic:
have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_iff]

Result:
case neg.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
hfc : ContinuousOn (fun x => f ↑x) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f ↑x₀ ≠ 0
hlt : ‖0‖ < ‖f ↑x₀‖
⊢ ∃ x, 0 ≤ x ∧ ∀ (y : ℝ), 0 ≤ y → ‖f ↑y‖ ≤ ‖f ↑x‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
⊢ ball (↑x₀) (dist 0 ↑x₀) ⊆ {z | 0 < z.re}

Tactic:
intro z hz

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
hre : Tendsto (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‖ ≤ C ⊔ C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : z ∈ ball (↑x₀) (dist 0 ↑x₀)
⊢ z ∈ {z | 0 < z.re}