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
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f (↑x₀ : ℂ) ≠ 0
hlt : norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖
neg : ∀ᶠ (x : ℝ) in atTop ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
⊢ ∀ᶠ (x : ℝ) in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖

Tactic:
rw [cocompact_eq_atBot_atTop, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot,
      bot_sup_eq]

Premises used: bot_sup_eq, inf_sup_right, cocompact_eq_atBot_atTop, OfNat.ofNat, Filter.disjoint_atBot_principal_Ici, Disjoint.eq_bot
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f (↑x₀ : ℂ) ≠ 0
hlt : norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖
⊢ ∀ᶠ (x : ℝ) in atTop ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖

Tactic:
(hre.norm.eventually <| ge_mem_nhds hlt).filter_mono inf_le_left

Premises used: Filter.Eventually.filter_mono, Set.Mem, setOf, Filter.Tendsto.norm, ge_mem_nhds, Filter.Tendsto.eventually, inf_le_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
hfc : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) (Ici 0)
x₀ : ℝ
hx₀ : 0 ≤ x₀
hne : f (↑x₀ : ℂ) ≠ 0
hlt : norm.{u_1} (E := E) 0 < ‖f (↑x₀ : ℂ)‖
⊢ ∀ᶠ (x : ℝ) in atTop ⊓ 𝓟 (Ici 0), ‖f (↑x : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖

Tactic:
exact (hre.norm.eventually <| ge_mem_nhds hlt).filter_mono inf_le_left

Premises used: Filter.Eventually.filter_mono, Filter.Tendsto.norm, ge_mem_nhds, Filter.Tendsto.eventually, inf_le_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
obtain :
  ∀ (x₀ : ℝ) (hx₀ : 0 ≤ x₀) (hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖) {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C

Tactic:
obtain ⟨x₀, hx₀, hmax⟩ : ∃ x : ℝ, 0 ≤ x ∧ ∀ y : ℝ, 0 ≤ y → ‖f y‖ ≤ ‖f x‖ := by
    have hfc : ContinuousOn (fun x : ℝ => f x) (Ici 0) := by
      refine hd.continuousOn.comp continuous_ofReal.continuousOn fun x hx => ?_
      rwa [closure_setOf_lt_re]
    by_cases! h₀ : ∀ x : ℝ, 0 ≤ x → f x = 0
    · refine ⟨0, le_rfl, fun y hy => ?_⟩; rw [h₀ y hy, h₀ 0 le_rfl]
    rcases h₀ with ⟨x₀, hx₀, hne⟩
    have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_iff]
    suffices ∀ᶠ x : ℝ in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f x‖ ≤ ‖f x₀‖ by
      simpa only [exists_prop] using hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this
    rw [cocompact_eq_atBot_atTop, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot,
      bot_sup_eq]
    exact (hre.norm.eventually <| ge_mem_nhds hlt).filter_mono inf_le_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
inl : ∀ (h : ‖f (↑x₀ : ℂ)‖ ≤ C) {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
inr : ∀ (h : C < ‖f (↑x₀ : ℂ)‖) {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C

Tactic:
rcases le_or_gt ‖f x₀‖ C with h | h

Premises used: Norm.norm, Complex.ofReal, le_or_gt
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
h : ‖f (↑x₀ : ℂ)‖ ≤ C
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C

Tactic:
simpa only [max_eq_left h] using hle _ hmax

Premises used: max_eq_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
h : C < ‖f (↑x₀ : ℂ)‖
z : ℂ
hz : 0 < z.re
⊢ Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ (norm ∘ f) x ≤ (norm ∘ f) (↑x₀ : ℂ)) x} z

Tactic:
simpa [max_eq_right h.le] using hle _ hmax _ hz.le

Premises used: LT.lt.le, max_eq_right
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
hmax : ∀ (y : ℝ), 0 ≤ y → ‖f (↑y : ℂ)‖ ≤ ‖f (↑x₀ : ℂ)‖
h : C < ‖f (↑x₀ : ℂ)‖
⊢ IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)

Tactic:
replace hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} x₀ := by
      rintro z (hz : 0 < z.re)
      simpa [max_eq_right h.le] using hle _ hmax _ hz.le
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
apply : ball (↑x₀ : ℂ) (dist 0 (↑x₀ : ℂ)) ⊆ {z : ℂ | 0 < z.re}
⊢ ‖f 0‖ = ‖f (↑x₀ : ℂ)‖

Tactic:
apply norm_eq_norm_of_isMaxOn_of_ball_subset hd hmax

Premises used: Complex.norm_eq_norm_of_isMaxOn_of_ball_subset
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z ∈ ball (↑x₀ : ℂ) (dist 0 (↑x₀ : ℂ))
⊢ ‖z - (↑x₀ : ℂ)‖ < x₀

Tactic:
rw [mem_ball, dist_zero_left, dist_eq, Complex.norm_of_nonneg hx₀] at hz

Premises used: Complex.norm_of_nonneg, Metric.mem_ball, Complex.dist_eq, dist_zero_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : ‖z - (↑x₀ : ℂ)‖ < x₀
contrapose! : ∀ (hz : z.re ≤ 0), x₀ ≤ ‖z - (↑x₀ : ℂ)‖
⊢ 0 < z.re

Tactic:
contrapose! hz
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
⊢ x₀ ≤ x₀ - z.re

