awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
⊢ Bf ≤ max 0 (max Bf Bg)

Tactic:
(le_max_left _ _).trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
⊢ cg ≤ max cf cg

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
⊢ Bg ≤ max 0 (max Bf Bg)

Tactic:
(le_max_right _ _).trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          IsBigO (E := ℝ) (F := ℝ) (cobounded ℂ ⊓ l) (fun (z : ℂ) ↦ expR (B₁ * ‖z‖ ^ c₁)) fun (z : ℂ) ↦
            expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) f fun (z : ℂ) ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : IsBigO (F := ℝ) (cobounded ℂ ⊓ l) g fun (z : ℂ) ↦ expR (Bg * ‖z‖ ^ cg)
⊢ cf ≤ max cf cg

Tactic:
exacts [le_max_left _ _, le_max_left _ _, (le_max_left _ _).trans (le_max_right _ _),
    le_max_right _ _, le_max_left _ _, (le_max_right _ _).trans (le_max_right _ _)]

Premises used: le_max_right, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a ≤ z.im
hzb : z.im ≤ b
⊢ a = z.im ∨ a < z.im

Tactic:
rw [le_iff_eq_or_lt] at hza hzb

Premises used: le_iff_eq_or_lt
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a ≤ z.im
hzb : z.im ≤ b
hza₁ : a = z.im ∨ a < z.im
⊢ z.im = b ∨ z.im < b

Tactic:
rw [le_iff_eq_or_lt] at hza hzb

Premises used: le_iff_eq_or_lt
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a = z.im ∨ a < z.im
hzb : z.im = b ∨ z.im < b
inl : ∀ (hza : a = z.im), ‖f z‖ ≤ C
inr : ∀ (hza : a < z.im), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
rcases hza with hza | hza
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a = z.im
⊢ ‖f z‖ ≤ C

Tactic:
hle_a _ hza.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a = z.im
⊢ ‖f z‖ ≤ C

Tactic:
exact hle_a _ hza.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hzb : z.im = b ∨ z.im < b
hza : a < z.im
inr : ∀ (hzb : z.im = b), ‖f z‖ ≤ C
inr₁ : ∀ (hzb : z.im < b), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
rcases hzb with hzb | hzb
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im = b
⊢ ‖f z‖ ≤ C

Tactic:
hle_b _ hzb
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im = b
⊢ ‖f z‖ ≤ C

Tactic:
exact hle_b _ hzb
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
inr :
  ∀
    (this :
      ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C),
        ‖f z‖ ≤ C)
    (hC₀ : ¬0 < C), ‖f z‖ ≤ C
wlog :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
wlog hC₀ : 0 < C generalizing C
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
⊢ ‖f z‖ ≤ C

Tactic:
le_of_forall_gt_imp_ge_of_dense fun C' hC' => this (fun w hw => ?_) (fun w hw => ?_) ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
inr : ∀ (C' : ℝ) (hC' : C < C') (w : ℂ) (hw : w.im = a), ‖f w‖ ≤ C'
inr₁ : ∀ (C' : ℝ) (hC' : C < C') (w : ℂ) (hw : w.im = b), ‖f w‖ ≤ C'
inr₂ : ∀ (C' : ℝ) (hC' : C < C'), 0 < C'
⊢ ‖f z‖ ≤ C

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun C' hC' => this (fun w hw => ?_) (fun w hw => ?_) ?_

Premises used: le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
w : ℂ
hw : w.im = a
⊢ ‖f w‖ ≤ C'

Tactic:
(hle_a _ hw).trans hC'.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
w : ℂ
hw : w.im = a
⊢ ‖f w‖ ≤ C'

Tactic:
exact (hle_a _ hw).trans hC'.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
w : ℂ
hw : w.im = b
⊢ ‖f w‖ ≤ C'

Tactic:
(hle_b _ hw).trans hC'.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
w : ℂ
hw : w.im = b
⊢ ‖f w‖ ≤ C'

Tactic:
exact (hle_b _ hw).trans hC'.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
⊢ 0 < C'

Tactic:
((norm_nonneg (f (a * I))).trans (hle_a _ ?_)).trans_lt hC'

Premises used: HMul.hMul, Complex.ofReal, LE.le.trans, LE.le.trans_lt, norm_nonneg, Complex.I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
inr : ((↑a : ℂ) * I).im = a
⊢ 0 < C'

Tactic:
refine ((norm_nonneg (f (a * I))).trans (hle_a _ ?_)).trans_lt hC'

Premises used: HMul.hMul, Complex.ofReal, LE.le.trans, LE.le.trans_lt, norm_nonneg, Complex.I
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hza : a < z.im
hzb : z.im < b
this :
  ∀ {C : ℝ} (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C) (hC₀ : 0 < C), ‖f z‖ ≤ C
hC₀ : ¬0 < C
C' : ℝ
hC' : C < C'
inr : (↑a : ℂ).re = a
inr₁ inr₂ : a = a
⊢ ((↑a : ℂ) * I).im = a

Tactic:
rw [mul_I_im, ofReal_re]

Premises used: Complex.ofReal_re, Complex.mul_I_im
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C_1 : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hza : a < z.im
hzb : z.im < b
C : ℝ
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hC₀ : 0 < C
⊢ a = (a + b) / 2 - (b - a) / 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C_1 : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hza : a < z.im
hzb : z.im < b
C : ℝ
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hC₀ : 0 < C
⊢ b = (a + b) / 2 + (b - a) / 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b C_1 : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)
hB :
  ∃ c < π / (b - a),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)) f fun (z : ℂ) ↦ expR (B * expR (c * |z.re|))
