awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
left : l ≤ l + z.re * (u - l)
right : l + z.re * (u - l) ≤ u
⊢ l ≤ l + z.re * (u - l) ∧ l + z.re * (u - l) ≤ u

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
nlinarith : l + z.re * (u - l) < l → l + z.re * (u - l) - l + (0 - (l - u) * (0 - z.re)) = 0
⊢ l ≤ l + z.re * (u - l)

Tactic:
nlinarith [hz.1, hz.2, hul]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
nlinarith : u < l + z.re * (u - l) → u - (l + z.re * (u - l)) + (0 - (l - u) * (z.re - 1)) = 0
⊢ l + z.re * (u - l) ≤ u

Tactic:
nlinarith [hz.1, hz.2, hul]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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:
hB.mono ?_

Premises used: BddAbove.mono
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
refine : norm ∘ scale f l u '' verticalClosedStrip 0 1 ⊆ norm ∘ f '' verticalClosedStrip l u
⊢ BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)

Tactic:
refine hB.mono ?_

Premises used: BddAbove.mono
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ (norm ∘ scale f l u) z ∈ norm ∘ f '' verticalClosedStrip l u

Tactic:
⟨l + z * (u - l), scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hz, rfl⟩

Premises used: HMul.hMul, Set.Mem, setOf, HSub.hSub, Complex.ofReal, HAdd.hAdd, And.intro, Exists.intro, Set.image, Complex.HadamardThreeLines.scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip, rfl
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ (norm ∘ scale f l u) z ∈ norm ∘ f '' verticalClosedStrip l u

Tactic:
exact ⟨l + z * (u - l), scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hz, rfl⟩
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
simp : ∀ (z : ℂ), z.re = 0 → ‖f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤ a
⊢ ∀ z ∈ re ⁻¹' {0}, ‖scale f l u z‖ ≤ a

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

Premises used: Complex.HadamardThreeLines.scale, Set.mem_singleton_iff, smul_eq_mul, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ (↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)) ∈ re ⁻¹' {l}

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
z : ℂ
hz : z.re = 0
⊢ ‖f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤ a

Tactic:
exact ha (↑l + z * (↑u - ↑l)) (by simp [hz])

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
simp : ∀ (z : ℂ), z.re = 1 → ‖f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤ b
⊢ ∀ z ∈ re ⁻¹' {1}, ‖scale f l u z‖ ≤ b

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

Premises used: Complex.HadamardThreeLines.scale, Set.mem_singleton_iff, smul_eq_mul, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ (↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)) ∈ re ⁻¹' {u}

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
z : ℂ
hz : z.re = 1
⊢ ‖f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤ b

Tactic:
exact hb (↑l + z * (↑u - ↑l)) (by simp [hz])

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
simp_rw : sSup (norm '' scale f l u '' re ⁻¹' {0}) = sSup (norm '' f '' re ⁻¹' {l})
⊢ sSupNormIm (scale f l u) 0 = sSupNormIm f l

Tactic:
simp_rw [sSupNormIm, image_comp]

Premises used: Complex.HadamardThreeLines.sSupNormIm, Set.image_comp
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
h : ∀ (e : E), e ∈ scale f l u '' re ⁻¹' {0} ↔ e ∈ f '' re ⁻¹' {l}
⊢ scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l}

Tactic:
ext e
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
⊢ 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]

Premises used: Complex.HadamardThreeLines.scale, Set.mem_image, Set.mem_singleton_iff, smul_eq_mul, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h₁ : (∃ (x : ℂ), x.re = l ∧ f x = e) → ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ (∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = l ∧ f x = e

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h₁ : ∀ (z : ℂ) (hz₁ : z.re = 0) (hz₂ : f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e), ∃ (x : ℂ), x.re = l ∧ f x = e
⊢ ∃ (x : ℂ), x.re = l ∧ f x = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))).re = l ∧ f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = l ∧ f x = e

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

Premises used: HSub.hSub
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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₂]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ (x : ℂ), x.re = l ∧ f x = e
h₁ : ∀ (z : ℂ) (hz₁ : z.re = l) (hz₂ : f z = e), ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h :
  ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e

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

