awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ z ∈ verticalClosedStrip 0 1

Tactic:
simp only [verticalClosedStrip, mem_preimage, zero_le_one, hz1, right_mem_Icc]

Premises used: Set.right_mem_Icc, zero_le_one, 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 : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
apply :
  ∃ c < Real.pi / HSub.hSub (α := ℝ) 1 0,
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (c * |z.im|))
⊢ ‖F f ε z‖ ≤ 1

Tactic:
apply PhragmenLindelof.vertical_strip
    (DiffContOnCl.smul (diffContOnCl_invInterpStrip f hε) hd) _
    (fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inl hx))
    (fun x hx ↦ F_edge_le_one f ε hε x hB (Or.inr hx)) hz.1 hz.2

Premises used: DiffContOnCl.smul, PhragmenLindelof.vertical_strip, Complex.HadamardThreeLines.F_edge_le_one, And.right, And.left, Or.inl, Complex.HadamardThreeLines.diffContOnCl_invInterpStrip, Or.inr
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
h :
  0 < Real.pi / HSub.hSub (α := ℝ) 1 0 ∧
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
⊢ ∃ c < Real.pi / HSub.hSub (α := ℝ) 1 0,
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (c * |z.im|))

Tactic:
use 0
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
h :
  0 < Real.pi ∧
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
⊢ 0 < Real.pi / HSub.hSub (α := ℝ) 1 0 ∧
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
rw [sub_zero, div_one]

Premises used: sub_zero, div_one
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
⊢ 0 < Real.pi ∧
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
⟨ Real.pi_pos, ?_⟩

Premises used: Real.pi_pos, And.intro
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
h :
  ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
⊢ 0 < Real.pi ∧
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
refine ⟨ Real.pi_pos, ?_⟩
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
h :
  ∀ (BF : ℝ) (hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)),
    ∃ (B : ℝ),
      Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
        (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))
⊢ ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
obtain ⟨BF, hBF⟩ := F_BddAbove f ε hε hB

Premises used: Complex.HadamardThreeLines.F_BddAbove
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : BF ∈ upperBounds (norm ∘ F f ε '' verticalClosedStrip 0 1)
⊢ ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF

Tactic:
simp only [comp_apply, mem_upperBounds, mem_image, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂] at hBF

Premises used: and_imp, Set.mem_image, forall_exists_index, Function.comp_apply, forall_apply_eq_imp_iff₂, mem_upperBounds
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
h :
  Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
    (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (BF * Real.exp (0 * |z.im|))
⊢ ∃ (B : ℝ),
    Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
      (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (B * Real.exp (0 * |z.im|))

Tactic:
use BF
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
h :
  ∃ (c : ℝ),
    ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
      ‖invInterpStrip f x ε • f x‖ ≤ c * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
⊢ Asymptotics.IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1))
    (fun (x : ℂ) ↦ invInterpStrip f x ε • f x) fun (z : ℂ) ↦ Real.exp (BF * Real.exp (0 * |z.im|))

Tactic:
rw [Asymptotics.isBigO_iff]

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
h :
  ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
    ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
      ‖invInterpStrip f x ε • f x‖ ≤ c * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖

Tactic:
use 1
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
h :
  ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop,
    x ∈ re ⁻¹' Ioo 0 1 → ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
⊢ ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
    ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖

Tactic:
rw [eventually_inf_principal]

Premises used: Filter.eventually_inf_principal
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
h : ∀ x ∈ re ⁻¹' Ioo 0 1, ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
⊢ ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop,
    x ∈ re ⁻¹' Ioo 0 1 → ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖

Tactic:
apply Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
x : ℂ
hx : x ∈ re ⁻¹' Ioo 0 1
⊢ ‖invInterpStrip f x ε • f x‖ ≤ 1 * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖

Tactic:
simpa using (hBF x ((preimage_mono Ioo_subset_Icc_self) hx)).trans
    ((le_of_lt (lt_add_one BF)).trans (Real.add_one_le_exp BF))

