tendsto.nhds_congr

Stream: maths

[Yury G. Kudryashov]

Hi, do we have the following lemma somewhere in mathlib?

lemma tendsto.nhds_congr [uniform_space β] {l : filter α} {f g : α → β} {y : β}
  (hf : tendsto f l (𝓝 y)) (hfg : tendsto (λ x, (f x, g x)) l (𝓤 β)) :
  tendsto g l (𝓝 y) :=
sorry

I have a proof, just wonder if I should PR it, or use some existing lemma instead.

[Yury G. Kudryashov]

Probably this can be reformulated in terms of two filters on β without α.