awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
        ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(x + sSupNormIm f 1) : ℂ) ^ z‖
hg : 0 ≤ z.re
⊢ sSupNormIm f 1 ≠ 0 ∨ 0 ≤ z.re

Tactic:
right
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
        ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(x + sSupNormIm f 1) : ℂ) ^ z‖
⊢ 0 ≤ z.re

Tactic:
simp only [le_of_lt hz.1]

Premises used: le_of_lt, And.left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
        ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(x + sSupNormIm f 1) : ℂ) ^ z‖
⊢ z.re ≠ 0

Tactic:
simpa using (ne_comm.mpr (ne_of_lt hz.1))

Premises used: Iff.mpr, And.left, ne_comm, ne_of_lt
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
        ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(x + sSupNormIm f 1) : ℂ) ^ z‖
⊢ (1 - z).re ≠ 0

Tactic:
simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))

Premises used: Iff.mpr, sub_eq_zero, And.right, ne_comm, ne_of_lt
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hx : z ∈ closure (verticalStrip 0 1)
⊢ ‖f z‖ ≤ ‖interpStrip f z‖

Tactic:
apply le_on_closure (fun w hw ↦ norm_le_interpStrip_of_mem_verticalStrip_zero f w hd hB hw)
    (Continuous.comp_continuousOn' continuous_norm hd.2)
    (Continuous.comp_continuousOn' continuous_norm (diffContOnCl_interpStrip f).2)

Premises used: Complex.HadamardThreeLines.diffContOnCl_interpStrip, Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalStrip_zero, DiffContOnCl.continuousOn, Continuous.comp_continuousOn', continuous_norm, le_on_closure
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hx :
  ∀ (hz : z ∈ re ⁻¹' Icc 0 1) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
hx₁ :
  ∀ (hz : z ∈ re ⁻¹' closure (Ioo 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
hx₂ hx₃ hx₄ hx₅ :
  ∀ (hz : z ∈ closure (re ⁻¹' Ioo 0 1)) (hd : DiffContOnCl ℂ f (verticalStrip 0 1))
    (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), z ∈ closure (verticalStrip 0 1)
⊢ z ∈ closure (verticalStrip 0 1)

Tactic:
rwa [verticalClosedStrip, ← closure_Ioo zero_ne_one, ← closure_preimage_re] at hz

Premises used: zero_ne_one, Complex.closure_preimage_re, Complex.HadamardThreeLines.verticalClosedStrip, closure_Ioo
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
pos :
  ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0),
    ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
neg :
  ∀ (h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0),
    ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0

Premises used: Complex.HadamardThreeLines.sSupNormIm, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
pos :
  0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re ∨
    sSupNormIm f 0 ^ (1 - z.re) ≤ 0 ∧ sSupNormIm f 1 ^ z.re ≤ 0
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
rw [interpStrip_eq_of_zero f z h, norm_zero, mul_nonneg_iff]

Premises used: mul_nonneg_iff, norm_zero, Complex.HadamardThreeLines.interpStrip_eq_of_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
pos : 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re
⊢ 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re ∨
    sSupNormIm f 0 ^ (1 - z.re) ≤ 0 ∧ sSupNormIm f 1 ^ z.re ≤ 0

Tactic:
left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re

Tactic:
⟨Real.rpow_nonneg (sSupNormIm_nonneg f _) _,
        Real.rpow_nonneg (sSupNormIm_nonneg f _) _ ⟩

Premises used: And.intro, Real.rpow_nonneg, Complex.HadamardThreeLines.sSupNormIm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re

Tactic:
exact ⟨Real.rpow_nonneg (sSupNormIm_nonneg f _) _,
        Real.rpow_nonneg (sSupNormIm_nonneg f _) _ ⟩
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ sSupNormIm f 0 ≠ 0

Tactic:
rcases h with ⟨h0, h1⟩
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
h0 : sSupNormIm f 0 ≠ 0
⊢ sSupNormIm f 1 ≠ 0

Tactic:
rcases h with ⟨h0, h1⟩
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
⊢ 0 ≠ sSupNormIm f 0

Tactic:
rw [ne_comm] at h0 h1

Premises used: ne_comm
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
h0₁ : 0 ≠ sSupNormIm f 0
⊢ 0 ≠ sSupNormIm f 1

Tactic:
rw [ne_comm] at h0 h1

Premises used: ne_comm
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
neg :
  ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤
    sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]

Premises used: Complex.HadamardThreeLines.interpStrip_eq_of_pos, Complex.HadamardThreeLines.sSupNormIm_nonneg, OfNat.ofNat, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
neg :
  ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤
    sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤
    sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
simp only [norm_mul]

Premises used: norm_mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
neg : sSupNormIm f 0 ^ (1 - z).re * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤
    sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h0).mp (sSupNormIm_nonneg f _)) _]

Premises used: Ne.le_iff_lt, Iff.mp, Complex.HadamardThreeLines.sSupNormIm_nonneg, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
neg : sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSupNormIm f 0 ^ (1 - z).re * ‖(↑(sSupNormIm f 1) : ℂ) ^ z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h1).mp (sSupNormIm_nonneg f _)) _]

