-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem isEquivalent_iff_exists_eq_mul :
    u ~[l] v ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Proof state:
case h.e'_5.h
α : 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]

Result:
no goals

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

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

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

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
⊢ u ~[l] v ↔ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
rw [IsEquivalent, isLittleO_iff_exists_eq_mul]

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

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

Tactic:
exact hφ.add tendsto_const_nhds

Result:
no goals

Proof state:
case mpr.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 (1 - 1))

Tactic:
exact hφ.sub tendsto_const_nhds

Result:
no goals

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

Tactic:
convert h.add (EventuallyEq.refl l v) <;> simp [add_mul]

Result:
no goals

Proof state:
case mpr.intro.intro.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
convert h.sub (EventuallyEq.refl l v)

Result:
case h.e'_5.h
α : 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✝

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v) ↔ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]

Result:
case mp.intro.intro.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
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 β
u v : α → β
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 β
u v : α → β
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 β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

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

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

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