case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v → Tendsto (u / v) l (𝓝 1)

case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v ↔ Tendsto (u / v) l (𝓝 1)
constructor
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
⊢ Tendsto (u / v) l (𝓝 1)
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v → Tendsto (u / v) l (𝓝 1)
intro hequiv
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => (u - v) x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
⊢ Tendsto (u / v) l (𝓝 1)
have := hequiv.isLittleO.tendsto_div_nhds_zero
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => (u - v) x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
simp only [Pi.sub_apply, sub_div] at this
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
⊢ Tendsto (u / v) l (𝓝 1)
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
⊢ Tendsto (u / v) l (𝓝 1)
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
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
x✝ : α
⊢ (u / v) x✝ = u x✝ / v x✝ - v x✝ / v x✝ + v x✝ / v x✝

case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
⊢ Tendsto (u / v) l (𝓝 1)
convert this.add key
no goals
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
x✝ : α
⊢ (u / v) x✝ = u x✝ / v x✝ - v x✝ / v x✝ + v x✝ / v x✝
simp
no goals
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
hequiv : u ~[l] v
this : Tendsto (fun x => u x / v x - v x / v x) l (𝓝 0)
key : Tendsto (fun x => v x / v x) l (𝓝 1)
⊢ 1 = 0 + 1
norm_num
no goals
case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ Tendsto (u / v) l (𝓝 1) → u ~[l] v
exact isEquivalent_of_tendsto_one (hz.mono fun x hnvz hz ↦ (hnvz hz).elim)