Premises used: Ne.le_iff_lt, Iff.mp, Complex.HadamardThreeLines.sSupNormIm_nonneg, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
simp only [sub_re, one_re, le_refl]

Premises used: le_refl, Complex.sub_re, Complex.one_re
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
⊢ ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re

Tactic:
have : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re := by
    by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
    · rw [interpStrip_eq_of_zero f z h, norm_zero, mul_nonneg_iff]
      left
      exact ⟨Real.rpow_nonneg (sSupNormIm_nonneg f _) _,
        Real.rpow_nonneg (sSupNormIm_nonneg f _) _ ⟩
    · rcases h with ⟨h0, h1⟩
      rw [ne_comm] at h0 h1
      simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]
      simp only [norm_mul]
      rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h0).mp (sSupNormIm_nonneg f _)) _]
      rw [norm_cpow_eq_rpow_re_of_pos ((Ne.le_iff_lt h1).mp (sSupNormIm_nonneg f _)) _]
      simp only [sub_re, one_re, le_refl]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
apply : sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re
⊢ ‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re

Tactic:
apply (norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ f hz hd hB).trans (this.trans _)

Premises used: Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip₀₁, LE.le.trans
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
apply : 0 ≤ b ^ z.re
apply₁ : sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)
apply₂ : sSupNormIm f 1 ^ z.re ≤ b ^ z.re
⊢ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re

Tactic:
apply mul_le_mul_of_nonneg _ _ (Real.rpow_nonneg (sSupNormIm_nonneg f _) _)

Premises used: mul_le_mul_of_nonneg, Real.rpow_nonneg, Complex.HadamardThreeLines.sSupNormIm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
apply : 0 ≤ b
⊢ 0 ≤ b ^ z.re

Tactic:
apply (Real.rpow_nonneg _ _)

Premises used: Real.rpow_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 1 ∈ re ⁻¹' {1} → ‖f 1‖ ≤ b

Tactic:
specialize hb 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
hb : 1 ∈ re ⁻¹' {1} → ‖f 1‖ ≤ b
⊢ ‖f 1‖ ≤ b

Tactic:
simp only [mem_preimage, one_re, mem_singleton_iff, forall_true_left] at hb

Premises used: forall_true_left, Set.mem_singleton_iff, Complex.one_re, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
hb : ‖f 1‖ ≤ b
⊢ 0 ≤ b

Tactic:
(norm_nonneg _).trans hb

Premises used: LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
hb : ‖f 1‖ ≤ b
⊢ 0 ≤ b

Tactic:
exact (norm_nonneg _).trans hb

Premises used: LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
h : 0 ≤ sSupNormIm f 0
h₂ : 0 ≤ 1 - z.re
h₁ : sSupNormIm f 0 ≤ a
⊢ sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ≤ sSupNormIm f 0

Tactic:
sSupNormIm_nonneg f _

Premises used: Complex.HadamardThreeLines.sSupNormIm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ≤ sSupNormIm f 0

Tactic:
exact sSupNormIm_nonneg f _

Premises used: Complex.HadamardThreeLines.sSupNormIm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ≤ 1 - z.re

Tactic:
sub_nonneg.mpr hz.2

Premises used: Iff.mpr, And.right, sub_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ≤ 1 - z.re

Tactic:
exact sub_nonneg.mpr hz.2

Premises used: Iff.mpr, And.right, sub_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
h₁ : ∀ b ∈ norm ∘ f '' re ⁻¹' {0}, b ≤ a
apply : (norm ∘ f '' re ⁻¹' {0}).Nonempty
⊢ sSup (norm ∘ f '' re ⁻¹' {0}) ≤ a

Tactic:
apply csSup_le _

Premises used: csSup_le
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ∀ b ∈ norm ∘ f '' re ⁻¹' {0}, b ≤ a

Tactic:
simpa [comp_apply, mem_image, forall_exists_index,
        and_imp, forall_apply_eq_imp_iff₂] using ha

Premises used: and_imp, Set.mem_image, forall_exists_index, Function.comp_apply, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
h : 0 ∈ re ⁻¹' {0} ∧ (norm ∘ f) 0 = ‖f 0‖
⊢ (norm ∘ f '' re ⁻¹' {0}).Nonempty

Tactic:
use ‖(f 0)‖, 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ∈ re ⁻¹' {0} ∧ (norm ∘ f) 0 = ‖f 0‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
apply : sSupNormIm f 1 ≤ b
⊢ sSupNormIm f 1 ^ z.re ≤ b ^ z.re

Tactic:
apply Real.rpow_le_rpow (sSupNormIm_nonneg f _) _ hz.1

Premises used: And.left, Real.rpow_le_rpow, Complex.HadamardThreeLines.sSupNormIm_nonneg