E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
⊢ ∃ c, c < a ∧ ∃ B, (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
⊢ ∃ c, c < a ∧ ∃ B, (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
have : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ →
    (fun z : ℂ => expR (B₁ * abs z ^ c₁)) =O[comap Complex.abs atTop ⊓ l]
      fun z => expR (B₂ * abs z ^ c₂) := fun hc hB₀ hB ↦ .of_bound 1 <| by
  have : ∀ᶠ z : ℂ in comap Complex.abs atTop ⊓ l, 1 ≤ abs z :=
    ((eventually_ge_atTop 1).comap _).filter_mono inf_le_left
  refine this.mono fun z hz => ?_
  rw [one_mul, Real.norm_eq_abs, Real.norm_eq_abs, Real.abs_exp, Real.abs_exp, Real.exp_le_exp]
  exact mul_le_mul hB (Real.rpow_le_rpow_of_exponent_le hz hc)
    (Real.rpow_nonneg_of_nonneg (Complex.abs.nonneg _) _) hB₀
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
⊢ ∃ c, c < a ∧ ∃ B, (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
⊢ ∃ c, c < a ∧ ∃ B, (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
rcases hBf with ⟨cf, hcf, Bf, hOf⟩
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ ∃ c, c < a ∧ ∃ B, (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
⊢ ∃ c, c < a ∧ ∃ B, (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
rcases hBg with ⟨cg, hcg, Bg, hOg⟩
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (max 0 (max Bf Bg) * ↑Complex.abs z ^ max cf cg)
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ ∃ c, c < a ∧ ∃ B, (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
refine' ⟨max cf cg, max_lt hcf hcg, max 0 (max Bf Bg), _⟩
case intro.intro.intro.intro.intro.intro.refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ cf ≤ max cf cg

case intro.intro.intro.intro.intro.intro.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

case intro.intro.intro.intro.intro.intro.refine'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ Bf ≤ max 0 (max Bf Bg)

case intro.intro.intro.intro.intro.intro.refine'_4
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ cg ≤ max cf cg

case intro.intro.intro.intro.intro.intro.refine'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

case intro.intro.intro.intro.intro.intro.refine'_6
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ Bg ≤ max 0 (max Bf Bg)
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ (f - g) =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (max 0 (max Bf Bg) * ↑Complex.abs z ^ max cf cg)
refine' (hOf.trans <| this _ _ _).sub (hOg.trans <| this _ _ _)
no goals
case intro.intro.intro.intro.intro.intro.refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ cf ≤ max cf cg

case intro.intro.intro.intro.intro.intro.refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

case intro.intro.intro.intro.intro.intro.refine'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ Bf ≤ max 0 (max Bf Bg)

case intro.intro.intro.intro.intro.intro.refine'_4
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ cg ≤ max cf cg

case intro.intro.intro.intro.intro.intro.refine'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

case intro.intro.intro.intro.intro.intro.refine'_6
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ →
      0 ≤ B₂ →
        B₁ ≤ B₂ →
          (fun z => expR (B₁ * ↑Complex.abs z ^ c₁)) =O[comap (↑Complex.abs) atTop ⊓ l] fun z =>
            expR (B₂ * ↑Complex.abs z ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bf * ↑Complex.abs z ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (Bg * ↑Complex.abs z ^ cg)
⊢ Bg ≤ max 0 (max Bf Bg)
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 _ _)]
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
this : ∀ᶠ (z : ℂ) in comap (↑Complex.abs) atTop ⊓ l, 1 ≤ ↑Complex.abs z
⊢ ∀ᶠ (x : ℂ) in comap (↑Complex.abs) atTop ⊓ l,
    ‖expR (B₁✝ * ↑Complex.abs x ^ c₁✝)‖ ≤ 1 * ‖expR (B₂✝ * ↑Complex.abs x ^ c₂✝)‖
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
⊢ ∀ᶠ (x : ℂ) in comap (↑Complex.abs) atTop ⊓ l,
    ‖expR (B₁✝ * ↑Complex.abs x ^ c₁✝)‖ ≤ 1 * ‖expR (B₂✝ * ↑Complex.abs x ^ c₂✝)‖
have : ∀ᶠ z : ℂ in comap Complex.abs atTop ⊓ l, 1 ≤ abs z :=
  ((eventually_ge_atTop 1).comap _).filter_mono inf_le_left
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
this : ∀ᶠ (z : ℂ) in comap (↑Complex.abs) atTop ⊓ l, 1 ≤ ↑Complex.abs z
z : ℂ
hz : 1 ≤ ↑Complex.abs z
⊢ ‖expR (B₁✝ * ↑Complex.abs z ^ c₁✝)‖ ≤ 1 * ‖expR (B₂✝ * ↑Complex.abs z ^ c₂✝)‖
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
this : ∀ᶠ (z : ℂ) in comap (↑Complex.abs) atTop ⊓ l, 1 ≤ ↑Complex.abs z
⊢ ∀ᶠ (x : ℂ) in comap (↑Complex.abs) atTop ⊓ l,
    ‖expR (B₁✝ * ↑Complex.abs x ^ c₁✝)‖ ≤ 1 * ‖expR (B₂✝ * ↑Complex.abs x ^ c₂✝)‖
refine this.mono fun z hz => ?_
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
this : ∀ᶠ (z : ℂ) in comap (↑Complex.abs) atTop ⊓ l, 1 ≤ ↑Complex.abs z
z : ℂ
hz : 1 ≤ ↑Complex.abs z
⊢ B₁✝ * ↑Complex.abs z ^ c₁✝ ≤ B₂✝ * ↑Complex.abs z ^ c₂✝
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
this : ∀ᶠ (z : ℂ) in comap (↑Complex.abs) atTop ⊓ l, 1 ≤ ↑Complex.abs z
z : ℂ
hz : 1 ≤ ↑Complex.abs z
⊢ ‖expR (B₁✝ * ↑Complex.abs z ^ c₁✝)‖ ≤ 1 * ‖expR (B₂✝ * ↑Complex.abs z ^ c₂✝)‖
rw [one_mul, Real.norm_eq_abs, Real.norm_eq_abs, Real.abs_exp, Real.abs_exp, Real.exp_le_exp]
no goals
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
hBf : ∃ c, c < a ∧ ∃ B, f =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
hBg : ∃ c, c < a ∧ ∃ B, g =O[comap (↑Complex.abs) atTop ⊓ l] fun z => expR (B * ↑Complex.abs z ^ c)
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
this : ∀ᶠ (z : ℂ) in comap (↑Complex.abs) atTop ⊓ l, 1 ≤ ↑Complex.abs z
z : ℂ
hz : 1 ≤ ↑Complex.abs z
⊢ B₁✝ * ↑Complex.abs z ^ c₁✝ ≤ B₂✝ * ↑Complex.abs z ^ c₂✝
exact mul_le_mul hB (Real.rpow_le_rpow_of_exponent_le hz hc)
  (Real.rpow_nonneg_of_nonneg (Complex.abs.nonneg _) _) hB₀