awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v

Tactic:
⟨φ - 1, ?_, ?_⟩

Premises used: HSub.hSub, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
mpr : Tendsto (φ - 1) l (𝓝 0)
mpr₁ : u - v =ᶠ[l] (φ - 1) * v
⊢ ∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v

Tactic:
refine ⟨φ - 1, ?_, ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
mp : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), Tendsto (φ + 1) l (𝓝 1)
mp₁ : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 0)) (h : u - v =ᶠ[l] φ * v), u =ᶠ[l] (φ + 1) * v
mpr : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h : u =ᶠ[l] φ * v), Tendsto (φ - 1) l (𝓝 0)
mpr₁ : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h : u =ᶠ[l] φ * v), u - v =ᶠ[l] (φ - 1) * v
⊢ (∃ (φ : α → β), Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
rw : 𝓝 (HAdd.hAdd (α := β) 0 1)
| 𝓝 1

Tactic:
rw [← zero_add (1 : β)]

Premises used: zero_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
mp : Tendsto (φ + 1) l (𝓝 (HAdd.hAdd (α := β) 0 1))
⊢ Tendsto (φ + 1) l (𝓝 1)

Tactic:
conv in 𝓝 _ => rw [← zero_add (1 : β)]

Premises used: nhds, zero_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 (HAdd.hAdd (α := β) 0 1))

Tactic:
hφ.add tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 (HAdd.hAdd (α := β) 0 1))

Tactic:
exact hφ.add tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ EventuallyEq.{u_1, u_2} (β := β) l (fun (i : α) ↦ (u - v) i + v i) fun (i : α) ↦ (φ * v) i + v i

Tactic:
h.fun_add (EventuallyEq.refl l v)

Premises used: Filter.EventuallyEq.refl, Filter.EventuallyEq.fun_add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
h₁ : ∀ (x : α), u x = (u - v) x + v x
h₂ : ∀ (x : α), ((φ + 1) * v) x = (φ * v) x + v x
⊢ u =ᶠ[l] (φ + 1) * v

Tactic:
convert! h.fun_add (EventuallyEq.refl l v)

Premises used: Filter.EventuallyEq.refl, Filter.EventuallyEq.fun_add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
x : α
⊢ u x = (u - v) x + v x

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
x : α
⊢ ((φ + 1) * v) x = (φ * v) x + v x

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
rw : 𝓝 (HSub.hSub (α := β) 1 1)
| 𝓝 0

Tactic:
rw [← sub_self (1 : β)]

Premises used: sub_self, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
mpr : Tendsto (φ - 1) l (𝓝 (HSub.hSub (α := β) 1 1))
⊢ Tendsto (φ - 1) l (𝓝 0)

Tactic:
conv in 𝓝 _ => rw [← sub_self (1 : β)]

Premises used: sub_self, nhds, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (HSub.hSub (α := β) 1 1))

Tactic:
hφ.sub tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (HSub.hSub (α := β) 1 1))

Tactic:
exact hφ.sub tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ EventuallyEq.{u_1, u_2} (β := β) l (fun (i : α) ↦ u i - v i) fun (i : α) ↦ (φ * v) i - v i

Tactic:
h.fun_sub (EventuallyEq.refl l v)

Premises used: Filter.EventuallyEq.fun_sub, Filter.EventuallyEq.refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
h₁ : ∀ (x : α), ((φ - 1) * v) x = (φ * v) x - v x
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
convert! h.fun_sub (EventuallyEq.refl l v)

Premises used: Filter.EventuallyEq.fun_sub, Filter.EventuallyEq.refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x : α
⊢ ((φ - 1) * v) x = (φ * v) x - v x

Tactic:
simp [sub_mul]

Premises used: sub_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
isEquivalent_iff_exists_eq_mul.mp huv

Premises used: Asymptotics.isEquivalent_iff_exists_eq_mul, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
this : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
rw : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
⊢ u ~[l] v

Tactic:
rw [isEquivalent_iff_exists_eq_mul]

