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 : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
ε : ℝ
h : ∀ (hε : 0 < ε), ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) ε →
    ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖

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

Tactic:
norm_le_interpStrip_of_mem_verticalClosedStrip_eps f ε hε z hB hd
      (mem_of_mem_of_subset hz (preimage_mono Ioo_subset_Icc_self))

Premises used: Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip_eps, Set.Ioo_subset_Icc_self, Set.preimage_mono, Set.mem_of_mem_of_subset
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
inst_1 : NormedSpace ℂ E
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) (Ioi 0) x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  LE.le (α := ℝ) ((fun (x : ℝ) ↦ ‖f z‖) x)
                    ((fun (ε : ℝ) ↦
                        ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
                      x))
                x}
            x}
      a
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      ‖f z‖ ≤ ‖((↑a : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑a : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
h₂ :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ‖f z‖ ≤ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ ‖f z‖) fun (ε : ℝ) ↦
    ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖

Tactic:
filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε) using
    norm_le_interpStrip_of_mem_verticalClosedStrip_eps f ε hε z hB hd
      (mem_of_mem_of_subset hz (preimage_mono Ioo_subset_Icc_self))

Premises used: self_mem_nhdsWithin
-- 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
apply : Tendsto (fun (x : ℝ) ↦ ‖f z‖) (𝓝[>] 0) (𝓝 ‖f z‖)
apply₁ :
  Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖interpStrip f z‖)
⊢ ‖f z‖ ≤ ‖interpStrip f z‖

Tactic:
apply tendsto_le_of_eventuallyLE _ _ (eventuallyle f z hB hd hz)

Premises used: tendsto_le_of_eventuallyLE, Complex.HadamardThreeLines.eventuallyle
-- 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
⊢ Tendsto (fun (x : ℝ) ↦ ‖f z‖) (𝓝[>] 0) (𝓝 ‖f z‖)

Tactic:
simp only [tendsto_const_nhds_iff]

Premises used: tendsto_const_nhds_iff
-- 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
rw :
  Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
⊢ Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖interpStrip f z‖)

Tactic:
rw [interpStrip_eq_of_mem_verticalStrip _ _ hz]

Premises used: Complex.HadamardThreeLines.interpStrip_eq_of_mem_verticalStrip
-- 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
⊢ Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖((↑0 : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑0 : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)

Tactic:
ContinuousWithinAt.tendsto _

Premises used: ContinuousWithinAt.tendsto
-- 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
h :
  ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ =
    ‖((↑0 : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑0 : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖
convert_8 :
  ContinuousWithinAt (Y := ℝ)
    (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖) (Ioi 0)
    0
⊢ Tendsto (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖)
    (𝓝[>] 0) (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)

Tactic:
convert! ContinuousWithinAt.tendsto _ using 2

Premises used: ContinuousWithinAt.tendsto
-- 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
⊢ ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖ =
    ‖((↑0 : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑0 : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖

Tactic:
simp only [ofReal_zero, zero_add]

Premises used: zero_add, Complex.ofReal_zero
-- 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
convert_8 :
  ContinuousWithinAt (Y := ℝ) (fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖)
    (Ioi 0) 0
⊢ ContinuousWithinAt (Y := ℝ)
    (fun (ε : ℝ) ↦ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (1 - z) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ z‖) (Ioi 0)
    0

Tactic:
simp_rw [← ofReal_add]

Premises used: Complex.ofReal_add
-- 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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
simp :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(x + sSupNormIm f 1) : ℂ) ^ z‖

Tactic:
simp only [norm_mul]

Premises used: norm_mul
-- 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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖
rw₁ : (1 - z).re ≠ 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖

Tactic:
rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]

Premises used: le_of_lt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.norm_cpow_eq_rpow_re_of_nonneg
-- 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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re
rw₁ : z.re ≠ 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖

Tactic:
rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]

Premises used: le_of_lt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.norm_cpow_eq_rpow_re_of_nonneg
-- 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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
repeat :
  (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    (x + sSupNormIm f 0) ^ (1 - z).re * (x + sSupNormIm f 1) ^ z.re
repeat₁ : z.re ≠ 0
repeat₂ : (1 - z).re ≠ 0
⊢ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
    ‖(↑(x + sSupNormIm f 0) : ℂ) ^ (1 - z)‖ * ‖(↑(x + sSupNormIm f 1) : ℂ) ^ z‖

Tactic:
repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]

Premises used: le_of_lt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.norm_cpow_eq_rpow_re_of_nonneg
-- 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
x : ℝ
hx : 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).re * (x + sSupNormIm f 1) ^ z.re

Tactic:
simp only [sub_re, one_re]

Premises used: Complex.sub_re, Complex.one_re
-- 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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 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
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (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
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
⊢ ∀ (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‖

Tactic:
have : ∀ x ∈ Ioi 0, (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re
          = ‖((x + sSupNormIm f 0 : ℝ) ^ (1 - z) * (x + sSupNormIm f 1 : ℝ) ^ z : ℂ)‖ := by
              intro x hx
              simp only [norm_mul]
              repeat rw [norm_cpow_eq_rpow_re_of_nonneg (le_of_lt (sSupNormIm_eps_pos f hx _)) _]
              · simp only [sub_re, one_re]
              · simpa using (ne_comm.mpr (ne_of_lt hz.1))
              · simpa [sub_eq_zero] using (ne_comm.mpr (ne_of_lt hz.2))
-- 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‖
apply :
  Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ((fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖) 0))
⊢ ContinuousWithinAt (Y := ℝ) (fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖)
    (Ioi 0) 0

Tactic:
apply tendsto_nhdsWithin_congr this _

Premises used: tendsto_nhdsWithin_congr
-- 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‖
simp :
  Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ((fun (ε : ℝ) ↦ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(ε + sSupNormIm f 1) : ℂ) ^ z‖) 0))

Tactic:
simp only [zero_add]

Premises used: zero_add
-- 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‖
rw :
  Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))
