awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u v w : α → β
l : Filter α
htu : t ~[l] u
hvw : v ~[l] w
⊢ t / v ~[l] u / w

Tactic:
simpa only [div_eq_mul_inv] using htu.mul hvw.inv

Premises used: Asymptotics.IsEquivalent.mul, div_eq_mul_inv, Asymptotics.IsEquivalent.inv
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
⊢ HPow.hPow (β := ℕ) t 0 ~[l] HPow.hPow (β := ℕ) u 0

Tactic:
simpa using IsEquivalent.refl

Premises used: Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
n : ℕ
ih : t ^ n ~[l] u ^ n
⊢ t ^ (n + 1) ~[l] u ^ (n + 1)

Tactic:
simpa [pow_succ] using ih.mul h

Premises used: pow_succ, Asymptotics.IsEquivalent.mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
n : ℕ
zero : HPow.hPow (β := ℕ) t 0 ~[l] HPow.hPow (β := ℕ) u 0
succ : ∀ (n : ℕ) (ih : t ^ n ~[l] u ^ n), t ^ (n + 1) ~[l] u ^ (n + 1)
⊢ t ^ n ~[l] u ^ n

Tactic:
induction n with
  | zero => simpa using IsEquivalent.refl
  | succ _ ih => simpa [pow_succ] using ih.mul h

Premises used: pow_succ, Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
z : ℤ
a : ℕ
⊢ t ^ Int.ofNat a ~[l] u ^ Int.ofNat a

Tactic:
simpa using h.pow _

Premises used: Asymptotics.IsEquivalent.pow
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
z : ℤ
a : ℕ
⊢ t ^ Int.negSucc a ~[l] u ^ Int.negSucc a

Tactic:
simpa using (h.pow _).inv

Premises used: Asymptotics.IsEquivalent.pow, Asymptotics.IsEquivalent.inv
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
z : ℤ
⊢ t ^ z ~[l] u ^ z

Tactic:
match z with
  | Int.ofNat _ => simpa using h.pow _
  | Int.negSucc _ => simpa using (h.pow _).inv
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atTop
⊢ Tendsto v l atTop

Tactic:
let ⟨φ, hφ, h⟩ := huv.symm.exists_eq_mul
  Tendsto.congr' h.symm (mul_comm u φ ▸ hu.atTop_mul_pos zero_lt_one hφ)

Premises used: Eq.rec, Filter.atTop, zero_lt_one, Asymptotics.IsEquivalent.exists_eq_mul, Filter.Tendsto, mul_comm, _private.0.Asymptotics.IsEquivalent.tendsto_atTop.match_1, Filter.Tendsto.atTop_mul_pos, Filter.Tendsto.congr', Filter.EventuallyEq.symm, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
⊢ Tendsto u l atTop ↔ Tendsto v l atTop

Tactic:
⟨huv.tendsto_atTop, huv.symm.tendsto_atTop⟩

Premises used: Asymptotics.IsEquivalent.tendsto_atTop, Iff.intro, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ Tendsto.{u_1, u_2} (β := β) (Neg.neg ∘ fun (x : α) ↦ -v x) l atBot

Tactic:
tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)

Premises used: Filter.tendsto_neg_atBot_atTop, Filter.tendsto_neg_atTop_atBot, Asymptotics.IsEquivalent.neg, Asymptotics.IsEquivalent.tendsto_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
h : v = Neg.neg ∘ fun (x : α) ↦ -v x
⊢ Tendsto v l atBot

Tactic:
convert! tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)

Premises used: Filter.tendsto_neg_atBot_atTop, Filter.tendsto_neg_atTop_atBot, Asymptotics.IsEquivalent.neg, Asymptotics.IsEquivalent.tendsto_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
h : ∀ (x : α), v x = (Neg.neg ∘ fun (x : α) ↦ -v x) x
⊢ v = Neg.neg ∘ fun (x : α) ↦ -v x

Tactic:
ext
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
x : α
⊢ v x = (Neg.neg ∘ fun (x : α) ↦ -v x) x

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
⊢ Tendsto u l atBot ↔ Tendsto v l atBot

