awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
H : f =o[l] g
⊢ ∀ᶠ (x : α) in l, (↑0 : ℝ) * ‖f x‖ ≤ ‖g x‖

Tactic:
(H.def one_pos).mono fun x h₀' => ?_

Premises used: Filter.Eventually.mono, one_pos, 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₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
mp : ∀ (x : α) (h₀' : ‖f x‖ ≤ 1 * ‖g x‖), (↑0 : ℝ) * ‖f x‖ ≤ ‖g x‖
⊢ ∀ᶠ (x : α) in l, (↑0 : ℝ) * ‖f x‖ ≤ ‖g x‖

Tactic:
refine (H.def one_pos).mono fun x h₀' => ?_

Premises used: Filter.Eventually.mono, one_pos, 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₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
mp : 0 ≤ ‖g x‖
⊢ (↑0 : ℝ) * ‖f x‖ ≤ ‖g x‖

Tactic:
rw [Nat.cast_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Nat.cast_zero
-- 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‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
⊢ 0 ≤ ‖g x‖

Tactic:
h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x

Premises used: LE.le.trans, Or.elim
-- 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‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
mp : ∀ (hf : ∀ (x : α), 0 ≤ ‖f x‖), ‖f x‖ ≤ ‖g x‖
⊢ 0 ≤ ‖g x‖

Tactic:
refine h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x

Premises used: LE.le.trans, Or.elim
-- 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‖
H : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
mp mp₁ mp₂ mp₃ : ∀ (h₀' : ‖f x‖ ≤ ‖g x‖) (hf : ∀ (x : α), 0 ≤ ‖f x‖), ‖f x‖ ≤ ‖g x‖
⊢ ‖f x‖ ≤ ‖g x‖

Tactic:
rwa [one_mul] at 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 α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
n : ℕ
⊢ LT.lt (α := ℝ) 0 (↑n.succ : ℝ)

Tactic:
have : (0 : ℝ) < n.succ := Nat.cast_pos.2 n.succ_pos
-- 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‖
H : f =o[l] g
n : ℕ
this : LT.lt (α := ℝ) 0 (↑n.succ : ℝ)
⊢ ∀ᶠ (x : α) in l, (↑(n + 1) : ℝ) * ‖f x‖ ≤ ‖g x‖

Tactic:
(isBigOWith_inv this).1 (H.def' <| inv_pos.2 this)

Premises used: Iff.mpr, inv_pos, Iff.mp, Asymptotics.IsLittleO.def', Asymptotics.isBigOWith_inv
-- 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‖
H : f =o[l] g
n : ℕ
this : LT.lt (α := ℝ) 0 (↑n.succ : ℝ)
⊢ ∀ᶠ (x : α) in l, (↑(n + 1) : ℝ) * ‖f x‖ ≤ ‖g x‖

Tactic:
exact (isBigOWith_inv this).1 (H.def' <| inv_pos.2 this)

Premises used: Iff.mpr, inv_pos, Iff.mp, Asymptotics.IsLittleO.def', Asymptotics.isBigOWith_inv
-- 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‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖) → f =o[l] g

Tactic:
fun H => isLittleO_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, 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₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
mpr :
  ∀ (H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖) (ε : ℝ) (ε0 : 0 < ε), ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖) → f =o[l] g

Tactic:
refine fun H => isLittleO_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, 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₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
mpr : ∀ (n : ℕ) (hn : ε⁻¹ < (↑n : ℝ)), ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖

Tactic:
rcases exists_nat_gt ε⁻¹ with ⟨n, hn⟩

Premises used: Inv.inv, exists_nat_gt
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hn₀ : (0 : ℝ) < n := (inv_pos.2 ε0).trans hn
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖

Tactic:
((isBigOWith_inv hn₀).2 (H n)).bound.mono fun x hfg => ?_

Premises used: Iff.mpr, Filter.Eventually.mono, Asymptotics.IsBigOWith.bound, Asymptotics.isBigOWith_inv
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
mpr : ∀ (x : α) (hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖), ‖f x‖ ≤ ε * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖

Tactic:
refine ((isBigOWith_inv hn₀).2 (H n)).bound.mono fun x hfg => ?_

Premises used: Iff.mpr, Filter.Eventually.mono, Asymptotics.IsBigOWith.bound, Asymptotics.isBigOWith_inv
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
⊢ ‖f x‖ ≤ ε * ‖g x‖

Tactic:
hfg.trans (mul_le_mul_of_nonneg_right (inv_le_of_inv_le₀ ε0 hn.le) ?_)

Premises used: LT.lt.le, mul_le_mul_of_nonneg_right, inv_le_of_inv_le₀, LE.le.trans
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
mpr : 0 ≤ ‖g x‖
⊢ ‖f x‖ ≤ ε * ‖g x‖

Tactic:
refine hfg.trans (mul_le_mul_of_nonneg_right (inv_le_of_inv_le₀ ε0 hn.le) ?_)

Premises used: LT.lt.le, mul_le_mul_of_nonneg_right, inv_le_of_inv_le₀, LE.le.trans
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
⊢ 0 ≤ ‖g x‖

Tactic:
h₀.elim (fun hf => nonneg_of_mul_nonneg_right ((hf x).trans hfg) ?_) fun h => h x

Premises used: nonneg_of_mul_nonneg_right, LE.le.trans, Or.elim
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
mpr : ∀ (hf : ∀ (x : α), 0 ≤ ‖f x‖), LT.lt (α := ℝ) 0 (↑n : ℝ)⁻¹
⊢ 0 ≤ ‖g x‖

Tactic:
refine h₀.elim (fun hf => nonneg_of_mul_nonneg_right ((hf x).trans hfg) ?_) fun h => h x

Premises used: nonneg_of_mul_nonneg_right, LE.le.trans, Or.elim
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)⁻¹

Tactic:
inv_pos.2 hn₀

Premises used: Iff.mpr, inv_pos
-- 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‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
n : ℕ
hn : ε⁻¹ < (↑n : ℝ)
hn₀ : LT.lt (α := ℝ) 0 (↑n : ℝ)
x : α
hfg : ‖f x‖ ≤ (↑n : ℝ)⁻¹ * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)⁻¹

Tactic:
exact inv_pos.2 hn₀

Premises used: Iff.mpr, inv_pos
-- 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' ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f x‖ ≤ ‖g' x‖

Tactic:
isLittleO_iff_nat_mul_le_aux (Or.inr fun _x => norm_nonneg _)

Premises used: Asymptotics.isLittleO_iff_nat_mul_le_aux, norm_nonneg, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ f' =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, (↑n : ℝ) * ‖f' x‖ ≤ ‖g x‖

Tactic:
isLittleO_iff_nat_mul_le_aux (Or.inl fun _x => norm_nonneg _)

Premises used: Asymptotics.isLittleO_iff_nat_mul_le_aux, Or.inl, norm_nonneg
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
inst_2 : Subsingleton E'
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖g' x‖

Tactic:
simp [Subsingleton.elim (f' _) 0, mul_nonneg hc.le]

Premises used: mul_nonneg, LT.lt.le, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst : SeminormedAddCommGroup E'
inst_1 : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
inst_2 : Subsingleton E'
⊢ f' =O[l] g'

Tactic:
isLittleO_of_subsingleton.isBigO

Premises used: Asymptotics.IsLittleO.isBigO, Asymptotics.isLittleO_of_subsingleton
-- 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₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
simp : (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂

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_4
inst : Norm E
inst_1 : Norm F
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
subst : (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖

Tactic:
subst c₂
-- 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₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
h : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
⊢ (∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖

Tactic:
apply Filter.eventually_congr

Premises used: Filter.eventually_congr
-- 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₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
h : ∀ (a : α) (e₁ : f₁ a = f₂ a) (e₂ : g₁ a = g₂ a), ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
⊢ ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖

Tactic:
filter_upwards [hf, hg] with _ e₁ e₂
-- 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₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a : α
e₁ : f₁ a = f₂ a
e₂ : g₁ a = g₂ a
h : ‖f₂ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
h₁ h₂ : ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖
⊢ ‖f₁ a‖ ≤ c₁ * ‖g₁ a‖ ↔ ‖f₂ a‖ ≤ c₁ * ‖g₂ a‖

Tactic:
rw [e₁, e₂]
-- 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₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
h : IsBigOWith c₁ l f₁ g₁
hc : c₁ = c₂
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ IsBigOWith c₂ l f₂ g₂

Tactic:
(isBigOWith_congr hc hf hg).mp h

Premises used: Asymptotics.isBigOWith_congr, Iff.mp
-- 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₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
h : IsBigOWith c₁ l f₁ g₁
hc : c₁ = c₂
hf : ∀ (x : α), f₁ x = f₂ x
hg : ∀ (x : α), g₁ x = g₂ x
⊢ IsBigOWith c₂ l f₂ g₂

Tactic:
h.congr' hc (univ_mem' hf) (univ_mem' hg)

Premises used: Asymptotics.IsBigOWith.congr', Filter.univ_mem'
-- 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 : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E
h : IsBigOWith c l f₁ g
hf : ∀ (x : α), f₁ x = f₂ x
⊢ IsBigOWith c l f₂ g

Tactic:
h.congr rfl hf fun _ => rfl

Premises used: Asymptotics.IsBigOWith.congr, rfl
-- 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
l : Filter α
g₁ g₂ : α → F
h : IsBigOWith c l f g₁
hg : ∀ (x : α), g₁ x = g₂ x
⊢ IsBigOWith c l f g₂

Tactic:
h.congr rfl (fun _ => rfl) hg

Premises used: Asymptotics.IsBigOWith.congr, rfl
-- 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₁ c₂ : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c₁ l f g
hc : c₁ = c₂
⊢ IsBigOWith c₂ l f g

Tactic:
h.congr hc (fun _ => rfl) fun _ => rfl

Premises used: Asymptotics.IsBigOWith.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
simp : (∃ (c : ℝ), IsBigOWith c l f₁ g₁) ↔ ∃ (c : ℝ), IsBigOWith c l f₂ g₂
⊢ f₁ =O[l] g₁ ↔ f₂ =O[l] g₂

Tactic:
simp only [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
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∃ (c : ℝ), IsBigOWith c l f₁ g₁) ↔ ∃ (c : ℝ), IsBigOWith c l f₂ g₂

Tactic:
exists_congr fun c => isBigOWith_congr rfl hf hg

Premises used: Asymptotics.isBigOWith_congr, exists_congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∃ (c : ℝ), IsBigOWith c l f₁ g₁) ↔ ∃ (c : ℝ), IsBigOWith c l f₂ g₂

Tactic:
exact exists_congr fun c => isBigOWith_congr rfl hf hg

Premises used: Asymptotics.isBigOWith_congr, exists_congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
h : f₁ =O[l] g₁
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₂ =O[l] g₂

Tactic:
(isBigO_congr hf hg).mp h

Premises used: Asymptotics.isBigO_congr, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
h : f₁ =O[l] g₁
hf : ∀ (x : α), f₁ x = f₂ x
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f₂ =O[l] g₂

Tactic:
h.congr' (univ_mem' hf) (univ_mem' hg)

Premises used: Asymptotics.IsBigO.congr', Filter.univ_mem'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
g : α → F
l : Filter α
f₁ f₂ : α → E
h : f₁ =O[l] g
hf : ∀ (x : α), f₁ x = f₂ x
⊢ f₂ =O[l] g

Tactic:
h.congr hf fun _ => rfl

Premises used: Asymptotics.IsBigO.congr, rfl
-- 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
l : Filter α
g₁ g₂ : α → F
h : f =O[l] g₁
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f =O[l] g₂

Tactic:
h.congr (fun _ => rfl) hg

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

Tactic:
simp only [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
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂

Tactic:
forall₂_congr fun c _hc => isBigOWith_congr (Eq.refl c) hf hg

Premises used: Asymptotics.isBigOWith_congr, forall₂_congr, Eq.refl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂

Tactic:
exact forall₂_congr fun c _hc => isBigOWith_congr (Eq.refl c) hf hg

Premises used: Asymptotics.isBigOWith_congr, forall₂_congr, Eq.refl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
h : f₁ =o[l] g₁
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₂ =o[l] g₂

Tactic:
(isLittleO_congr hf hg).mp h

Premises used: Asymptotics.isLittleO_congr, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
h : f₁ =o[l] g₁
hf : ∀ (x : α), f₁ x = f₂ x
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f₂ =o[l] g₂

Tactic:
h.congr' (univ_mem' hf) (univ_mem' hg)

Premises used: Asymptotics.IsLittleO.congr', Filter.univ_mem'
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
g : α → F
l : Filter α
f₁ f₂ : α → E
h : f₁ =o[l] g
hf : ∀ (x : α), f₁ x = f₂ x
⊢ f₂ =o[l] g

Tactic:
h.congr hf fun _ => rfl

Premises used: Asymptotics.IsLittleO.congr, rfl
-- 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
l : Filter α
g₁ g₂ : α → F
h : f =o[l] g₁
hg : ∀ (x : α), g₁ x = g₂ x
⊢ f =o[l] g₂

Tactic:
h.congr (fun _ => rfl) hg

Premises used: Asymptotics.IsLittleO.congr, rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g : α → F
hf : f₁ =ᶠ[l] f₂
h : f₂ =O[l] g
⊢ f₁ =O[l] g

Tactic:
h.congr' hf.symm EventuallyEq.rfl

Premises used: Asymptotics.IsBigO.congr', Filter.EventuallyEq.rfl, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g : α → F
hf : f₁ =ᶠ[l] f₂
h : f₂ =o[l] g
⊢ f₁ =o[l] g

Tactic:
h.congr' hf.symm EventuallyEq.rfl

Premises used: Asymptotics.IsLittleO.congr', Filter.EventuallyEq.rfl, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α → E
g₁ g₂ : α → F
h : f =O[l] g₁
hg : g₁ =ᶠ[l] g₂
⊢ f =O[l] g₂

Tactic:
h.congr' EventuallyEq.rfl hg

Premises used: Asymptotics.IsBigO.congr', Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α → E
g₁ g₂ : α → F
h : f =o[l] g₁
hg : g₁ =ᶠ[l] g₂
⊢ f =o[l] g₂

Tactic:
h.congr' EventuallyEq.rfl hg

Premises used: Asymptotics.IsLittleO.congr', Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
hcfg : IsBigOWith c l f g
k : β → α
l' : Filter β
hk : Tendsto k l' l
⊢ IsBigOWith c l' (f ∘ k) (g ∘ k)

Tactic:
IsBigOWith.of_bound <| hk hcfg.bound

Premises used: Asymptotics.IsBigOWith.bound, Asymptotics.IsBigOWith.of_bound
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hfg : f =O[l] g
k : β → α
l' : Filter β
hk : Tendsto k l' l
⊢ (f ∘ k) =O[l'] (g ∘ k)

Tactic:
isBigO_iff_isBigOWith.2 <| hfg.isBigOWith.imp fun _c h => h.comp_tendsto hk

Premises used: Iff.mpr, Exists.imp, Asymptotics.IsBigO.isBigOWith, Asymptotics.isBigO_iff_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
rw :
  IsBigO.{0, u_3, u_4} (E := E) (F := F) cofinite (fun (n : ℤ) ↦ f ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)) fun (n : ℤ) ↦
    g ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)
⊢ IsBigO.{0, u_3, u_4} (E := E) (F := F) cofinite (fun (n : ℤ) ↦ f (-n)) fun (n : ℤ) ↦ g (-n)

Tactic:
rw [← Equiv.neg_apply]

Premises used: Equiv.neg_apply
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
⊢ IsBigO.{0, u_3, u_4} (E := E) (F := F) cofinite (fun (n : ℤ) ↦ f ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)) fun (n : ℤ) ↦
    g ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)

Tactic:
hf.comp_tendsto (Equiv.neg ℤ).injective.tendsto_cofinite

Premises used: Equiv.neg, Int, Function.Injective.tendsto_cofinite, Equiv.injective, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : ℤ → E
g : ℤ → F
hf : f =O[cofinite] g
⊢ IsBigO.{0, u_3, u_4} (E := E) (F := F) cofinite (fun (n : ℤ) ↦ f ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)) fun (n : ℤ) ↦
    g ((Equiv.neg ℤ : (a : ℤ) → ℤ) n)

Tactic:
exact hf.comp_tendsto (Equiv.neg ℤ).injective.tendsto_cofinite

Premises used: Equiv.neg, Int, Function.Injective.tendsto_cofinite, Equiv.injective, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Defs
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
hfg : f =o[l] g
k : β → α
l' : Filter β
hk : Tendsto k l' l
⊢ (f ∘ k) =o[l'] (g ∘ k)

Tactic:
IsLittleO.of_isBigOWith fun _c cpos => (hfg.forall_isBigOWith cpos).comp_tendsto hk

Premises used: Asymptotics.IsLittleO.forall_isBigOWith, Asymptotics.IsLittleO.of_isBigOWith, Asymptotics.IsBigOWith.comp_tendsto