-- Mathlib/Analysis/Complex/Hadamard.lean
/-- The supremum of the norm of `scale f l u` on the line `z.re = 0` is the same as the supremum
  of `f` on the line `z.re = l`. -/
lemma sSupNormIm_scale_left (f : ℂ → E) {l u : ℝ} (hul : l < u) :
    sSupNormIm (scale f l u) 0 = sSupNormIm f l

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ¬u - l = 0

Tactic:
linarith

Result:
no goals

Proof state:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ (z - ↑l).re * (u - l) / ((u - l) * (u - l)) + (z - ↑l).im * (↑(u - l)).im / ((u - l) * (u - l)) = 0

Tactic:
simp[hz₁]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' (re ⁻¹' {0}) = f '' (re ⁻¹' {l})

Tactic:
ext e

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ e ∈ scale f l u '' (re ⁻¹' {0}) ↔ e ∈ f '' (re ⁻¹' {l})

Proof state:
case h.mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = l ∧ f x = e
⊢ ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h

Result:
case h.mpr.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e

Proof state:
case h.mpr.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e

Tactic:
use ((z - l) / (u - l))

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 0 ∧ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Proof state:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / ↑(u - l)).re = 0

Tactic:
rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]

Result:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ (z - ↑l).re * (u - l) / ((u - l) * (u - l)) + (z - ↑l).im * (↑(u - l)).im / ((u - l) * (u - l)) = 0

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 0 ∧ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
constructor

Result:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 0

case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ↑u - ↑l ≠ 0

Tactic:
norm_cast

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ¬u - l = 0

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e) ↔ ∃ x, x.re = l ∧ f x = e

Tactic:
constructor

Result:
case h.mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e) → ∃ x, x.re = l ∧ f x = e

case h.mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = l ∧ f x = e) → ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e

Proof state:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑u - ↑l)) = e

Tactic:
rw [div_mul_comm, div_self (by norm_cast; linarith)]

Result:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e

Proof state:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 0

Tactic:
norm_cast

Result:
case h.left
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - ↑l) / ↑(u - l)).re = 0

Proof state:
case h.mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e
⊢ ∃ x, x.re = l ∧ f x = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h

Result:
case h.mp.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = 0
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ ∃ x, x.re = l ∧ f x = e

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSupNormIm (scale f l u) 0 = sSupNormIm f l

Tactic:
simp_rw [sSupNormIm, image_comp]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSup (norm '' (scale f l u '' (re ⁻¹' {0}))) = sSup (norm '' (f '' (re ⁻¹' {l})))

Proof state:
case h.mp.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = 0
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ ∃ x, x.re = l ∧ f x = e

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

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = 0
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ (↑l + z * (↑u - ↑l)).re = l ∧ f (↑l + z * (↑u - ↑l)) = e

Proof state:
case h.mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = l ∧ f x = e) → ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e

Tactic:
intro h

Result:
case h.mpr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = l ∧ f x = e
⊢ ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e

Proof state:
case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e

Tactic:
simp [hz₂]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ e ∈ scale f l u '' (re ⁻¹' {0}) ↔ e ∈ f '' (re ⁻¹' {l})

Tactic:
simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e) ↔ ∃ x, x.re = l ∧ f x = e

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = 0
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ (↑l + z * (↑u - ↑l)).re = l ∧ f (↑l + z * (↑u - ↑l)) = e

Tactic:
simp [hz₁, hz₂]

Result:
no goals

Proof state:
case h.mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e) → ∃ x, x.re = l ∧ f x = e

Tactic:
intro h

Result:
case h.mp
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ x, x.re = 0 ∧ f (↑l + x * (↑u - ↑l)) = e
⊢ ∃ x, x.re = l ∧ f x = e

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
this : scale f l u '' (re ⁻¹' {0}) = f '' (re ⁻¹' {l})
⊢ sSup (norm '' (scale f l u '' (re ⁻¹' {0}))) = sSup (norm '' (f '' (re ⁻¹' {l})))

Tactic:
rw [this]

Result:
no goals