α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
⊢ ((fun x => -u x) - fun x => -v x) =o[l] fun x => -v x
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
⊢ (fun x => -u x) ~[l] fun x => -v x
rw [IsEquivalent]
case h.e'_7.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
x✝ : α
⊢ ((fun x => -u x) - fun x => -v x) x✝ = -(u - v) x✝
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
⊢ ((fun x => -u x) - fun x => -v x) =o[l] fun x => -v x
convert huv.isLittleO.neg_left.neg_right
no goals
case h.e'_7.h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
x✝ : α
⊢ ((fun x => -u x) - fun x => -v x) x✝ = -(u - v) x✝
simp [neg_add_eq_sub]