awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
obtain : ∀ (d : ℝ) (hd : d < π / 2 / b) (hcd : c < d) (hd₀ : 0 < d), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
obtain ⟨d, ⟨hcd, hd₀⟩, hd⟩ : ∃ d, (c < d ∧ 0 < d) ∧ d < π / 2 / b := by
    simpa only [max_lt_iff] using exists_between (max_lt hc hπb)
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
⊢ d * b < π / 2

Tactic:
have hb' : d * b < π / 2 := (lt_div_iff₀ hb).1 hd
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖g ε z • f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this

Premises used: le_of_tendsto, nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖g ε z • f z‖ ≤ C
refine : Tendsto (fun (c : ℝ) ↦ ‖g c z • f z‖) (𝓝 0) (𝓝 ‖f z‖)
⊢ ‖f z‖ ≤ C

Tactic:
refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this

Premises used: le_of_tendsto, nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖g ε z • f z‖ ≤ C
h : ‖cexp (HMul.hMul (β := ℝ → ℂ) ofReal (fun (x : ℝ) ↦ cexp (aff z) + cexp (-aff z)) 0) • f z‖ = ‖f z‖
⊢ Tendsto (fun (c : ℝ) ↦ ‖g c z • f z‖) (𝓝 0) (𝓝 ‖f z‖)

Tactic:
apply ((continuous_ofReal.mul continuous_const).cexp.smul continuous_const).norm.tendsto'

Premises used: continuous_const, Continuous.cexp, Continuous.norm, Continuous.mul, Continuous.smul, Complex.continuous_ofReal, Continuous.tendsto'
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖g ε z • f z‖ ≤ C
⊢ ‖cexp (HMul.hMul (β := ℝ → ℂ) ofReal (fun (x : ℝ) ↦ cexp (aff z) + cexp (-aff z)) 0) • f z‖ = ‖f z‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
suffices : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖g ε z • f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
suffices ∀ᶠ ε : ℝ in 𝓝[<] (0 : ℝ), ‖g ε z • f z‖ ≤ C by
    refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
    apply ((continuous_ofReal.mul continuous_const).cexp.smul continuous_const).norm.tendsto'
    simp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
h : ∀ (ε : ℝ) (ε₀ : Membership.mem (γ := Set ℝ) (Iio 0) ε), ‖g ε z • f z‖ ≤ C
⊢ ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖g ε z • f z‖ ≤ C

Tactic:
filter_upwards [self_mem_nhdsWithin] with ε ε₀

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : Membership.mem (γ := Set ℝ) (Iio 0) ε
⊢ ε < 0

Tactic:
change ε < 0 at ε₀
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
⊢ ∃ δ < 0, ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))

Tactic:
⟨ε * Real.cos (d * b),
        mul_neg_of_neg_of_pos ε₀
          (Real.cos_pos_of_mem_Ioo <| abs_lt.1 <| (abs_of_pos (mul_pos hd₀ hb)).symm ▸ hb'),
        fun w hw => ?_⟩

Premises used: mul_neg_of_neg_of_pos, HMul.hMul, Real.cos, Eq.rec, Real.cos_pos_of_mem_Ioo, mul_pos, And.intro, Exists.intro, Iff.mp, abs_lt, abs_of_pos, Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
mul_neg_of_neg_of_pos :
  ∀ (w : ℂ) (hw : w.im ∈ Icc (a - b) (a + b)), ‖g ε w‖ ≤ expR (ε * Real.cos (d * b) * expR (d * |w.re|))
⊢ ∃ δ < 0, ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))

