no goals
α : Type u_1
β : Type u_2
inst✝ : NormedField β
t u v w : α → β
l : Filter α
htu : t ~[l] u
hvw : v ~[l] w
⊢ (fun x => t x / v x) ~[l] fun x => u x / w x
simpa only [div_eq_mul_inv] using htu.mul hvw.inv