-- Mathlib/Analysis/Complex/Hadamard.lean
/-- If z is on the closed strip `re ⁻¹' [l, u]`, then `(z - l) / (u - l)` is on the closed strip
  `re ⁻¹' [0, 1]`. -/
lemma mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip {z : ℂ} {l u : ℝ} (hul : l < u)
    (hz : z ∈ verticalClosedStrip l u) : z / (u - l) - l / (u - l) ∈ verticalClosedStrip 0 1

Proof state:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ u - l ≠ 0

Tactic:
linarith

Result:
no goals

Proof state:
case left.hab
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l ≤ z.re

Tactic:
exact hz.1

Result:
no goals

Proof state:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l * (u - l) / normSq (↑u - ↑l) ≤ z.re * (u - l) / normSq (↑u - ↑l) ∧
    z.re * (u - l) / normSq (↑u - ↑l) ≤ 1 + l * (u - l) / normSq (↑u - ↑l)

Tactic:
norm_cast

Result:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l * (u - l) / normSq ↑(u - l) ≤ z.re * (u - l) / normSq ↑(u - l) ∧
    z.re * (u - l) / normSq ↑(u - l) ≤ 1 + l * (u - l) / normSq ↑(u - l)

Proof state:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
⊢ z / (↑u - ↑l) - ↑l / (↑u - ↑l) ∈ verticalClosedStrip 0 1

Tactic:
simp only [verticalClosedStrip, Complex.div_re, mem_preimage, sub_re, mem_Icc,
  sub_nonneg, tsub_le_iff_right, ofReal_re, ofReal_im, sub_im, sub_self, mul_zero, zero_div,
  add_zero]

Result:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
⊢ l * (u - l) / normSq (↑u - ↑l) ≤ z.re * (u - l) / normSq (↑u - ↑l) ∧
    z.re * (u - l) / normSq (↑u - ↑l) ≤ 1 + l * (u - l) / normSq (↑u - ↑l)

Proof state:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l * (u - l) / normSq ↑(u - l) ≤ z.re * (u - l) / normSq ↑(u - l) ∧
    z.re * (u - l) / normSq ↑(u - l) ≤ 1 + l * (u - l) / normSq ↑(u - l)

Tactic:
simp_rw [Complex.normSq_ofReal, mul_div_assoc, div_mul_eq_div_div_swap,
  div_self (by linarith : u - l ≠ 0), ← div_eq_mul_one_div]

Result:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l / (u - l) ≤ z.re / (u - l) ∧ z.re / (u - l) ≤ 1 + l / (u - l)

Proof state:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l / (u - l) ≤ z.re / (u - l) ∧ z.re / (u - l) ≤ 1 + l / (u - l)

Tactic:
constructor

Result:
case left
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l / (u - l) ≤ z.re / (u - l)

case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re / (u - l) ≤ 1 + l / (u - l)

Proof state:
case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re / (u - l) ≤ 1 + l / (u - l)

Tactic:
rw [← sub_le_sub_iff_right (l / (u - l)), add_sub_assoc, sub_self, add_zero, div_sub_div_same,
  div_le_one (by simp[hul]), sub_le_sub_iff_right l]

Result:
case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re ≤ u

Proof state:
case left.hc.hab
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ 0 < u - l

Tactic:
simp [hul]

Result:
no goals

Proof state:
case left
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l / (u - l) ≤ z.re / (u - l)

Tactic:
gcongr

Result:
case left.hc
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ 0 ≤ u - l

case left.hab
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l ≤ z.re

Proof state:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
⊢ l * (u - l) / normSq (↑u - ↑l) ≤ z.re * (u - l) / normSq (↑u - ↑l) ∧
    z.re * (u - l) / normSq (↑u - ↑l) ≤ 1 + l * (u - l) / normSq (↑u - ↑l)

Tactic:
simp only [verticalClosedStrip] at hz

Result:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l * (u - l) / normSq (↑u - ↑l) ≤ z.re * (u - l) / normSq (↑u - ↑l) ∧
    z.re * (u - l) / normSq (↑u - ↑l) ≤ 1 + l * (u - l) / normSq (↑u - ↑l)

Proof state:
case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re ≤ u

Tactic:
exact hz.2

Result:
no goals

Proof state:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ 0 < u - l

Tactic:
simp[hul]

Result:
no goals

Proof state:
case left.hc
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ 0 ≤ u - l

Tactic:
apply le_of_lt

Result:
case left.hc.hab
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ 0 < u - l