Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
⊢ ‖g ε z • f z‖ ≤ C

Tactic:
obtain ⟨R, hzR, hR⟩ :
    ∃ R : ℝ, |z.re| < R ∧ ∀ w, |re w| = R → im w ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C := by
    refine ((eventually_gt_atTop _).and ?_).exists
    rcases hO.exists_pos with ⟨A, hA₀, hA⟩
    simp only [isBigOWith_iff, eventually_inf_principal, eventually_comap, mem_Ioo,
      mem_preimage, (· ∘ ·), Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] at hA
    suffices
        Tendsto (fun R => expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0) by
      filter_upwards [this.eventually (ge_mem_nhds hC₀), hA] with R hR Hle w hre him
      calc
        ‖g ε w • f w‖ ≤ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) := ?_
        _ ≤ C := hR
      rw [norm_smul, Real.exp_add, ← hre, Real.exp_add, Real.exp_log hA₀, mul_assoc, mul_comm _ A]
      gcongr
      exacts [hδ <| Ioo_subset_Icc_self him, Hle _ hre him]
    refine Real.tendsto_exp_atBot.comp ?_
    suffices H : Tendsto (fun R => δ + B * (expR ((d - c) * R))⁻¹) atTop (𝓝 (δ + B * 0)) by
      rw [mul_zero, add_zero] at H
      refine Tendsto.atBot_add ?_ tendsto_const_nhds
      simpa only [id, (· ∘ ·), add_mul, mul_assoc, ← div_eq_inv_mul, ← Real.exp_sub, ← sub_mul,
        sub_sub_cancel]
        using H.neg_mul_atTop δ₀ <| Real.tendsto_exp_atTop.comp <| tendsto_id.const_mul_atTop hd₀
    refine tendsto_const_nhds.add (tendsto_const_nhds.mul ?_)
    exact tendsto_inv_atTop_zero.comp <| Real.tendsto_exp_atTop.comp <|
      tendsto_id.const_mul_atTop (sub_pos.2 hcd)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
R : ℝ
hzR : |z.re| < R
hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C
⊢ ‖g ε z • f z‖ ≤ C