Tactic:
⟨huv.tendsto_atBot, huv.symm.tendsto_atBot⟩

Premises used: Asymptotics.IsEquivalent.tendsto_atBot, Iff.intro, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
obtain :
  ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h_eq : u =ᶠ[l] φ * v),
    ∃ (φ : α → β), (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β), (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v

Tactic:
obtain ⟨φ, hφ, h_eq⟩ := h.exists_eq_mul

Premises used: Asymptotics.IsEquivalent.exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h_eq : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β), (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v

Tactic:
⟨φ, hφ.eventually_const_lt (zero_lt_one' β), h_eq⟩

Premises used: Filter.Tendsto.eventually_const_lt, zero_lt_one', And.intro, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h_eq : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β), (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v

Tactic:
exact ⟨φ, hφ.eventually_const_lt (zero_lt_one' β), h_eq⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 ≤ v t
obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, 0 ≤ u x
⊢ ∀ᶠ (x : α) in l, 0 ≤ u x

Tactic:
obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul

Premises used: Asymptotics.IsEquivalent.exists_pos_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 ≤ v t
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, 0 ≤ u x

Tactic:
(hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_nonneg hφ.le hv)

Premises used: mul_nonneg, Eq.rec, Filter.Eventually.and, LT.lt.le, LE.le, Filter.Eventually.mono, _private.0.Asymptotics.IsEquivalent.eventually_nonneg.match_1, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 ≤ v t
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, 0 ≤ u x

Tactic:
exact (hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_nonneg hφ.le hv)

Premises used: Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 < v t
obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, 0 < u x
⊢ ∀ᶠ (x : α) in l, 0 < u x

Tactic:
obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul

Premises used: Asymptotics.IsEquivalent.exists_pos_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 < v t
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, 0 < u x

Tactic:
(hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_pos hφ hv)

Premises used: Eq.rec, Filter.Eventually.and, _private.0.Asymptotics.IsEquivalent.eventually_pos.match_1, Filter.Eventually.mono, mul_pos, LT.lt, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 < v t
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, 0 < u x

Tactic:
exact (hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_pos hφ hv)

Premises used: Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t ≤ 0
obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, u x ≤ 0
⊢ ∀ᶠ (x : α) in l, u x ≤ 0

Tactic:
obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul

Premises used: Asymptotics.IsEquivalent.exists_pos_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t ≤ 0
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, u x ≤ 0

Tactic:
(hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦
    h_eq ▸ mul_nonpos_of_nonneg_of_nonpos hφ.le hv)

Premises used: Eq.rec, Filter.Eventually.and, LT.lt.le, LE.le, Filter.Eventually.mono, _private.0.Asymptotics.IsEquivalent.eventually_nonpos.match_1, mul_nonpos_of_nonneg_of_nonpos, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t ≤ 0
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, u x ≤ 0

Tactic:
exact (hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦
    h_eq ▸ mul_nonpos_of_nonneg_of_nonpos hφ.le hv)

Premises used: Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t < 0
obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, u x < 0
⊢ ∀ᶠ (x : α) in l, u x < 0

Tactic:
obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul

Premises used: Asymptotics.IsEquivalent.exists_pos_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t < 0
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, u x < 0

Tactic:
(hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_neg_of_pos_of_neg hφ hv)

Premises used: Eq.rec, Filter.Eventually.and, Filter.Eventually.mono, LT.lt, _private.0.Asymptotics.IsEquivalent.eventually_neg.match_1, OfNat.ofNat, Eq.symm, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t < 0
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, u x < 0

Tactic:
exact (hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_neg_of_pos_of_neg hφ hv)

Premises used: Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
simp : (u - v + (t - w)) =o[l] (v + w)
⊢ u + t ~[l] v + w

Tactic:
simp only [IsEquivalent, add_sub_add_comm]

Premises used: Asymptotics.IsEquivalent, add_sub_add_comm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
h : ∀ (x : α), v x + w x
| IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ v x + w x

Tactic:
enter [3, x]
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
x : α
h : |v x| + |w x|
| v x + w x

Tactic:
rw [← abs_eq_self.mpr (hu x), ← abs_eq_self.mpr (hw x)]

Premises used: Iff.mpr, abs_eq_self
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
h : ∀ (x : α), |v x| + |w x|
| IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ v x + w x

Tactic:
enter [3, x]; rw [← abs_eq_self.mpr (hu x), ← abs_eq_self.mpr (hw x)]
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
conv : IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ |v x| + |w x|
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ v x + w x

Tactic:
conv => enter [3, x]; rw [← abs_eq_self.mpr (hu x), ← abs_eq_self.mpr (hw x)]
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ |v x| + |w x|

Tactic:
simpa [← Real.norm_eq_abs] using .add_add htu hvw

Premises used: Real.norm_eq_abs
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
l : Filter α
u v : α → β
h : u =ᶠ[l] v
⊢ u ~[l] v

Tactic:
IsEquivalent.congr_right (isLittleO_refl_left _ _) h

Premises used: Asymptotics.IsEquivalent.congr_right, Asymptotics.isLittleO_refl_left
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
l : Filter α
f g₁ g₂ : α → β
h : f =ᶠ[l] g₁
h₂ : g₁ ~[l] g₂
⊢ f ~[l] g₂

Tactic:
h.isEquivalent.trans h₂

Premises used: Asymptotics.IsEquivalent.trans, Filter.EventuallyEq.isEquivalent
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
l : Filter α
f g₁ g₂ : α → β
h : f ~[l] g₁
h₂ : g₁ =ᶠ[l] g₂
⊢ f ~[l] g₂

Tactic:
h.trans h₂.isEquivalent

Premises used: Asymptotics.IsEquivalent.trans, Filter.EventuallyEq.isEquivalent
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
β₂ : Type u_3
inst : NormedAddCommGroup β
inst_1 : Norm β₂
l : Filter α
f g₁ : α → β
g₂ : α → β₂
h : f ~[l] g₁
h₂ : g₁ =O[l] g₂
⊢ f =O[l] g₂

Tactic:
IsBigO.trans h.isBigO h₂

Premises used: Asymptotics.IsEquivalent.isBigO, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
β₂ : Type u_3
inst : NormedAddCommGroup β
inst_1 : Norm β₂
l : Filter α
f : α → β₂
g₁ g₂ : α → β
h : f =O[l] g₁
h₂ : g₁ ~[l] g₂
⊢ f =O[l] g₂

Tactic:
IsBigO.trans h h₂.isBigO

Premises used: Asymptotics.IsEquivalent.isBigO, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
β₂ : Type u_3
inst : NormedAddCommGroup β
inst_1 : Norm β₂
l : Filter α
f g₁ : α → β
g₂ : α → β₂
h : f ~[l] g₁
h₂ : g₁ =o[l] g₂
⊢ f =o[l] g₂

Tactic:
IsBigO.trans_isLittleO h.isBigO h₂

Premises used: Asymptotics.IsEquivalent.isBigO, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
β₂ : Type u_3
inst : NormedAddCommGroup β
inst_1 : Norm β₂
l : Filter α
f : α → β₂
g₁ g₂ : α → β
h : f =o[l] g₁
h₂ : g₁ ~[l] g₂
⊢ f =o[l] g₂

Tactic:
IsLittleO.trans_isBigO h h₂.isBigO

Premises used: Asymptotics.IsEquivalent.isBigO, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
β₂ : Type u_3
inst : NormedAddCommGroup β
inst_1 : Norm β₂
l : Filter α
f g₁ : α → β
g₂ : α → β₂
h : f ~[l] g₁
h₂ : g₁ =Θ[l] g₂
⊢ f =Θ[l] g₂

Tactic:
IsTheta.trans h.isTheta h₂

Premises used: Asymptotics.IsTheta.trans, Asymptotics.IsEquivalent.isTheta
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
β₂ : Type u_3
inst : NormedAddCommGroup β
inst_1 : Norm β₂
l : Filter α
f : α → β₂
g₁ g₂ : α → β
h : f =Θ[l] g₁
h₂ : g₁ ~[l] g₂
⊢ f =Θ[l] g₂

Tactic:
IsTheta.trans h h₂.isTheta

Premises used: Asymptotics.IsTheta.trans, Asymptotics.IsEquivalent.isTheta
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
l : Filter α
α₂ : Type u_4
f g : α₂ → β
l' : Filter α₂
hfg : f ~[l'] g
k : α → α₂
hk : Tendsto k l l'
⊢ f ∘ k ~[l] g ∘ k

Tactic:
IsLittleO.comp_tendsto hfg hk

Premises used: Asymptotics.IsEquivalent, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
l : Filter α
α₂ : Type u_4
f g : α₂ → β
k : α → α₂
⊢ f ~[map k l] g ↔ f ∘ k ~[l] g ∘ k

Tactic:
isLittleO_map

Premises used: Asymptotics.IsEquivalent, Asymptotics.isLittleO_map
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
l : Filter α
f g : α → β
l' : Filter α
h : f ~[l'] g
hl : l ≤ l'
⊢ f ~[l] g

Tactic:
IsLittleO.mono h hl

Premises used: Asymptotics.IsEquivalent, Asymptotics.IsLittleO.mono
-- Module: Mathlib.Analysis.Asymptotics.Completion
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ IsBigO.{u_1, u_3, u_2} (E := F̂) l (fun (x : α) ↦ (↑(g x) : F̂)) f ↔ g =O[l] f

Tactic:
simp only [isBigO_iff, norm_coe]

Premises used: Asymptotics.isBigO_iff, UniformSpace.Completion.norm_coe
-- Module: Mathlib.Analysis.Asymptotics.Completion
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ (IsBigO.{u_1, u_2, u_3} (F := F̂) l f fun (x : α) ↦ (↑(g x) : F̂)) ↔ f =O[l] g

Tactic:
simp only [isBigO_iff, norm_coe]

Premises used: Asymptotics.isBigO_iff, UniformSpace.Completion.norm_coe
-- Module: Mathlib.Analysis.Asymptotics.Completion
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ IsTheta.{u_1, u_3, u_2} (E := F̂) l (fun (x : α) ↦ (↑(g x) : F̂)) f ↔ g =Θ[l] f

Tactic:
and_congr isBigO_completion_left isBigO_completion_right

Premises used: Asymptotics.isBigO_completion_right, Asymptotics.IsTheta, Asymptotics.isBigO_completion_left, and_congr
-- Module: Mathlib.Analysis.Asymptotics.Completion
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ (IsTheta.{u_1, u_2, u_3} (F := F̂) l f fun (x : α) ↦ (↑(g x) : F̂)) ↔ f =Θ[l] g

Tactic:
and_congr isBigO_completion_right isBigO_completion_left

Premises used: Asymptotics.isBigO_completion_right, Asymptotics.IsTheta, Asymptotics.isBigO_completion_left, and_congr
-- Module: Mathlib.Analysis.Asymptotics.Completion
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ IsLittleO.{u_1, u_3, u_2} (E := F̂) l (fun (x : α) ↦ (↑(g x) : F̂)) f ↔ g =o[l] f

Tactic:
simp only [isLittleO_iff, norm_coe]

Premises used: UniformSpace.Completion.norm_coe, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Asymptotics.Completion
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ (IsLittleO.{u_1, u_2, u_3} (F := F̂) l f fun (x : α) ↦ (↑(g x) : F̂)) ↔ f =o[l] g

Tactic:
simp only [isLittleO_iff, norm_coe]

Premises used: UniformSpace.Completion.norm_coe, 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 α
rw rw₁ : (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

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

Tactic:
simp only [IsBigO_def, IsBigOWith_def]

Premises used: Asymptotics.IsBigOWith_def, Asymptotics.IsBigO_def
-- 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, ‖f x‖ ≤ c * ‖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, ‖f x‖ ≤ c * ‖g x‖
refine₁ : ∀ (h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), f =O[l] g
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖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 : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [isBigO_iff] at h

Premises used: Asymptotics.isBigO_iff