Premises used: HSub.hSub, HDiv.hDiv, Complex.ofReal
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0
h₁ : f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : ((z - (↑l : ℂ)) / (↑(u - l) : ℂ)).re = 0
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : (z - (↑l : ℂ)).re * (u - l) / ((u - l) * (u - l)) + (z - (↑l : ℂ)).im * (↑(u - l) : ℂ).im / ((u - l) * (u - l)) = 0
⊢ ((z - (↑l : ℂ)) / (↑(u - l) : ℂ)).re = 0

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

Premises used: Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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₁]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
norm_cast : ¬u - l = 0
⊢ (↑u : ℂ) - (↑l : ℂ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
linarith : u - l = 0 → l - u + (u - l - 0) = 0
⊢ ¬u - l = 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : f ((↑l : ℂ) + 1 * (z - (↑l : ℂ))) = e
⊢ f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e

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

Premises used: div_mul_comm, div_self
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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₂]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l}

Tactic:
have : scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l} := by
    ext e
    simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
    constructor
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ↑l + z * (↑u - ↑l)
      simp [hz₁, hz₂]
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ((z - l) / (u - l))
      constructor
      · norm_cast
        rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]
        simp [hz₁]
      · rw [div_mul_comm, div_self (by norm_cast; linarith)]
        simp [hz₂]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
this : scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l}
rw rw₁ : sSup (norm '' f '' re ⁻¹' {l}) = sSup (norm '' f '' re ⁻¹' {l})
⊢ sSup (norm '' scale f l u '' re ⁻¹' {0}) = sSup (norm '' f '' re ⁻¹' {l})

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
simp_rw : sSup (norm '' scale f l u '' re ⁻¹' {1}) = sSup (norm '' f '' re ⁻¹' {u})
⊢ sSupNormIm (scale f l u) 1 = sSupNormIm f u

Tactic:
simp_rw [sSupNormIm, image_comp]

Premises used: Complex.HadamardThreeLines.sSupNormIm, Set.image_comp
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
h : ∀ (e : E), e ∈ scale f l u '' re ⁻¹' {1} ↔ e ∈ f '' re ⁻¹' {u}
⊢ scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u}

Tactic:
ext e
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
⊢ 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]

Premises used: Complex.HadamardThreeLines.scale, Set.mem_image, Set.mem_singleton_iff, smul_eq_mul, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h₁ : (∃ (x : ℂ), x.re = u ∧ f x = e) → ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ (∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = u ∧ f x = e

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h₁ : ∀ (z : ℂ) (hz₁ : z.re = 1) (hz₂ : f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e), ∃ (x : ℂ), x.re = u ∧ f x = e
⊢ ∃ (x : ℂ), x.re = u ∧ f x = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))).re = u ∧ f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = u ∧ f x = e

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

Premises used: HSub.hSub
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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]

Premises used: Complex.mul_re, sub_self, and_self, Complex.sub_im, sub_zero, Complex.sub_re, Complex.add_re, MulZeroClass.mul_zero, add_sub_cancel, Complex.ofReal_re, Complex.ofReal_im, one_mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ (x : ℂ), x.re = u ∧ f x = e
h₁ : ∀ (z : ℂ) (hz₁ : z.re = u) (hz₂ : f z = e), ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := h
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h :
  ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e

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

Premises used: HSub.hSub, HDiv.hDiv, Complex.ofReal
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1
h₁ : f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : ((z - (↑l : ℂ)) / (↑(u - l) : ℂ)).re = 1
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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:
grind [Complex.div_re, Complex.normSq_ofReal, sub_re, ofReal_re, ofReal_im, mul_eq_zero]

Premises used: Complex.sub_re, mul_eq_zero, Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
norm_cast : ¬u - l = 0
⊢ (↑u : ℂ) - (↑l : ℂ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
linarith : u - l = 0 → l - u + (u - l - 0) = 0
⊢ ¬u - l = 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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
h : f ((↑l : ℂ) + 1 * (z - (↑l : ℂ))) = e
⊢ f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e

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

Premises used: div_mul_comm, div_self
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
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₂]

Premises used: add_sub_cancel, one_mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u}

Tactic:
have : scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u} := by
    ext e
    simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
    constructor
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ↑l + z * (↑u - ↑l)
      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]
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ((z - l) / (u - l))
      constructor
      · norm_cast
        grind [Complex.div_re, Complex.normSq_ofReal, sub_re, ofReal_re, ofReal_im, mul_eq_zero]
      · rw [div_mul_comm, div_self (by norm_cast; linarith)]
        simp only [one_mul, add_sub_cancel, hz₂]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
this : scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u}
rw rw₁ : sSup (norm '' f '' re ⁻¹' {u}) = sSup (norm '' f '' re ⁻¹' {u})
⊢ sSup (norm '' scale f l u '' re ⁻¹' {1}) = sSup (norm '' f '' re ⁻¹' {u})

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
simp_rw :
  (if sSupNormIm f l = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
    else
      (↑(sSupNormIm f l) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
        (↑(sSupNormIm (scale f l u) 1) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))) =
    if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
    else
      (↑(sSupNormIm f l) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
        (↑(sSupNormIm f u) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))
⊢ (if sSupNormIm (scale f l u) 0 = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
    else
      (↑(sSupNormIm (scale f l u) 0) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
        (↑(sSupNormIm (scale f l u) 1) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))) =
    if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
    else
      (↑(sSupNormIm f l) : ℂ) ^ (1 - (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))) *
        (↑(sSupNormIm f u) : ℂ) ^ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)))

Tactic:
simp_rw [sSupNormIm_scale_left f hul, sSupNormIm_scale_right f hul]

Premises used: Complex.HadamardThreeLines.sSupNormIm_scale_left, Complex.HadamardThreeLines.sSupNormIm_scale_right
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
simp : ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re
⊢ ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖

Tactic:
simp only [norm_mul, ← ofReal_add, norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _,
    sub_re, one_re]

Premises used: Complex.sub_re, Complex.ofReal_add, norm_mul, Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.one_re, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
rw :
  ‖f z‖ * HPow.hPow (β := ℝ) ((ε + sSupNormIm f 0) ^ (1 - z.re)) (-1) *
      HPow.hPow (β := ℝ) ((ε + sSupNormIm f 1) ^ z.re) (-1) ≤
    1
rw₁ : 0 < (ε + sSupNormIm f 1) ^ z.re
rw₂ : 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)
⊢ ‖f z‖ ≤ (ε + sSupNormIm f 0) ^ (1 - z.re) * (ε + sSupNormIm f 1) ^ z.re

Tactic:
rw [← mul_inv_le_iff₀', ← one_mul (((ε + sSupNormIm f 1) ^ z.re)), ← mul_inv_le_iff₀,
    ← Real.rpow_neg_one, ← Real.rpow_neg_one]

Premises used: Real.rpow_neg_one, mul_inv_le_iff₀, Complex.re, Complex.HadamardThreeLines.sSupNormIm, HPow.hPow, HAdd.hAdd, OfNat.ofNat, one_mul, mul_inv_le_iff₀'
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
simp : ‖f z‖ * ((ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)) ≤ 1
⊢ ‖f z‖ * HPow.hPow (β := ℝ) ((ε + sSupNormIm f 0) ^ (1 - z.re)) (-1) *
      HPow.hPow (β := ℝ) ((ε + sSupNormIm f 1) ^ z.re) (-1) ≤
    1

Tactic:
simp only [← Real.rpow_mul (le_of_lt (sSupNormIm_eps_pos f hε _)),
    mul_neg, mul_one, neg_sub, mul_assoc]

Premises used: neg_sub, mul_assoc, le_of_lt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, mul_one, Real.rpow_mul, mul_neg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ * ((ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)) ≤ 1

Tactic:
simpa [F, norm_invInterpStrip _ _ hε, norm_smul, mul_comm] using
      norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip f ε hε z hd hB hz

Premises used: norm_smul, Complex.HadamardThreeLines.norm_invInterpStrip, mul_comm, Complex.HadamardThreeLines.F, Complex.HadamardThreeLines.norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 1) ^ z.re

Tactic:
simp only [Real.rpow_pos_of_pos (sSupNormIm_eps_pos f hε _) z.re]

Premises used: Real.rpow_pos_of_pos, Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.re
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < (ε + sSupNormIm f 0) ^ (1 - z.re)

Tactic:
simp only [Real.rpow_pos_of_pos (sSupNormIm_eps_pos f hε _) (1 - z.re)]

Premises used: Real.rpow_pos_of_pos, HSub.hSub, Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.re, OfNat.ofNat