-- Mathlib/Analysis/Complex/Hadamard.lean
/-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`. -/
lemma scale_bddAbove {f : ℂ → E} {l u : ℝ} (hul : l < u)
    (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip l u)) :
    BddAbove ((norm ∘ scale f l u) '' verticalClosedStrip 0 1)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ∃ x ∈ verticalClosedStrip l u, ‖f x‖ = ‖f (↑l + w * (↑u - ↑l))‖

Tactic:
use ↑l + w * (↑u - ↑l)

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ↑l + w * (↑u - ↑l) ∈ verticalClosedStrip l u ∧ ‖f (↑l + w * (↑u - ↑l))‖ = ‖f (↑l + w * (↑u - ↑l))‖

Proof state:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
⊢ ∃ x, ∀ y ∈ norm ∘ scale f l u '' verticalClosedStrip 0 1, y ≤ x

Tactic:
use R

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
⊢ ∀ y ∈ norm ∘ scale f l u '' verticalClosedStrip 0 1, y ≤ R

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ↑l + w * (↑u - ↑l) ∈ verticalClosedStrip l u

Tactic:
exact scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hw₁

Result:
no goals

Proof state:
case h.intro.intro.refl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ (norm ∘ scale f l u) w ≤ R

Tactic:
simp only [comp_apply, scale, smul_eq_mul]

Result:
case h.intro.intro.refl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ‖f (↑l + w * (↑u - ↑l))‖ ≤ R

Proof state:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
⊢ BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)

Tactic:
rw [bddAbove_def]

Result:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
⊢ ∃ x, ∀ y ∈ norm ∘ scale f l u '' verticalClosedStrip 0 1, y ≤ x

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ↑l + w * (↑u - ↑l) ∈ verticalClosedStrip l u ∧ ‖f (↑l + w * (↑u - ↑l))‖ = ‖f (↑l + w * (↑u - ↑l))‖

Tactic:
simp only [and_true]

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ↑l + w * (↑u - ↑l) ∈ verticalClosedStrip l u

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
r : ℝ
hr : r ∈ norm ∘ scale f l u '' verticalClosedStrip 0 1
⊢ r ≤ R

Tactic:
obtain ⟨w, hw₁, hw₂, _⟩ := hr

Result:
case h.intro.intro.refl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ (norm ∘ scale f l u) w ≤ R

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ‖f (↑l + w * (↑u - ↑l))‖ ∈ norm ∘ f '' verticalClosedStrip l u

Tactic:
simp only [comp_apply, mem_image]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ∃ x ∈ verticalClosedStrip l u, ‖f x‖ = ‖f (↑l + w * (↑u - ↑l))‖

Proof state:
case h.intro.intro.refl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
this : ‖f (↑l + w * (↑u - ↑l))‖ ∈ norm ∘ f '' verticalClosedStrip l u
⊢ ‖f (↑l + w * (↑u - ↑l))‖ ≤ R

Tactic:
exact hR ‖f (↑l + w * (↑u - ↑l))‖ this

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
⊢ ∀ y ∈ norm ∘ scale f l u '' verticalClosedStrip 0 1, y ≤ R

Tactic:
intro r hr

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
r : ℝ
hr : r ∈ norm ∘ scale f l u '' verticalClosedStrip 0 1
⊢ r ≤ R

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
⊢ BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)

Tactic:
obtain ⟨R, hR⟩ := bddAbove_def.mp hB

Result:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
⊢ BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)

Proof state:
case h.intro.intro.refl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
⊢ ‖f (↑l + w * (↑u - ↑l))‖ ≤ R

Tactic:
have : ‖f (↑l + w * (↑u - ↑l))‖ ∈ norm ∘ f '' verticalClosedStrip l u := by
  simp only [comp_apply, mem_image]
  use ↑l + w * (↑u - ↑l)
  simp only [and_true]
  exact scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hw₁

Result:
case h.intro.intro.refl
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
R : ℝ
hR : ∀ y ∈ norm ∘ f '' verticalClosedStrip l u, y ≤ R
w : ℂ
hw₁ : w ∈ verticalClosedStrip 0 1
this : ‖f (↑l + w * (↑u - ↑l))‖ ∈ norm ∘ f '' verticalClosedStrip l u
⊢ ‖f (↑l + w * (↑u - ↑l))‖ ≤ R