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 : ℝ
f : ℂ → E
z_1 : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
z : ℂ
rw : ‖cexp ((↑ε : ℂ) * z)‖ * ‖f z‖ = expR (ε * z.re) * ‖f z‖
rw₁ : expR ((↑ε : ℂ) * z).re * ‖f z‖ = expR (ε * z.re) * ‖f z‖
rw₂ rw₃ : expR (ε * z.re) * ‖f z‖ = expR (ε * z.re) * ‖f z‖
⊢ ‖g z‖ = expR (ε * z.re) * ‖f z‖

Tactic:
rw [norm_smul, norm_exp, re_ofReal_mul]

Premises used: norm_smul, Complex.norm_exp, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
⊢ ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖

Tactic:
have hgn : ∀ z, ‖g z‖ = expR (ε * z.re) * ‖f z‖ := fun z ↦ by
    rw [norm_smul, norm_exp, re_ofReal_mul]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ ‖g z‖ ≤ C

Tactic:
right_half_plane_of_tendsto_zero_on_real hd ?_ ?_ (fun y => ?_) hz

Premises used: PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
h₁ : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g (↑x : ℂ)) atTop (𝓝 0)
h₂ : ∀ (y : ℝ), ‖g ((↑y : ℂ) * I)‖ ≤ C
⊢ ‖g z‖ ≤ C

Tactic:
refine right_half_plane_of_tendsto_zero_on_real hd ?_ ?_ (fun y => ?_) hz

Premises used: PhragmenLindelof.right_half_plane_of_tendsto_zero_on_real
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h :
  ∀ (c : ℝ) (hc : c < 2) (B : ℝ)
    (hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)),
    ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
rcases hexp with ⟨c, hc, B, hO⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
⟨c, hc, B, .trans (.of_bound' ?_) hO⟩

Premises used: Asymptotics.IsBigO.trans, And.intro, Exists.intro, Asymptotics.IsBigO.of_bound'
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
h : ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}, ‖g x‖ ≤ ‖f x‖
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
refine ⟨c, hc, B, .trans (.of_bound' ?_) hO⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
⊢ ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}, ‖g x‖ ≤ ‖f x‖

Tactic:
eventually_inf_principal.2 <| Eventually.of_forall fun z hz => ?_

Premises used: Filter.eventually_inf_principal, Iff.mpr, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
h : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z), ‖g z‖ ≤ ‖f z‖
⊢ ∀ᶠ (x : ℂ) in cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}, ‖g x‖ ≤ ‖f x‖

Tactic:
refine eventually_inf_principal.2 <| Eventually.of_forall fun z hz => ?_

Premises used: Filter.eventually_inf_principal, Iff.mpr, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z_1 : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_1 : 0 ≤ z_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z
h : expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖
⊢ ‖g z‖ ≤ ‖f z‖

Tactic:
rw [hgn]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z_1 : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_1 : 0 ≤ z_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z
⊢ expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖

Tactic:
mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 ?_)

Premises used: Iff.mpr, mul_le_of_le_one_left, Real.exp_le_one_iff, norm_nonneg
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z_1 : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_1 : 0 ≤ z_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z
h : ε * z.re ≤ 0
⊢ expR (ε * z.re) * ‖f z‖ ≤ ‖f z‖

Tactic:
refine mul_le_of_le_one_left (norm_nonneg _) (Real.exp_le_one_iff.2 ?_)

Premises used: Iff.mpr, mul_le_of_le_one_left, Real.exp_le_one_iff, norm_nonneg
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z_1 : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_1 : 0 ≤ z_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z
⊢ ε * z.re ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg ε₀.le (le_of_lt hz)

Premises used: mul_nonpos_of_nonpos_of_nonneg, le_of_lt, LT.lt.le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z_1 : ℂ
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz_1 : 0 ≤ z_1.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
c : ℝ
hc : c < 2
B : ℝ
hO : IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.re} z
⊢ ε * z.re ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg ε₀.le (le_of_lt hz)

Premises used: mul_nonpos_of_nonpos_of_nonneg, le_of_lt, LT.lt.le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ expR (ε * x) • f (↑x : ℂ)) atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ g (↑x : ℂ)) atTop (𝓝 0)

Tactic:
simp_rw [g, ← ofReal_mul, ← ofReal_exp, coe_smul]

Premises used: Complex.ofReal_exp, Complex.coe_smul, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ expR (ε * x)) atTop (𝓝 0)

Tactic:
have h₀ : Tendsto (fun x : ℝ => expR (ε * x)) atTop (𝓝 0) :=
      Real.tendsto_exp_atBot.comp (tendsto_const_nhds.neg_mul_atTop ε₀ tendsto_id)
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h₀ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ expR (ε * x)) atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ expR (ε * x) • f (↑x : ℂ)) atTop (𝓝 0)

Tactic:
h₀.zero_smul_isBoundedUnder_le hre

