-- Mathlib/Analysis/Complex/PhragmenLindelof.lean
theorem isBigO_sub_exp_exp {a : ℝ} {f g : ℂ → E} {l : Filter ℂ} {u : ℂ → ℝ}
    (hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|)))
    (hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))) :
    ∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))
⊢ cf ≤ cf ⊔ cg

case intro.intro.intro.intro.intro.intro.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))
⊢ 0 ≤ 0 ⊔ (Bf ⊔ Bg)

case intro.intro.intro.intro.intro.intro.refine_3
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))
⊢ Bf ≤ 0 ⊔ (Bf ⊔ Bg)

case intro.intro.intro.intro.intro.intro.refine_4
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))
⊢ cg ≤ cf ⊔ cg

case intro.intro.intro.intro.intro.intro.refine_5
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))
⊢ 0 ≤ 0 ⊔ (Bf ⊔ Bg)

case intro.intro.intro.intro.intro.intro.refine_6
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))
⊢ Bg ≤ 0 ⊔ (Bf ⊔ Bg)

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 _ _)]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))

Tactic:
have : ∀ {c₁ c₂ B₁ B₂}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ z,
    ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖ := fun hc hB₀ hB z ↦ by
  simp only [Real.norm_eq_abs, Real.abs_exp]; gcongr

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
⊢ expR (B₁✝ * expR (c₁✝ * |u z|)) ≤ expR (B₂✝ * expR (c₂✝ * |u z|))

Tactic:
gcongr

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
⊢ ‖expR (B₁✝ * expR (c₁✝ * |u z|))‖ ≤ ‖expR (B₂✝ * expR (c₂✝ * |u z|))‖

Tactic:
simp only [Real.norm_eq_abs, Real.abs_exp]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
c₁✝ c₂✝ B₁✝ B₂✝ : ℝ
hc : c₁✝ ≤ c₂✝
hB₀ : 0 ≤ B₂✝
hB : B₁✝ ≤ B₂✝
z : ℂ
⊢ expR (B₁✝ * expR (c₁✝ * |u z|)) ≤ expR (B₂✝ * expR (c₂✝ * |u z|))

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))

Tactic:
rcases hBf with ⟨cf, hcf, Bf, hOf⟩

Result:
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))

Proof state:
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))

Tactic:
rcases hBg with ⟨cg, hcg, Bg, hOg⟩

Result:
case intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))
⊢ ∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))