hza : a < z.im
hzb : z.im < b
C : ℝ
hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C
hC₀ : 0 < C
obtain :
  ∀ (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)))
    (hB :
      ∃ c < π / (a + b - (a - b)),
        ∃ (B : ℝ),
          IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
            expR (B * expR (c * |z.re|))),
    ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
obtain ⟨a, b, rfl, rfl⟩ : ∃ a' b', a = a' - b' ∧ b = a' + b' :=
    ⟨(a + b) / 2, (b - a) / 2, by ring, by ring⟩

Premises used: rfl
-- 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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
⊢ a - b < a + b

Tactic:
have hab : a - b < a + b := hza.trans hzb
-- 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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
⊢ 0 < b

Tactic:
simpa only [sub_eq_add_neg, add_lt_add_iff_left, neg_lt_self_iff] using hab

Premises used: sub_eq_add_neg, neg_lt_self_iff, add_lt_add_iff_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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
⊢ 0 < b

Tactic:
have hb : 0 < b := by simpa only [sub_eq_add_neg, add_lt_add_iff_left, neg_lt_self_iff] using hab
-- 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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
⊢ ∃ c < π / 2 / b,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))

Tactic:
rw [add_sub_sub_cancel, ← two_mul, div_mul_eq_div_div] at hB

Premises used: add_sub_sub_cancel, two_mul, div_mul_eq_div_div
-- 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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
hB₁ :
  ∃ c < π / 2 / b,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
⊢ a - b < a + b

Tactic:
rw [add_sub_sub_cancel, ← two_mul, div_mul_eq_div_div] at hB

Premises used: add_sub_sub_cancel, two_mul, div_mul_eq_div_div
-- 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))
hB :
  ∃ c < π / (a + b - (a - b)),
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
hB₁ :
  ∃ c < π / 2 / b,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab₁ : a - b < a + b
⊢ 0 < b

Tactic:
rw [add_sub_sub_cancel, ← two_mul, div_mul_eq_div_div] at hB

Premises used: add_sub_sub_cancel, two_mul, div_mul_eq_div_div
-- 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))
hB :
  ∃ c < π / 2 / b,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
⊢ 0 < π / 2 / b

Tactic:
have hπb : 0 < π / 2 / b := div_pos Real.pi_div_two_pos hb
-- 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))
hB :
  ∃ c < π / 2 / b,
    ∃ (B : ℝ),
      IsBigO (F := ℝ) (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun (z : ℂ) ↦
        expR (B * expR (c * |z.re|))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
rcases :
  ∀ (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|))),
    ‖f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
rcases hB with ⟨c, hc, B, hO⟩
-- 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 : ℝ), (c < d ∧ 0 < d) ∧ d < π / 2 / b

Tactic:
simpa only [max_lt_iff] using exists_between (max_lt hc hπb)

Premises used: max_lt_iff, exists_between, max_lt