-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_iff_exists_eq_mul :
    u =O[l] v ↔ ∃ φ : α → 𝕜, l.IsBoundedUnder (· ≤ ·) (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Proof state:
case mp.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
rcases hc.exists_eq_mul hnnc with ⟨φ, hφ, huvφ⟩

Result:
case mp.intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
huvφ : u =ᶠ[l] φ * v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
φ : α → 𝕜
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
huvφ : u =ᶠ[l] φ * v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
exact ⟨φ, ⟨c, hφ⟩, huvφ⟩

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v ↔ ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
constructor

Result:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v → ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v) → u =O[l] v

Proof state:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
rcases h.exists_nonneg with ⟨c, hnnc, hc⟩

Result:
case mp.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
c : ℝ
hnnc : c ≥ 0
hc : IsBigOWith c l u v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Proof state:
case mpr.intro.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
huvφ : u =ᶠ[l] φ * v
c : ℝ
hφ : ∀ᶠ (x : ℝ) in map (norm ∘ φ) l, (fun x1 x2 => x1 ≤ x2) x c
⊢ u =O[l] v

Tactic:
exact isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v → ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
rintro h

Result:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
h : u =O[l] v
⊢ ∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Proof state:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v) → u =O[l] v

Tactic:
rintro ⟨φ, ⟨c, hφ⟩, huvφ⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v φ : α → 𝕜
huvφ : u =ᶠ[l] φ * v
c : ℝ
hφ : ∀ᶠ (x : ℝ) in map (norm ∘ φ) l, (fun x1 x2 => x1 ≤ x2) x c
⊢ u =O[l] v