awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨c, hc⟩ := h
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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:
⟨max c 1, zero_lt_one.trans_le (le_max_right _ _), ?_⟩

Premises used: le_max_right, zero_lt_one, Max.max, LT.lt.trans_le, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
refine : ∀ᶠ (x : α) in l, ‖f x‖ ≤ max c 1 * ‖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 _ _), ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
h : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖), ‖f x‖ ≤ max c 1 * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ max c 1 * ‖g x‖

Tactic:
filter_upwards [hc] with x hx
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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‖
h : c * ‖g x‖ ≤ max c 1 * ‖g x‖
⊢ ‖f x‖ ≤ max c 1 * ‖g x‖

Tactic:
apply hx.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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‖
h : c ≤ max c 1
⊢ c * ‖g x‖ ≤ max c 1 * ‖g x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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 ≤ max c 1

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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 ≤ max c 1

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

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

Premises used: Asymptotics.isBigO_iff, le_max_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
rw : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
rw [isBigO_iff]

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
obtain : ∀ c > 0, ∀ (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨c, ⟨_, hc⟩⟩ := h
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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:
⟨c, hc⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case case₁ case₂ : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case₃ : ∀ c > 0, ∀ (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ (c : ℝ), ∀ᶠ (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⟩

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

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

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
refine : ∀ (h : f =O[l] g), ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
refine₁ : ∀ (h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), f =O[l] g
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
refine ⟨fun h => ?mp, fun h => ?mpr⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : 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

Premises used: Asymptotics.isBigO_iff'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
obtain :
  ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ c⁻¹ > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
refine : ∀ᶠ (x : α) in l, c⁻¹ * ‖f x‖ ≤ ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
h : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖), c⁻¹ * ‖f x‖ ≤ ‖g x‖
⊢ ∀ᶠ (x : α) in l, c⁻¹ * ‖f x‖ ≤ ‖g x‖

Tactic:
filter_upwards [hc] with x hx
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ 0 < c

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
h h₁ h₂ h₃ : ‖f x‖ ≤ c * ‖g x‖
⊢ c⁻¹ * ‖f x‖ ≤ ‖g x‖

Tactic:
rwa [inv_mul_le_iff₀ (by positivity)]

Premises used: inv_mul_le_iff₀
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
case mp =>
    rw [isBigO_iff'] at h
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [inv_mul_le_iff₀ (by positivity)]

Premises used: inv_mul_le_iff₀, Asymptotics.isBigO_iff'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
rw : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
rw [isBigO_iff']

Premises used: Asymptotics.isBigO_iff'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
obtain :
  ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ c⁻¹ > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
refine : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c⁻¹ * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
h : ∀ (x : α) (hx : c * ‖f x‖ ≤ ‖g x‖), ‖f x‖ ≤ c⁻¹ * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c⁻¹ * ‖g x‖

Tactic:
filter_upwards [hc] with x hx
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c⁻¹⁻¹ * ‖f x‖ ≤ ‖g x‖
⊢ 0 < c⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c * ‖f x‖ ≤ ‖g x‖
h : ∀ (hx : c⁻¹⁻¹ * ‖f x‖ ≤ ‖g x‖), ‖f x‖ ≤ c⁻¹ * ‖g x‖
h₁ h₂ h₃ h₄ : ∀ (hx : ‖f x‖ ≤ c⁻¹ * ‖g x‖), ‖f x‖ ≤ c⁻¹ * ‖g x‖
⊢ ‖f x‖ ≤ c⁻¹ * ‖g x‖

Tactic:
rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx

Premises used: inv_mul_le_iff₀, inv_inv
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
case case₁ case₂ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case₃ :
  ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case₄ : ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c⁻¹ * ‖g x‖
h₁ :
  ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖) (x : α) (hx : c * ‖f x‖ ≤ ‖g x‖),
    ‖f x‖ ≤ c⁻¹ * ‖g x‖
⊢ f =O[l] g

Tactic:
case mpr =>
    rw [isBigO_iff']
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx

Premises used: inv_mul_le_iff₀, Asymptotics.isBigO_iff'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
c : ℝ
h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g

Tactic:
isBigO_iff.2 ⟨c, h⟩

Premises used: Iff.mpr, Asymptotics.isBigO_iff, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
simpa only [one_mul] using h

Premises used: one_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g → ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
isBigO_iff.1

Premises used: Asymptotics.isBigO_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
g : α → ℝ
h : (fun (x : α) ↦ ‖f x‖) ≤ᶠ[l] g
⊢ f =O[l] g

Tactic:
.of_bound' <| h.mono fun _ h ↦ h.trans <| le_abs_self _

Premises used: le_abs_self, Filter.Eventually.mono, Asymptotics.IsBigO.of_bound', LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
g : α → ℝ
h : ∀ (x : α), ‖f x‖ ≤ g x
⊢ f =O[l] g

Tactic:
.of_norm_eventuallyLE <| .of_forall h

Premises used: Asymptotics.IsBigO.of_norm_eventuallyLE, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₁ : f =O[l] g
h₂ : g =O[l] f
⊢ f =Θ[l] g

Tactic:
⟨h₁, h₂⟩

Premises used: Asymptotics.IsTheta, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =Θ[l] g
⊢ f =O[l] g

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =Θ[l] g
⊢ g =O[l] f

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
rw rw₁ : (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Tactic:
rw [IsLittleO_def]

Premises used: Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp only [IsLittleO_def, IsBigOWith_def]

Premises used: Asymptotics.IsBigOWith_def, Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
isLittleO_iff.1 h hc

Premises used: Iff.mp, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hc : 0 < c
⊢ IsBigOWith c l f g

Tactic:
isBigOWith_iff.2 <| isLittleO_iff.1 h hc

Premises used: Iff.mpr, Asymptotics.isBigOWith_iff, Iff.mp, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖

Tactic:
simpa using h.def zero_lt_one

Premises used: zero_lt_one, Asymptotics.IsLittleO.def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
⊢ LT.lt (α := ℝ) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
refine :
  ∀ (x : α), ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖ → ∀ (hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖) (hx₂ : 0 < ‖g x‖), 2⁻¹ * ‖g x‖ < ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ < ‖g x‖

Tactic:
refine ((h.def (show 0 < 2⁻¹ by simp)).and hg).mono fun x ⟨hx₁, hx₂⟩ ↦ hx₁.trans_lt ?_

Premises used: Filter.Eventually.and, Filter.Eventually.mono, Asymptotics.IsLittleO.def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
x : α
h_1 : ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖
hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖
hx₂ : 0 < ‖g x‖
rw : LT.lt (α := ℝ) 2⁻¹ 1
⊢ 2⁻¹ * ‖g x‖ < ‖g x‖

Tactic:
rw [mul_lt_iff_lt_one_left hx₂]

Premises used: mul_lt_iff_lt_one_left
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
x : α
h_1 : ‖f x‖ ≤ 2⁻¹ * ‖g x‖ ∧ 0 < ‖g x‖
hx₁ : ‖f x‖ ≤ 2⁻¹ * ‖g x‖
hx₂ : 0 < ‖g x‖
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
rw : ∃ (c : ℝ), IsBigOWith c l f g
⊢ f =O[l] g

Tactic:
rw [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ ∃ (c : ℝ), IsBigOWith c l f g

Tactic:
⟨c, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ ∃ (c : ℝ), IsBigOWith c l f g

Tactic:
exact ⟨c, h⟩
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hgf : f =o[l] g
⊢ IsBigOWith 1 l f g

Tactic:
hgf.def' zero_lt_one

Premises used: zero_lt_one, Asymptotics.IsLittleO.def'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hgf : f =o[l] g
⊢ f =O[l] g

Tactic:
hgf.isBigOWith.isBigO

Premises used: Asymptotics.IsLittleO.isBigOWith, Asymptotics.IsBigOWith.isBigO
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g → ∃ (c : ℝ), IsBigOWith c l f g

Tactic:
isBigO_iff_isBigOWith.1

Premises used: Iff.mp, Asymptotics.isBigO_iff_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
c c' : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
hc : c ≤ c'
x : α
hx : Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖f x‖ ≤ c * ‖g' x‖) x} x
ha : 0 ≤ ‖g' x‖
⊢ c * ‖g' x‖ ≤ c' * ‖g' x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
⊢ ∃ c' > 0, IsBigOWith c' l f g'

Tactic:
⟨max c 1, lt_of_lt_of_le zero_lt_one (le_max_right c 1), h.weaken <| le_max_left c 1⟩

Premises used: le_max_right, zero_lt_one, Max.max, And.intro, Exists.intro, OfNat.ofNat, Asymptotics.IsBigOWith.weaken, le_max_left, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
h : f =O[l] g'
⊢ ∃ c > 0, IsBigOWith c l f g'

Tactic:
let ⟨_c, hc⟩ := h.isBigOWith
  hc.exists_pos

Premises used: Asymptotics.IsBigOWith, _private.0.Asymptotics.IsBigO.exists_pos.match_1, Exists, GT.gt, And, Asymptotics.IsBigOWith.exists_pos, Asymptotics.IsBigO.isBigOWith, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
⊢ ∃ c' ≥ 0, IsBigOWith c' l f g'

Tactic:
let ⟨c, cpos, hc⟩ := h.exists_pos
  ⟨c, le_of_lt cpos, hc⟩

Premises used: _private.0.Asymptotics.IsBigOWith.exists_nonneg.match_1, Asymptotics.IsBigOWith, le_of_lt, Exists, GE.ge, And, And.intro, Asymptotics.IsBigOWith.exists_pos, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
h : f =O[l] g'
⊢ ∃ c ≥ 0, IsBigOWith c l f g'

Tactic:
let ⟨_c, hc⟩ := h.isBigOWith
  hc.exists_nonneg

Premises used: Asymptotics.IsBigOWith, _private.0.Asymptotics.IsBigO.exists_pos.match_1, Exists, GE.ge, And, Asymptotics.IsBigOWith.exists_nonneg, Asymptotics.IsBigO.isBigOWith, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ f =O[l] g' ↔ ∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g'

Tactic:
isBigO_iff_isBigOWith.trans
    ⟨fun ⟨c, hc⟩ => mem_atTop_sets.2 ⟨c, fun _c' hc' => hc.weaken hc'⟩, fun h => h.exists⟩

Premises used: Iff.mpr, Asymptotics.IsBigOWith, _private.0.Asymptotics.IsBigO.exists_pos.match_1, Filter.mem_atTop_sets, Filter.Eventually, Filter.Eventually.exists, Filter.atTop, Iff.intro, Exists.intro, Iff.trans, Asymptotics.isBigO_iff_isBigOWith, Asymptotics.IsBigOWith.weaken
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (c : ℝ) in atTop, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
simp only [IsBigOWith_def]

Premises used: Asymptotics.IsBigOWith_def
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
ι : Sort u_18
p : ι → Prop
s : ι → Set α
h_1 : f =O[l] g'
hb : l.HasBasis p s
c : ℝ
h : c > 0 ∧ IsBigOWith c l f g'
⊢ c > 0 ∧ ∃ (i : ι), p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖

Tactic:
simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h

Premises used: Asymptotics.isBigOWith_iff, exists_prop, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
hc : 0 < c
⊢ IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
simp only [IsBigOWith_def, ← div_eq_inv_mul, le_div_iff₀' hc]

Premises used: le_div_iff₀', Asymptotics.IsBigOWith_def, div_eq_inv_mul
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
mp : f =o[l] g → ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
mpr : (∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖) → f =o[l] g
⊢ f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖

Tactic:
constructor