Tactic:
refine
      ⟨ε * Real.cos (d * b),
        mul_neg_of_neg_of_pos ε₀
          (Real.cos_pos_of_mem_Ioo <| abs_lt.1 <| (abs_of_pos (mul_pos hd₀ hb)).symm ▸ hb'),
        fun w hw => ?_⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : w.im ∈ Icc (a - b) (a + b)
⊢ |w.im - a| ≤ b

Tactic:
rw [← Real.closedBall_eq_Icc, mem_closedBall, Real.dist_eq] at hw

Premises used: Real.closedBall_eq_Icc, Real.dist_eq, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : |w.im - a| ≤ b
rw : d * |w.im - a| ≤ d * b
⊢ |(aff w).im| ≤ d * b

Tactic:
rw [im_ofReal_mul, sub_im, mul_I_im, ofReal_re, _root_.abs_mul, abs_of_pos hd₀]

Premises used: Complex.sub_im, abs_mul, Complex.im_ofReal_mul, Complex.ofReal_re, abs_of_pos, Complex.mul_I_im
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : |w.im - a| ≤ b
ha : 0 ≤ d
⊢ d * |w.im - a| ≤ d * b

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : w.im ∈ Icc (a - b) (a + b)
⊢ |(aff w).im| ≤ d * b

Tactic:
replace hw : |im (aff w)| ≤ d * b := by
      rw [← Real.closedBall_eq_Icc, mem_closedBall, Real.dist_eq] at hw
      rw [im_ofReal_mul, sub_im, mul_I_im, ofReal_re, _root_.abs_mul, abs_of_pos hd₀]
      gcongr
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : |(aff w).im| ≤ d * b
⊢ ‖g ε w‖ ≤ expR (ε * Real.cos (d * b) * expR (d * |w.re|))

Tactic:
simpa only [aff, re_ofReal_mul, _root_.abs_mul, abs_of_pos hd₀, sub_re, mul_I_re, ofReal_im,
      zero_mul, neg_zero, sub_zero] using
      norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le ε₀.le hw hb'.le

Premises used: sub_zero, MulZeroClass.zero_mul, Complex.sub_re, abs_mul, LT.lt.le, Complex.mul_I_re, Complex.norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le, Complex.ofReal_im, abs_of_pos, neg_zero, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
h :
  ∀ (δ : ℝ) (δ₀ : δ < 0) (hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))),
    ‖g ε z • f z‖ ≤ C
⊢ ‖g ε z • f z‖ ≤ C

Tactic:
obtain ⟨δ, δ₀, hδ⟩ :
    ∃ δ : ℝ,
      δ < 0 ∧ ∀ ⦃w⦄, im w ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |re w|)) := by
    refine
      ⟨ε * Real.cos (d * b),
        mul_neg_of_neg_of_pos ε₀
          (Real.cos_pos_of_mem_Ioo <| abs_lt.1 <| (abs_of_pos (mul_pos hd₀ hb)).symm ▸ hb'),
        fun w hw => ?_⟩
    replace hw : |im (aff w)| ≤ d * b := by
      rw [← Real.closedBall_eq_Icc, mem_closedBall, Real.dist_eq] at hw
      rw [im_ofReal_mul, sub_im, mul_I_im, ofReal_re, _root_.abs_mul, abs_of_pos hd₀]
      gcongr
    simpa only [aff, re_ofReal_mul, _root_.abs_mul, abs_of_pos hd₀, sub_re, mul_I_re, ofReal_im,
      zero_mul, neg_zero, sub_zero] using
      norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le ε₀.le hw hb'.le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
⊢ ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1

Tactic:
fun w hw => (hδ <| hw.by_cases ?_ ?_).trans (Real.exp_le_one_iff.2 ?_)

Premises used: Iff.mpr, Or.by_cases, Real.exp_le_one_iff, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
refine_1 : ∀ (w : ℂ) (hw : w.im = a - b ∨ w.im = a + b), w.im = a - b → w.im ∈ Icc (a - b) (a + b)
refine_2 : ∀ (w : ℂ) (hw : w.im = a - b ∨ w.im = a + b), w.im = a + b → w.im ∈ Icc (a - b) (a + b)
refine_3 : ∀ (w : ℂ) (hw : w.im = a - b ∨ w.im = a + b), δ * expR (d * |w.re|) ≤ 0
⊢ ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1

Tactic:
refine fun w hw => (hδ <| hw.by_cases ?_ ?_).trans (Real.exp_le_one_iff.2 ?_)

Premises used: Iff.mpr, Real.exp_le_one_iff, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
w : ℂ
hw : w.im = a - b ∨ w.im = a + b
⊢ w.im = a - b → w.im ∈ Icc (a - b) (a + b)

Tactic:
fun h => h.symm ▸ left_mem_Icc.2 hab.le

Premises used: Iff.mpr, Eq.rec, LT.lt.le, Set.left_mem_Icc, Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
w : ℂ
hw : w.im = a - b ∨ w.im = a + b
⊢ w.im = a + b → w.im ∈ Icc (a - b) (a + b)

Tactic:
fun h => h.symm ▸ right_mem_Icc.2 hab.le

Premises used: Iff.mpr, Set.right_mem_Icc, Eq.rec, LT.lt.le, Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C_1 : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO :
  IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : (w : ℂ) → ℂ := fun (w : ℂ) ↦ (↑d : ℂ) * (w - (↑a : ℂ) * I)
g : (ε : ℝ) → (w : ℂ) → ℂ := fun (ε : ℝ) (w : ℂ) ↦ cexp ((↑ε : ℂ) * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
w : ℂ
hw : w.im = a - b ∨ w.im = a + b
⊢ δ * expR (d * |w.re|) ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg δ₀.le (Real.exp_pos _).le

Premises used: mul_nonpos_of_nonpos_of_nonneg, LT.lt.le, Real.exp_pos