Tactic:
(le_sub_self_iff _).2 hz

Premises used: Iff.mpr, le_sub_self_iff
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
⊢ x₀ - z.re ≤ |x₀ - z.re|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
rw : |x₀ - z.re| = |z.re - (↑x₀ : ℂ).re|
rw₁ : |x₀ - z.re| = |z.re - x₀|
rw₂ rw₃ : |z.re - x₀| = |z.re - x₀|
⊢ |x₀ - z.re| = |(z - (↑x₀ : ℂ)).re|

Tactic:
rw [sub_re, ofReal_re, _root_.abs_sub_comm]

Premises used: Complex.sub_re, Complex.ofReal_re, abs_sub_comm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
⊢ |(z - (↑x₀ : ℂ)).re| ≤ ‖z - (↑x₀ : ℂ)‖

Tactic:
abs_re_le_norm _

Premises used: Complex.abs_re_le_norm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
z : ℂ
hz : z.re ≤ 0
x₁ : |x₀ - z.re| = |(z - (↑x₀ : ℂ)).re|
⊢ x₀ ≤ ‖z - (↑x₀ : ℂ)‖

Tactic:
calc
        x₀ ≤ x₀ - z.re := (le_sub_self_iff _).2 hz
        _ ≤ |x₀ - z.re| := le_abs_self _
        _ = |(z - x₀).re| := by rw [sub_re, ofReal_re, _root_.abs_sub_comm]
        _ ≤ ‖z - x₀‖ := abs_re_le_norm _

Premises used: Iff.mpr, le_abs_self, HSub.hSub, Complex.ofReal, Complex.re, Complex.abs_re_le_norm, le_sub_self_iff
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
⊢ ‖f 0‖ = ‖f (↑x₀ : ℂ)‖

Tactic:
have : ‖f 0‖ = ‖f x₀‖ := by
      apply norm_eq_norm_of_isMaxOn_of_ball_subset hd hmax
      -- move to a lemma?
      intro z hz
      rw [mem_ball, dist_zero_left, dist_eq, Complex.norm_of_nonneg hx₀] at hz
      rw [mem_setOf_eq]
      contrapose! hz
      calc
        x₀ ≤ x₀ - z.re := (le_sub_self_iff _).2 hz
        _ ≤ |x₀ - z.re| := le_abs_self _
        _ = |(z - x₀).re| := by rw [sub_re, ofReal_re, _root_.abs_sub_comm]
        _ ≤ ‖z - x₀‖ := abs_re_le_norm _
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
this : ‖f 0‖ = ‖f (↑x₀ : ℂ)‖
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C

Tactic:
(h.not_ge <| this ▸ ?_).elim

Premises used: False.elim, Eq.rec, LT.lt.not_ge
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
this : ‖f 0‖ = ‖f (↑x₀ : ℂ)‖
inr : ‖f 0‖ ≤ C
⊢ ∀ {z : ℂ} (hz : 0 ≤ z.re), ‖f z‖ ≤ C

Tactic:
refine (h.not_ge <| this ▸ ?_).elim

Premises used: False.elim, Eq.rec, LT.lt.not_ge
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
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 : Tendsto.{0, u_1} (β := E) (fun (x : ℝ) ↦ f (↑x : ℂ)) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f (↑x : ℂ)‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f (↑x₀ : ℂ)‖
hmax : IsMaxOn (norm ∘ f) {z : ℂ | 0 < z.re} (↑x₀ : ℂ)
this : ‖f 0‖ = ‖f (↑x₀ : ℂ)‖
⊢ ‖f 0‖ ≤ C

Tactic:
simpa using him 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * 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 : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
refine : Tendsto (fun (c : ℝ) ↦ ‖cexp ((↑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 : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
⊢ Continuous (Y := ℝ) fun (c : ℝ) ↦ ‖cexp ((↑c : ℂ) * z) • f z‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
⊢ ‖cexp ((↑0 : ℂ) * z) • f z‖ = ‖f z‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
⊢ Tendsto (fun (c : ℝ) ↦ ‖cexp ((↑c : ℂ) * z) • f z‖) (𝓝 0) (𝓝 ‖f z‖)

Tactic:
exact Continuous.tendsto' (by fun_prop) _ _ (by simp)

Premises used: Continuous.tendsto'
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
suffices : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
suffices ∀ᶠ ε : ℝ in 𝓝[<] 0, ‖exp (ε * z) • f z‖ ≤ C by
    refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this
    exact Continuous.tendsto' (by fun_prop) _ _ (by simp)
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
h : ∀ (ε : ℝ) (ε₀ : Membership.mem (γ := Set ℝ) (Iio 0) ε), ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C
⊢ ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp ((↑ε : ℂ) * 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 : ℝ
f : ℂ → E
z : ℂ
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 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (x : ℝ) ↦ ‖f (↑x : ℂ)‖
him : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : 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 : ℝ
f : ℂ → E
z : ℂ
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 : 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
h : ‖g z‖ ≤ C
⊢ ‖cexp ((↑ε : ℂ) * z) • f z‖ ≤ C

Tactic:
change ‖g z‖ ≤ C
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
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 : 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
⊢ DiffContOnCl ℂ g {z : ℂ | 0 < z.re}

Tactic:
replace hd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re} :=
    (differentiable_id.const_mul _).cexp.diffContOnCl.smul hd