-- Mathlib/Analysis/Complex/PhragmenLindelof.lean
theorem vertical_strip (hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b))
    (hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)]
      fun z ↦ expR (B * expR (c * |z.im|)))
    (hle_a : ∀ z : ℂ, re z = a → ‖f z‖ ≤ C) (hle_b : ∀ z, re z = b → ‖f z‖ ≤ C) (hza : a ≤ re z)
    (hzb : re z ≤ b) : ‖f z‖ ≤ C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ ‖f (z * I * -I)‖ ≤ C

Tactic:
refine horizontal_strip (f := fun z ↦ f (z * -I))
  (hfd.comp (differentiable_id.mul_const _).diffContOnCl H) ?_ (fun z hz => hle_a _ ?_)
  (fun z hz => hle_b _ ?_) ?_ ?_

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ ∃ c < π / (b - a),
    ∃ B, (fun z => f (z * -I)) =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.re|))

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z✝ : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z✝.re
hzb : z✝.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = a
⊢ (z * -I).re = a

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z✝ : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z✝.re
hzb : z✝.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = b
⊢ (z * -I).re = b

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ a ≤ (z * I).im

case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ (z * I).im ≤ b

Proof state:
case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ (z * I).im ≤ b

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z✝ : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z✝.re
hzb : z✝.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = a
⊢ (z * -I).re = a

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z✝ : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z✝.re
hzb : z✝.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = b
⊢ (z * -I).re = b

case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ a ≤ (z * I).im

case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ (z * I).im ≤ b

Tactic:
all_goals simpa

Result:
no goals