awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
apply : (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), id x - 1 ≠ 0
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)

Tactic:
apply Differentiable.const_cpow (Differentiable.sub_const differentiable_id 1) _

Premises used: Differentiable.sub_const, differentiable_id, OfNat.ofNat, Differentiable.const_cpow
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), id x - 1 ≠ 0

Tactic:
left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : ε + sSupNormIm f 0 ≠ 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ) ≠ 0

Tactic:
rw [← ofReal_add, ofReal_ne_zero]

Premises used: Complex.ofReal_ne_zero, Complex.ofReal_add
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ε + sSupNormIm f 0 ≠ 0

Tactic:
simp only [ne_eq, ne_of_gt (sSupNormIm_eps_pos f hε 0), not_false_eq_true]

Premises used: ne_of_gt, ne_eq, Complex.HadamardThreeLines.sSupNormIm_eps_pos, OfNat.ofNat, not_false_eq_true
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), Ne (α := ℂ) ((-id) x : ℂ) (0 : ℂ)
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)

Tactic:
apply Differentiable.const_cpow (Differentiable.neg differentiable_id)

Premises used: Differentiable.neg, differentiable_id, Differentiable.const_cpow
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ ∀ (x : ℂ), Ne (α := ℂ) ((-id) x : ℂ) (0 : ℂ)

Tactic:
apply Or.inl

Premises used: Or.inl
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : ε + sSupNormIm f 1 ≠ 0
⊢ (↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ) ≠ 0

Tactic:
rw [← ofReal_add, ofReal_ne_zero]

Premises used: Complex.ofReal_ne_zero, Complex.ofReal_add
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ε + sSupNormIm f 1 ≠ 0

Tactic:
(ne_of_gt (sSupNormIm_eps_pos f hε 1))

Premises used: ne_of_gt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ ε + sSupNormIm f 1 ≠ 0

Tactic:
exact (ne_of_gt (sSupNormIm_eps_pos f hε 1))

Premises used: ne_of_gt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ sSupNormIm f z.re

Tactic:
le_csSup ?_ ?_

Premises used: Complex.HadamardThreeLines.sSupNormIm, le_csSup
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
refine_1 : BddAbove (norm ∘ f '' re ⁻¹' {z.re})
refine_2 : ‖f z‖ ∈ norm ∘ f '' re ⁻¹' {z.re}
⊢ ‖f z‖ ≤ sSupNormIm f z.re

Tactic:
refine le_csSup ?_ ?_

Premises used: le_csSup
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
refine_1 : ∀ (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), BddAbove (norm ∘ f '' re ⁻¹' {z.re})
⊢ BddAbove (norm ∘ f '' re ⁻¹' {z.re})

Tactic:
revert hB
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
refine_1 : re ⁻¹' {z.re} ⊆ verticalClosedStrip 0 1
⊢ ∀ (hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)), BddAbove (norm ∘ f '' re ⁻¹' {z.re})

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
⊢ re ⁻¹' {z.re} ⊆ verticalClosedStrip 0 1

Tactic:
preimage_mono (singleton_subset_iff.mpr hD)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.preimage_mono, Complex.HadamardThreeLines.verticalClosedStrip
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
⊢ re ⁻¹' {z.re} ⊆ verticalClosedStrip 0 1

Tactic:
exact preimage_mono (singleton_subset_iff.mpr hD)

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.preimage_mono
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
refine_2 : z ∈ re ⁻¹' {z.re}
⊢ ‖f z‖ ∈ norm ∘ f '' re ⁻¹' {z.re}

Tactic:
apply mem_image_of_mem (norm ∘ f)

Premises used: Norm.norm, Function.comp, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ z ∈ re ⁻¹' {z.re}

Tactic:
simp only [mem_preimage, mem_singleton]

Premises used: Set.mem_singleton, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ < ε + sSupNormIm f z.re

Tactic:
lt_add_of_pos_of_le hε (norm_le_sSupNormIm f z hD hB)

Premises used: Complex.HadamardThreeLines.norm_le_sSupNormIm, lt_add_of_pos_of_le
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
simp :
  BddAbove (α := ℝ)
    ((fun (a : ℂ) ↦
        ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
      verticalClosedStrip 0 1)
⊢ BddAbove (norm ∘ F f ε '' verticalClosedStrip 0 1)

Tactic:
simp only [F, comp_apply, invInterpStrip]

Premises used: Complex.HadamardThreeLines.invInterpStrip, Complex.HadamardThreeLines.F, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ∃ (x : ℝ), ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x

Tactic:
rw [bddAbove_def] at *

Premises used: bddAbove_def
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : ∃ (x : ℝ), ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x
rcases :
  ∀ (B : ℝ) (hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B),
    ∃ (x : ℝ),
      ∀ (y : ℝ),
        Membership.mem (γ := Set ℝ)
            ((fun (a : ℂ) ↦
                ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) •
                    f a‖) ''
              verticalClosedStrip 0 1)
            y →
          y ≤ x
⊢ ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ)
          ((fun (a : ℂ) ↦
              ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
            verticalClosedStrip 0 1)
          y →
        y ≤ x

Tactic:
rcases hB with ⟨B, hB⟩
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
h :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ)
        ((fun (a : ℂ) ↦
            ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1)
        y →
      y ≤
        max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
⊢ ∃ (x : ℝ),
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ)
          ((fun (a : ℂ) ↦
              ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
            verticalClosedStrip 0 1)
          y →
        y ≤ x

Tactic:
use ((max 1 ((ε + sSupNormIm f 0) ^ (-(1 : ℝ)))) * max 1 ((ε + sSupNormIm f 1) ^ (-(1 : ℝ)))) * B

Premises used: HMul.hMul, Complex.HadamardThreeLines.sSupNormIm, HPow.hPow, HAdd.hAdd, Max.max, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
h :
  ∀ a ∈ verticalClosedStrip 0 1,
    ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖ ≤
      max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
⊢ ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ)
        ((fun (a : ℂ) ↦
            ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (a - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1)
        y →
      y ≤
        max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: and_imp, Set.mem_image, forall_exists_index, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ∈ norm ∘ f '' verticalClosedStrip 0 1

Tactic:
simpa [image_congr, mem_image, comp_apply] using ⟨z, hset, rfl⟩

Premises used: Set.mem_image, Set.image_congr, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
hB : ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ B
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ B

Tactic:
specialize hB (‖f z‖) (by simpa [image_congr, mem_image, comp_apply] using ⟨z, hset, rfl⟩)

Premises used: Norm.norm
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
h :
  ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ * ‖f z‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B
⊢ ‖(((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1) * ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)) • f z‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B

Tactic:
simp only [norm_smul, norm_mul, ← ofReal_add]

Premises used: norm_smul, Complex.ofReal_add, norm_mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
h : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
h₁ : ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ * ‖f z‖ ≤
    max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)) * max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)) * B

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
pos :
  ∀ (hM0_one : 1 ≤ ε + sSupNormIm f 0),
    ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