Premises used: Asymptotics.isEquivalent_iff_exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
this : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
⟨u / v, huv, this.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩

Premises used: div_mul_cancel_of_imp, HDiv.hDiv, Filter.Eventually.mono, Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
this : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
exact ⟨u / v, huv, this.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
suffices : ∀ᶠ (x : α) in l, v x = 0 → u x = 0
⊢ u ~[l] v

Tactic:
suffices ∀ᶠ x in l, v x = 0 → u x = 0 by
    rw [isEquivalent_iff_exists_eq_mul]
    exact ⟨u / v, huv, this.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
by_contra! : ∀ (h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0), False
⊢ ∀ᶠ (x : α) in l, v x = 0 → u x = 0

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0
x : α
h_1 : v x = 0 ∧ u x ≠ 0
hv : v x = 0
hu : u x ≠ 0
⊢ (u / v) x = 0

Tactic:
simp [hv]
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0
⊢ ∃ᶠ (t : α) in l, (u / v) t = 0

Tactic:
replace h : ∃ᶠ t in l, (u / v) t = 0 := h.mono fun x ⟨hv, hu⟩ ↦ by simp [hv]
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (t : α) in l, (u / v) t = 0
⊢ False

Tactic:
simpa using tendsto_nhds_unique_of_frequently_eq (b := 0) huv tendsto_const_nhds h

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_frequently_eq
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
mp : u ~[l] v → Tendsto (u / v) l (𝓝 1)
mpr : Tendsto (u / v) l (𝓝 1) → u ~[l] v
⊢ u ~[l] v ↔ Tendsto (u / v) l (𝓝 1)

Tactic:
constructor
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
⊢ Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ (u - v) x / v x) l (𝓝 0)

Tactic:
have := hequiv.isLittleO.tendsto_div_nhds_zero
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ (u - v) x / v x) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)

Tactic:
simp only [Pi.sub_apply, sub_div] at this

Premises used: sub_div, Pi.sub_apply
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)

Tactic:
have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
      (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)
⊢ Tendsto (fun (x : α) ↦ u x / v x - v x / v x + v x / v x) l (𝓝 (HAdd.hAdd (α := β) 0 1))

Tactic:
this.add key

Premises used: Filter.Tendsto.add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)
h : ∀ (x : α), (u / v) x = u x / v x - v x / v x + v x / v x
h₁ : 1 = HAdd.hAdd (α := β) 0 1
⊢ Tendsto (u / v) l (𝓝 1)

Tactic:
convert! this.add key

Premises used: Filter.Tendsto.add
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)
x : α
⊢ (u / v) x = u x / v x - v x / v x + v x / v x

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ u x / v x - v x / v x) l (𝓝 0)
key : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ v x / v x) l (𝓝 1)
⊢ 1 = HAdd.hAdd (α := β) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v

Tactic:
isEquivalent_of_tendsto_one

Premises used: Asymptotics.isEquivalent_of_tendsto_one
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v

Tactic:
exact isEquivalent_of_tendsto_one

Premises used: Asymptotics.isEquivalent_of_tendsto_one
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
rcases :
  ∀ (φ : α → 𝕜) (hφ : Tendsto φ l (𝓝 1)) (habφ : a =ᶠ[l] φ * b),
    IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x
⊢ IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x

Tactic:
rcases hab.exists_eq_mul with ⟨φ, hφ, habφ⟩

Premises used: Asymptotics.IsEquivalent.exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ EventuallyEq.{u_1, u_2} (β := E) l (fun (i : α) ↦ a i • u i - b i • v i) fun (i : α) ↦ (φ * b) i • u i - b i • v i

Tactic:
(habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).fun_sub
        (EventuallyEq.refl _ fun x ↦ b x • v x)

Premises used: Filter.EventuallyEq.fun_sub, Filter.EventuallyEq.comp₂, Filter.EventuallyEq.refl, HSMul.hSMul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
h : Eq (α := α → E) (fun (x : α) ↦ b x • (φ x • u x - v x)) fun (i : α) ↦ (φ * b) i • u i - b i • v i
⊢ (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)

