-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_iff' {g : α → E'''} :
    f =O[l] g ↔ ∃ c > 0, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
case intro
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
refine ⟨max c 1, zero_lt_one.trans_le (le_max_right _ _), ?_⟩

Result:
case intro
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (c ⊔ 1) * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨c, ⟨_, hc⟩⟩ := h

Result:
case intro.intro
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
left✝ : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
case mp
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

case mpr
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
case mp =>
  rw [isBigO_iff] at h
  obtain ⟨c, hc⟩ := h
  refine ⟨max c 1, zero_lt_one.trans_le (le_max_right _ _), ?_⟩
  filter_upwards [hc] with x hx
  apply hx.trans
  gcongr
  exact le_max_left _ _

Result:
case mpr
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Proof state:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
refine ⟨fun h => ?mp, fun h => ?mpr⟩

Result:
case mp
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

case mpr
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Proof state:
case h
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x‖ ≤ (c ⊔ 1) * ‖g x‖

Tactic:
apply hx.trans

Result:
case h
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c * ‖g x‖ ≤ (c ⊔ 1) * ‖g x‖

Proof state:
case h
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c * ‖g x‖ ≤ (c ⊔ 1) * ‖g x‖

Tactic:
gcongr

Result:
case h.h
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c ≤ c ⊔ 1

Proof state:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨c, hc⟩ := h

Result:
case intro
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
case intro.intro
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
left✝ : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
exact ⟨c, hc⟩

Result:
no goals

Proof state:
case h.h
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c ≤ c ⊔ 1

Tactic:
exact le_max_left _ _

Result:
no goals

Proof state:
case mpr
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
case mpr =>
  rw [isBigO_iff]
  obtain ⟨c, ⟨_, hc⟩⟩ := h
  exact ⟨c, hc⟩

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [isBigO_iff] at h

Result:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
rw [isBigO_iff]

Result:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
case intro
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (c ⊔ 1) * ‖g x‖

Tactic:
filter_upwards [hc] with x hx

Result:
case h
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x‖ ≤ (c ⊔ 1) * ‖g x‖