α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ (∃ φ _hφ, u - v =ᶠ[l] φ * v) ↔ ∃ φ x, u =ᶠ[l] φ * v
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ u ~[l] v ↔ ∃ φ x, u =ᶠ[l] φ * v
rw [IsEquivalent, isLittleO_iff_exists_eq_mul]
case mp.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 1)

case mp.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v

case mpr.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)

case mpr.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
⊢ (∃ φ _hφ, u - v =ᶠ[l] φ * v) ↔ ∃ φ x, u =ᶠ[l] φ * v
constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine' ⟨φ + 1, _, _⟩; refine' ⟨φ - 1, _, _⟩]
case mp.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 (0 + 1))
case mp.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 1)
conv in 𝓝 _ => rw [← zero_add (1 : β)]
no goals
case mp.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ Tendsto (φ + 1) l (𝓝 (0 + 1))
exact hφ.add tendsto_const_nhds
no goals
case mp.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 0)
h : u - v =ᶠ[l] φ * v
⊢ u =ᶠ[l] (φ + 1) * v
convert h.add (EventuallyEq.refl l v) <;> simp [add_mul]
case mpr.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (1 - 1))
case mpr.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)
conv in 𝓝 _ => rw [← sub_self (1 : β)]
no goals
case mpr.intro.intro.refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (1 - 1))
exact hφ.sub tendsto_const_nhds
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((φ - 1) * v) x✝ = (φ * v) x✝ - v x✝
case mpr.intro.intro.refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v
convert h.sub (EventuallyEq.refl l v)
no goals
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((φ - 1) * v) x✝ = (φ * v) x✝ - v x✝
simp [sub_mul]