-- Mathlib/Analysis/Complex/Hadamard.lean
theorem norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip (f : ℂ → E) (ε : ℝ) (hε : 0 < ε)
    (z : ℂ) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) (hz : z ∈ verticalClosedStrip 0 1) :
    ‖F f ε z‖ ≤ 1

Proof state:
case h.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)
⊢ ∃ B,
    (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
      Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
simp only [comp_apply, mem_upperBounds, mem_image, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂] at hBF

Result:
case h.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∃ B,
    (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
      Real.exp (B * Real.exp (0 * |z.im|))

Proof state:
case h.hp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
x : ℂ
hx : x ∈ re ⁻¹' Ioo 0 1
⊢ ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖

Tactic:
norm_num

Result:
case h.hp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
x : ℂ
hx : x ∈ re ⁻¹' Ioo 0 1
⊢ ‖invInterpStrip f x ε • f x‖ ≤ Real.exp BF

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖F f ε z‖ ≤ 1

Tactic:
apply PhragmenLindelof.vertical_strip
  (DiffContOnCl.smul (diffContOnCl_invInterpStrip f hε) hd) _
  (fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inl hx))
  (fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inr hx)) hz.1 hz.2

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ∃ c < Real.pi / (1 - 0),
    ∃ B,
      (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
        Real.exp (B * Real.exp (c * |z.im|))

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < Real.pi ∧
    ∃ B,
      (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
        Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
refine ⟨ Real.pi_pos, ?_⟩

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ∃ B,
    (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
      Real.exp (B * Real.exp (0 * |z.im|))

Proof state:
case h.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∃ B,
    (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
      Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
use BF

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
    Real.exp (BF * Real.exp (0 * |z.im|))

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ∃ B,
    (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
      Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
obtain ⟨BF, hBF⟩ := F_BddAbove f ε hε hB

Result:
case h.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)
⊢ ∃ B,
    (fun x => invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z =>
      Real.exp (B * Real.exp (0 * |z.im|))