Premises used: Set.Ioo_subset_Icc_self, lt_add_one, le_of_lt, Set.preimage_mono, LE.le.trans, Real.add_one_le_exp
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
h0 : 0 < sSupNormIm f 0
h1 : 0 < sSupNormIm f 1
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

Tactic:
simp only [ne_of_gt h0, ne_of_gt h1, interpStrip, if_false, or_false]

Premises used: if_false, ne_of_gt, Complex.HadamardThreeLines.interpStrip, or_false
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ interpStrip f z = 0

Tactic:
if_pos h

Premises used: if_pos, Complex.HadamardThreeLines.interpStrip
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
pos :
  ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0),
    interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
neg :
  ∀ (h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0),
    interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

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
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
pos : 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

Tactic:
rw [interpStrip_eq_of_zero _ z h]

Premises used: Complex.HadamardThreeLines.interpStrip_eq_of_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
pos : ∀ (h0 : sSupNormIm f 0 = 0), 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
pos₁ : ∀ (h1 : sSupNormIm f 1 = 0), 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
⊢ 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

Tactic:
rcases h with h0 | h1
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
pos : ¬1 - z = 0 ∨ sSupNormIm f 1 = 0 ∧ ¬z = 0
⊢ 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

Tactic:
simp only [h0, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ne_eq, true_and, ofReal_eq_zero]

Premises used: zero_eq_mul, Complex.cpow_eq_zero_iff, ne_eq, Complex.ofReal_eq_zero, Complex.ofReal_zero, true_and
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
pos : ¬1 - z = 0
⊢ ¬1 - z = 0 ∨ sSupNormIm f 1 = 0 ∧ ¬z = 0

Tactic:
left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
pos : ¬z = 1
⊢ ¬1 - z = 0

Tactic:
rw [sub_eq_zero, eq_comm]

Premises used: sub_eq_zero, eq_comm
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ ¬z = 1

Tactic:
simp only [Complex.ext_iff, one_re, ne_of_lt hz.2, false_and, not_false_eq_true]

Premises used: false_and, Complex.ext_iff, And.right, not_false_eq_true, Complex.one_re, ne_of_lt
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
pos : sSupNormIm f 0 = 0 ∧ ¬1 - z = 0 ∨ ¬z = 0
⊢ 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

Tactic:
simp only [h1, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq, true_and]

Premises used: zero_eq_mul, Complex.cpow_eq_zero_iff, ne_eq, Complex.ofReal_eq_zero, Complex.ofReal_zero, true_and
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
pos : ¬z = 0
⊢ sSupNormIm f 0 = 0 ∧ ¬1 - z = 0 ∨ ¬z = 0

Tactic:
right
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
pos : ¬0 = z
⊢ ¬z = 0

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
⊢ ¬0 = z

Tactic:
simp only [Complex.ext_iff, zero_re, ne_of_lt hz.1, false_and, not_false_eq_true]

Premises used: false_and, Complex.ext_iff, And.left, Complex.zero_re, not_false_eq_true, ne_of_lt
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ 0 < sSupNormIm f 0 ∧ 0 < sSupNormIm f 1

Tactic:
replace h : (0 < sSupNormIm f 0) ∧ (0 < sSupNormIm f 1) :=
      ⟨(lt_of_le_of_ne (sSupNormIm_nonneg f 0) (ne_comm.mp h.1)),
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) (ne_comm.mp h.2))⟩
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : 0 < sSupNormIm f 0 ∧ 0 < sSupNormIm f 1
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

Tactic:
interpStrip_eq_of_pos f z h.1 h.2

Premises used: Complex.HadamardThreeLines.interpStrip_eq_of_pos, And.right, And.left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : 0 < sSupNormIm f 0 ∧ 0 < sSupNormIm f 1
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z

Tactic:
exact interpStrip_eq_of_pos f z h.1 h.2

Premises used: Complex.HadamardThreeLines.interpStrip_eq_of_pos, And.right, And.left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
pos : ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0), DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
neg : ∀ (h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0), DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

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
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
pos : DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) fun (a : ℂ) ↦ verticalStrip 0 1 a
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ interpStrip.{u_1} (E := E) (fun (a : ℂ) ↦ f a) z) fun (a : ℂ) ↦
    verticalStrip 0 1 a