Tactic:
convert!
      (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).fun_sub
        (EventuallyEq.refl _ fun x ↦ b x • v x) using 1

Premises used: Filter.EventuallyEq.fun_sub, Filter.EventuallyEq.comp₂, Filter.EventuallyEq.refl, HSMul.hSMul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
h : ∀ (x : α), b x • (φ x • u x - v x) = (φ * b) x • u x - b x • v x
⊢ Eq (α := α → E) (fun (x : α) ↦ b x • (φ x • u x - v x)) fun (i : α) ↦ (φ * b) i • u i - b i • v i

Tactic:
ext
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
x : α
h : b x • (φ x • u x - v x) = (φ x * b x) • u x - b x • v x
h₁ : b x • (φ x • u x - v x) = (b x * φ x) • u x - b x • v x
h₂ : b x • (φ x • u x - v x) = b x • φ x • u x - b x • v x
h₃ h₄ : b x • (φ x • u x - v x) = b x • (φ x • u x - v x)
⊢ b x • (φ x • u x - v x) = (φ * b) x • u x - b x • v x

Tactic:
rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]

Premises used: Pi.mul_apply, smul_sub, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)

Tactic:
have : ((fun x ↦ a x • u x) - (fun x ↦ b x • v x)) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x) := by
    convert!
      (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).fun_sub
        (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
    ext
    rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
⊢ IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x

Tactic:
(isLittleO_congr this.symm <| EventuallyEq.rfl).mp ((isBigO_refl b l).smul_isLittleO ?_)

Premises used: Asymptotics.isLittleO_congr, Asymptotics.IsEquivalent, Iff.mp, Filter.EventuallyEq.rfl, Filter.EventuallyEq.symm, Asymptotics.IsBigO.smul_isLittleO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
refine : IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
⊢ IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x

Tactic:
refine (isLittleO_congr this.symm <| EventuallyEq.rfl).mp ((isBigO_refl b l).smul_isLittleO ?_)

Premises used: Asymptotics.isLittleO_congr, Iff.mp, Filter.EventuallyEq.rfl, Filter.EventuallyEq.symm, Asymptotics.IsBigO.smul_isLittleO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
rcases : ∀ (C : ℝ) (hC : C > 0) (hCuv : IsBigOWith C l u v), IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
⊢ IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v

Tactic:
rcases huv.isBigO.exists_pos with ⟨C, hC, hCuv⟩

Premises used: Asymptotics.IsEquivalent.isBigO, Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
rw :
  ∀ (hab : (a - b) =o[l] b) (huv : (u - v) =o[l] v) (φ : α → 𝕜) (hφ : Tendsto φ l (𝓝 1)) (habφ : a =ᶠ[l] φ * b)
    (this :
      (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
        b x • (φ x • u x - v x))
    (C : ℝ) (hC : C > 0) (hCuv : IsBigOWith C l u v), IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
⊢ IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v

Tactic:
rw [IsEquivalent] at *

Premises used: Asymptotics.IsEquivalent
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : (a - b) =o[l] b
huv : (u - v) =o[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
rw :
  ∀ (hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖)
    (huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖) (φ : α → 𝕜) (hφ : Tendsto φ l (𝓝 1))
    (habφ : a =ᶠ[l] φ * b)
    (this :
      (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
        b x • (φ x • u x - v x))
    (C : ℝ) (hC : C > 0) (hCuv : IsBigOWith C l u v) ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
⊢ IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v

Tactic:
rw [isLittleO_iff] at *

Premises used: Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖

Tactic:
rw [IsBigOWith] at hCuv

Premises used: Asymptotics.IsBigOWith
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
⊢ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε

Tactic:
simp only [Metric.tendsto_nhds, dist_eq_norm] at hφ

Premises used: dist_eq_norm, Metric.tendsto_nhds
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C

Tactic:
specialize hφ (c / 2 / C) (div_pos (div_pos hc zero_lt_two) hC)

Premises used: HDiv.hDiv, div_pos, zero_lt_two, OfNat.ofNat