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

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 = u
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e

Tactic:
simp only [one_mul, add_sub_cancel, hz₂]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 1 ∧ 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 = u
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 1

case h.right
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = u
hz₂ : f z = e
⊢ f (↑l + (z - ↑l) / (↑u - ↑l) * (↑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 = u
hz₂ : f z = e
⊢ ∃ x, x.re = 1 ∧ 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 = u
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 1 ∧ 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
this : scale f l u '' (re ⁻¹' {1}) = f '' (re ⁻¹' {u})
⊢ sSup (norm '' (scale f l u '' (re ⁻¹' {1}))) = sSup (norm '' (f '' (re ⁻¹' {u})))

Tactic:
rw [this]

Result:
no goals

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

Tactic:
linarith

Result:
no goals

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 = u ∧ f x = e
⊢ ∃ x, x.re = 1 ∧ 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 = u
hz₂ : f z = e
⊢ ∃ x, x.re = 1 ∧ f (↑l + x * (↑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 = u
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 = u
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 = 1 ∧ f (↑l + x * (↑u - ↑l)) = e) ↔ ∃ x, x.re = u ∧ 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 = 1 ∧ f (↑l + x * (↑u - ↑l)) = e) → ∃ x, x.re = u ∧ 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 = u ∧ f x = e) → ∃ x, x.re = 1 ∧ f (↑l + x * (↑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 = u
hz₂ : f z = e
⊢ ((z - ↑l) / (↑u - ↑l)).re = 1

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 = u
hz₂ : f z = e
⊢ ((z - ↑l) / ↑(u - l)).re = 1

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 = 1
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ ∃ x, x.re = u ∧ 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 = 1
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ (↑l + z * (↑u - ↑l)).re = u ∧ f (↑l + z * (↑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 = u
hz₂ : f z = e
⊢ (z - ↑l).re * (u - l) / ((u - l) * (u - l)) + (z - ↑l).im * (↑(u - l)).im / ((u - l) * (u - l)) = 1

Tactic:
simp only [sub_re, hz₁, ofReal_re, sub_im, ofReal_im, sub_zero, ofReal_sub, sub_self,
  mul_zero, zero_div, add_zero]

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

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 = u
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 = u
hz₂ : f z = e
⊢ f (↑l + 1 * (z - ↑l)) = e

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 ⁻¹' {1}) ↔ e ∈ f '' (re ⁻¹' {u})

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 = 1 ∧ f (↑l + x * (↑u - ↑l)) = e) ↔ ∃ x, x.re = u ∧ 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 = 1
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ (↑l + z * (↑u - ↑l)).re = u ∧ f (↑l + z * (↑u - ↑l)) = e

Tactic:
simp only [add_re, ofReal_re, mul_re, hz₁, sub_re, one_mul, sub_im, ofReal_im, sub_self,
  mul_zero, sub_zero, add_sub_cancel, hz₂, and_self]

Result:
no goals

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

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

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 = 1 ∧ f (↑l + x * (↑u - ↑l)) = e
⊢ ∃ x, x.re = u ∧ 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 = 1
hz₂ : f (↑l + z * (↑u - ↑l)) = e
⊢ ∃ x, x.re = u ∧ f x = 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 = u
hz₂ : f z = e
⊢ ((z - ↑l) / ↑(u - l)).re = 1

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 = u
hz₂ : f z = e
⊢ (z - ↑l).re * (u - l) / ((u - l) * (u - l)) + (z - ↑l).im * (↑(u - l)).im / ((u - l) * (u - l)) = 1

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 = u
hz₂ : f z = e
⊢ (u - l) * (u - l) / ((u - l) * (u - l)) = 1

Tactic:
rw [div_mul_eq_div_div_swap, mul_div_assoc,
  div_self (by norm_cast; linarith),
  mul_one, div_self (by norm_cast; linarith)]

Result:
no goals