Premises used: Filter.Tendsto.zero_smul_isBoundedUnder_le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h₀ : Tendsto (β := ℝ) (fun (x : ℝ) ↦ expR (ε * x)) atTop (𝓝 0)
⊢ Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ expR (ε * x) • f (↑x : ℂ)) atTop (𝓝 0)

Tactic:
exact h₀.zero_smul_isBoundedUnder_le hre

Premises used: Filter.Tendsto.zero_smul_isBoundedUnder_le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
h : ‖f ((↑y : ℂ) * I)‖ ≤ C
⊢ ‖g ((↑y : ℂ) * I)‖ ≤ C

Tactic:
rw [hgn, re_ofReal_mul, I_re, mul_zero, mul_zero, Real.exp_zero,
      one_mul]

Premises used: Complex.I_re, MulZeroClass.mul_zero, Real.exp_zero, one_mul, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖f ((↑y : ℂ) * I)‖ ≤ C

Tactic:
him y
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun (z : ℂ) ↦ cexp ((↑ε : ℂ) * z) • f z
hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
y : ℝ
⊢ ‖f ((↑y : ℂ) * I)‖ ≤ C

Tactic:
exact him y
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
rcases : ∀ (C : ℝ) (hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C), EqOn f 0 {z : ℂ | 0 ≤ z.re}
⊢ EqOn f 0 {z : ℂ | 0 ≤ z.re}

Tactic:
rcases him with ⟨C, hC⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
this : ∀ (z : ℂ), 0 < z.re → f z = 0
⊢ EqOn f 0 {z : ℂ | 0 ≤ z.re}

Tactic:
simpa only [closure_setOf_lt_re] using
      EqOn.of_subset_closure this hd.continuousOn continuousOn_const subset_closure Subset.rfl

Premises used: Set.EqOn.of_subset_closure, subset_closure, continuousOn_const, Set.Subset.rfl, Complex.closure_setOf_lt_re, DiffContOnCl.continuousOn
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
suffices : ∀ (z : ℂ), 0 < z.re → f z = 0
⊢ EqOn f 0 {z : ℂ | 0 ≤ z.re}

Tactic:
suffices ∀ z : ℂ, 0 < z.re → f z = 0 by
    simpa only [closure_setOf_lt_re] using
      EqOn.of_subset_closure this hd.continuousOn continuousOn_const subset_closure Subset.rfl
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
n : ℕ
z : ℂ
⊢ ‖g n z‖ = expR z.re ^ n * ‖f z‖

Tactic:
simp only [g, norm_smul, norm_pow, norm_exp]

Premises used: norm_smul, norm_pow, Complex.norm_exp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
⊢ ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖

Tactic:
have hg : ∀ n z, ‖g n z‖ = expR z.re ^ n * ‖f z‖ := fun n z ↦ by
    simp only [g, norm_smul, norm_pow, norm_exp]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : ∀ (n : ℕ), ‖g n z‖ ≤ C
contrapose! : ∀ (H : f z ≠ 0), ∃ (n : ℕ), C < ‖g n z‖
⊢ f z = 0

Tactic:
contrapose! H
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : f z ≠ 0
simp : ∃ (n : ℕ), C < expR z.re ^ n * ‖f z‖
⊢ ∃ (n : ℕ), C < ‖g n z‖

Tactic:
simp only [hg]
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : f z ≠ 0
⊢ ∃ (n : ℕ), C < expR z.re ^ n * ‖f z‖

Tactic:
(((tendsto_pow_atTop_atTop_of_one_lt (Real.one_lt_exp_iff.2 hz)).atTop_mul_const
      (norm_pos_iff.2 H)).eventually (eventually_gt_atTop C)).exists

Premises used: Iff.mpr, norm_pos_iff, Filter.Tendsto.atTop_mul_const, Filter.Eventually.exists, tendsto_pow_atTop_atTop_of_one_lt, Real.one_lt_exp_iff, Filter.Tendsto.eventually, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : f z ≠ 0
⊢ ∃ (n : ℕ), C < expR z.re ^ n * ‖f z‖

Tactic:
exact (((tendsto_pow_atTop_atTop_of_one_lt (Real.one_lt_exp_iff.2 hz)).atTop_mul_const
      (norm_pos_iff.2 H)).eventually (eventually_gt_atTop C)).exists

Premises used: Iff.mpr, norm_pos_iff, Filter.Tendsto.atTop_mul_const, Filter.Eventually.exists, tendsto_pow_atTop_atTop_of_one_lt, Real.one_lt_exp_iff, Filter.Tendsto.eventually, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
C : ℝ
hC : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
suffices : ∀ (n : ℕ), ‖g n z‖ ≤ C
⊢ f z = 0

Tactic:
suffices H : ∀ n : ℕ, ‖g n z‖ ≤ C by
    contrapose! H
    simp only [hg]
    exact (((tendsto_pow_atTop_atTop_of_one_lt (Real.one_lt_exp_iff.2 hz)).atTop_mul_const
      (norm_pos_iff.2 H)).eventually (eventually_gt_atTop C)).exists