Tactic:
simp_rw [interpStrip_eq_of_zero f _ h]

Premises used: Complex.HadamardThreeLines.interpStrip_eq_of_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) fun (a : ℂ) ↦ verticalStrip 0 1 a

Tactic:
diffContOnCl_const

Premises used: diffContOnCl_const
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) fun (a : ℂ) ↦ verticalStrip 0 1 a

Tactic:
exact diffContOnCl_const

Premises used: diffContOnCl_const
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
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
f : ℂ → E
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
f : ℂ → E
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
f : ℂ → E
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
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
neg : Differentiable ℂ (interpStrip f)
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)

Tactic:
apply Differentiable.diffContOnCl

Premises used: Differentiable.diffContOnCl
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z) z
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ interpStrip.{u_1} (E := E) (fun (a : ℂ) ↦ f a) z) z

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
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z) z

Tactic:
DifferentiableAt.mul ?_ ?_

Premises used: DifferentiableAt.mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z)) z
neg₁ : DifferentiableAt ℂ (HPow.hPow (↑(sSupNormIm f 1) : ℂ)) z
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z) z

Tactic:
refine DifferentiableAt.mul ?_ ?_

Premises used: DifferentiableAt.mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
apply : (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ 1 - id z ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z)) z

Tactic:
apply DifferentiableAt.const_cpow (DifferentiableAt.const_sub differentiableAt_id 1) _

Premises used: DifferentiableAt.const_cpow, DifferentiableAt.const_sub, OfNat.ofNat, differentiableAt_id
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
h : (↑(sSupNormIm f 0) : ℂ) ≠ 0
⊢ (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ 1 - id z ≠ 0

Tactic:
left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
h : ¬sSupNormIm f 0 = 0
⊢ (↑(sSupNormIm f 0) : ℂ) ≠ 0

Tactic:
simp only [Ne, ofReal_eq_zero]

Premises used: Ne, Complex.ofReal_eq_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
h h₁ h₂ h₃ : ¬0 = sSupNormIm f 0
⊢ ¬sSupNormIm f 0 = 0

Tactic:
rwa [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (HPow.hPow (↑(sSupNormIm f 1) : ℂ)) z

Tactic:
DifferentiableAt.const_cpow ?_ ?_

Premises used: DifferentiableAt.const_cpow
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x) z
neg₁ : (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ z ≠ 0
⊢ DifferentiableAt ℂ (HPow.hPow (↑(sSupNormIm f 1) : ℂ)) z

Tactic:
refine DifferentiableAt.const_cpow ?_ ?_

Premises used: DifferentiableAt.const_cpow
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x) z

Tactic:
apply differentiableAt_id

Premises used: differentiableAt_id
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg : (↑(sSupNormIm f 1) : ℂ) ≠ 0
⊢ (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ z ≠ 0

Tactic:
left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg : ¬sSupNormIm f 1 = 0
⊢ (↑(sSupNormIm f 1) : ℂ) ≠ 0

Tactic:
simp only [Ne, ofReal_eq_zero]

Premises used: Ne, Complex.ofReal_eq_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg neg₁ neg₂ neg₃ : ¬0 = sSupNormIm f 1
⊢ ¬sSupNormIm f 1 = 0

Tactic:
rwa [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
simp : ∀ (hz : 0 ≤ z.re ∧ z.re ≤ 1), l ≤ l + z.re * (u - l) ∧ l + z.re * (u - l) ≤ u
⊢ (↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalClosedStrip l u

Tactic:
simp only [verticalClosedStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im,
    ofReal_im, sub_self, mul_zero, sub_zero, mem_Icc] at hz ⊢

Premises used: Complex.mul_re, sub_self, Complex.sub_im, sub_zero, Complex.sub_re, Complex.add_re, MulZeroClass.mul_zero, Set.mem_Icc, Complex.ofReal_re, Complex.HadamardThreeLines.verticalClosedStrip, Complex.ofReal_im, Set.mem_preimage