rw₁ : z.re ≠ 0
rw₂ : (1 - z).re ≠ 0
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 ‖(↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z‖)

Tactic:
rw [norm_mul, norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _,
        norm_cpow_eq_rpow_re_of_nonneg (sSupNormIm_nonneg _ _) _]

Premises used: norm_mul, Complex.norm_cpow_eq_rpow_re_of_nonneg, Complex.HadamardThreeLines.sSupNormIm_nonneg
-- 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‖
hf : Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re)) (𝓝[>] 0) (𝓝 (sSupNormIm f 0 ^ (1 - z).re))
hg : Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0) (𝓝 (sSupNormIm f 1 ^ z.re))
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0)
    (𝓝 (sSupNormIm f 0 ^ (1 - z).re * sSupNormIm f 1 ^ z.re))

Tactic:
apply Tendsto.mul

Premises used: Filter.Tendsto.mul
-- 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‖
hf : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (sSupNormIm f 0))
hf₁ : sSupNormIm f 0 ≠ 0 ∨ 0 ≤ 1 - z.re
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 0) ^ (1 - z.re)) (𝓝[>] 0) (𝓝 (sSupNormIm f 0 ^ (1 - z).re))

Tactic:
apply Tendsto.rpow_const

Premises used: Filter.Tendsto.rpow_const
-- 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‖
hf : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 0))
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (sSupNormIm f 0))

Tactic:
nth_rw 2 [← zero_add (sSupNormIm f 0)]

Premises used: zero_add, Complex.HadamardThreeLines.sSupNormIm, OfNat.ofNat
-- 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‖
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 0))

Tactic:
Tendsto.add_const (sSupNormIm f 0) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))

Premises used: continuous_id', Continuous.tendsto, tendsto_nhdsWithin_of_tendsto_nhds, Complex.HadamardThreeLines.sSupNormIm, Filter.Tendsto.add_const, OfNat.ofNat
-- 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‖
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 0))

Tactic:
exact Tendsto.add_const (sSupNormIm f 0) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))

Premises used: continuous_id', Continuous.tendsto, tendsto_nhdsWithin_of_tendsto_nhds, Complex.HadamardThreeLines.sSupNormIm, Filter.Tendsto.add_const, OfNat.ofNat
-- 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‖
hf : 0 ≤ 1 - z.re
⊢ sSupNormIm f 0 ≠ 0 ∨ 0 ≤ 1 - 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 ≤ 1 - z.re

Tactic:
simp only [sub_nonneg, le_of_lt hz.2]

Premises used: le_of_lt, And.right, sub_nonneg
-- 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 : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (sSupNormIm f 1))
hg₁ : sSupNormIm f 1 ≠ 0 ∨ 0 ≤ z.re
⊢ Tendsto (fun (x : ℝ) ↦ (x + sSupNormIm f 1) ^ z.re) (𝓝[>] 0) (𝓝 (sSupNormIm f 1 ^ z.re))

Tactic:
apply Tendsto.rpow_const

Premises used: Filter.Tendsto.rpow_const
-- 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 : Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 1))
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (sSupNormIm f 1))

Tactic:
nth_rw 2 [← zero_add (sSupNormIm f 1)]

Premises used: zero_add, Complex.HadamardThreeLines.sSupNormIm, OfNat.ofNat
-- 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‖
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 1))

Tactic:
Tendsto.add_const (sSupNormIm f 1) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))

Premises used: continuous_id', Continuous.tendsto, tendsto_nhdsWithin_of_tendsto_nhds, Complex.HadamardThreeLines.sSupNormIm, Filter.Tendsto.add_const, OfNat.ofNat
-- 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‖
⊢ Tendsto (fun (a : ℝ) ↦ a + sSupNormIm f 1) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 1))

Tactic:
exact Tendsto.add_const (sSupNormIm f 1) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))

Premises used: continuous_id', Continuous.tendsto, tendsto_nhdsWithin_of_tendsto_nhds, Complex.HadamardThreeLines.sSupNormIm, Filter.Tendsto.add_const, OfNat.ofNat