neg :
  ∀ (hM0_one : ¬1 ≤ ε + sSupNormIm f 0),
    ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))

Tactic:
by_cases hM0_one : 1 ≤ ε + sSupNormIm f 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
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : 1 ≤ ε + sSupNormIm f 0
apply : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ 1
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))

Tactic:
apply le_trans _ (le_max_left _ _)

Premises used: le_max_left, le_trans
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : 1 ≤ ε + sSupNormIm f 0
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ 1

Tactic:
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re,
        one_re, Real.rpow_le_one_of_one_le_of_nonpos hM0_one (sub_nonpos.mpr hset.2)]

Premises used: Iff.mpr, Complex.sub_re, Complex.HadamardThreeLines.sSupNormIm_eps_pos, And.right, Real.rpow_le_one_of_one_le_of_nonpos, sub_nonpos, OfNat.ofNat, Complex.one_re, 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
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ¬1 ≤ ε + sSupNormIm f 0
⊢ ε + sSupNormIm f 0 < 1

Tactic:
rw [not_le] at hM0_one

Premises used: not_le
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
apply : ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1))

Tactic:
apply le_trans _ (le_max_right _ _)

Premises used: le_max_right, le_trans
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
simp : (ε + sSupNormIm f 0) ^ (z.re - 1) ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)

Tactic:
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 0), sub_re,
        one_re]

Premises used: Complex.sub_re, Complex.HadamardThreeLines.sSupNormIm_eps_pos, OfNat.ofNat, Complex.one_re, 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
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
apply : -1 ≤ z.re - 1
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 0) (-1)

Tactic:
apply Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 0) (le_of_lt hM0_one) _

Premises used: le_of_lt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, Real.rpow_le_rpow_of_exponent_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM0_one : ε + sSupNormIm f 0 < 1
⊢ -1 ≤ z.re - 1

Tactic:
simp only [neg_le_sub_iff_le_add, le_add_iff_nonneg_left, hset.1]

Premises used: And.left, neg_le_sub_iff_le_add, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
pos :
  ∀ (hM1_one : 1 ≤ ε + sSupNormIm f 1),
    ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
neg :
  ∀ (hM1_one : ¬1 ≤ ε + sSupNormIm f 1),
    ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))
⊢ ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))

Tactic:
by_cases hM1_one : 1 ≤ ε + sSupNormIm f 1

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
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : 1 ≤ ε + sSupNormIm f 1
apply : ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ 1
⊢ ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))

Tactic:
apply le_trans _ (le_max_left _ _)

Premises used: le_max_left, le_trans
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : 1 ≤ ε + sSupNormIm f 1
⊢ ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ 1

