∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' → (Filter.Tendsto (norm ∘ f') l Filter.atTop ↔ Filter.Tendsto (norm ∘ g') l Filter.atTop)