Tactic:
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_one_of_one_le_of_nonpos
        hM1_one (Right.neg_nonpos_iff.mpr hset.1)]

Premises used: Iff.mpr, Right.neg_nonpos_iff, Complex.HadamardThreeLines.sSupNormIm_eps_pos, And.left, Complex.neg_re, Real.rpow_le_one_of_one_le_of_nonpos, OfNat.ofNat, 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
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : ¬1 ≤ ε + sSupNormIm f 1
⊢ ε + sSupNormIm f 1 < 1

Tactic:
rw [not_le] at hM1_one

Premises used: not_le
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : ε + sSupNormIm f 1 < 1
apply : ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)
⊢ ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ max 1 (HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1))

Tactic:
apply le_trans _ (le_max_right _ _)

Premises used: le_max_right, le_trans
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
B : ℝ
z : ℂ
hset : z ∈ verticalClosedStrip 0 1
hB : ‖f z‖ ≤ B
hM1_one : ε + sSupNormIm f 1 < 1
⊢ ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ ≤ HPow.hPow (β := ℝ) (ε + sSupNormIm f 1) (-1)

Tactic:
simp only [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε 1),
        neg_re, Real.rpow_le_rpow_of_exponent_ge (sSupNormIm_eps_pos f hε 1)
        (le_of_lt hM1_one) (neg_le_neg_iff.mpr hset.2)]

Premises used: Iff.mpr, le_of_lt, Complex.HadamardThreeLines.sSupNormIm_eps_pos, And.right, Complex.neg_re, Real.rpow_le_rpow_of_exponent_ge, OfNat.ofNat, Complex.norm_cpow_eq_rpow_re_of_pos, neg_le_neg_iff
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
simp : (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
⊢ ‖F f ε z‖ ≤ 1

Tactic:
simp only [F, norm_smul, norm_invInterpStrip f z hε]

Premises used: norm_smul, Complex.HadamardThreeLines.norm_invInterpStrip, Complex.HadamardThreeLines.F
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ re ⁻¹' {0, 1}
inl : ∀ (hz0 : z.re = 0), (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
inr :
  ∀ (hz1 : Membership.mem (γ := Set ℝ) {1} z.re),
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1

Tactic:
rcases hz with hz0 | hz1
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
inl : ‖f z‖ ≤ ε + sSupNormIm f 0
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1

Tactic:
simp only [hz0, zero_sub, Real.rpow_neg_one, neg_zero, Real.rpow_zero, mul_one,
      inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 0)]

Premises used: Real.rpow_neg_one, Real.rpow_zero, Complex.HadamardThreeLines.sSupNormIm_eps_pos, inv_mul_le_iff₀, mul_one, OfNat.ofNat, neg_zero, zero_sub
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
inl : ‖f z‖ ≤ ε + sSupNormIm f z.re
⊢ ‖f z‖ ≤ ε + sSupNormIm f 0

Tactic:
rw [← hz0]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
apply : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ ε + sSupNormIm f z.re

Tactic:
apply le_of_lt (norm_lt_sSupNormIm_eps f ε hε _ _ hB)

Premises used: le_of_lt, Complex.HadamardThreeLines.norm_lt_sSupNormIm_eps
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz0 : z.re = 0
⊢ z ∈ verticalClosedStrip 0 1

Tactic:
simp only [verticalClosedStrip, mem_preimage, zero_le_one, left_mem_Icc, hz0]

Premises used: zero_le_one, Set.left_mem_Icc, Complex.HadamardThreeLines.verticalClosedStrip, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : Membership.mem (γ := Set ℝ) {1} z.re
⊢ z.re = 1

Tactic:
rw [mem_singleton_iff] at hz1

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
inr : ‖f z‖ ≤ ε + sSupNormIm f 1
⊢ (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re) * ‖f z‖ ≤ 1

Tactic:
simp only [hz1, one_mul, Real.rpow_zero, sub_self, Real.rpow_neg_one,
      inv_mul_le_iff₀ (sSupNormIm_eps_pos f hε 1), mul_one]

Premises used: Real.rpow_neg_one, sub_self, Real.rpow_zero, Complex.HadamardThreeLines.sSupNormIm_eps_pos, inv_mul_le_iff₀, mul_one, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
inr : ‖f z‖ ≤ ε + sSupNormIm f z.re
⊢ ‖f z‖ ≤ ε + sSupNormIm f 1

Tactic:
rw [← hz1]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
apply : z ∈ verticalClosedStrip 0 1
⊢ ‖f z‖ ≤ ε + sSupNormIm f z.re

Tactic:
apply le_of_lt (norm_lt_sSupNormIm_eps f ε hε _ _ hB)

Premises used: le_of_lt, Complex.HadamardThreeLines.norm_lt_sSupNormIm_eps