Almost sure limits are almost surely unique

Stream: Is there code for X?

[Peter Pfaffelhuber]

If $X_n \to Y$ almost surely, and $X_n \to Z$ almost surely (wrt some measure), then $Y=Z$ almost surely. This basic fact must be in Mathlib, I guess, but I cannot find it. Or does it follow from some more general filter results?
The implementation is not hard, but I want to learn how this is implemented in mathlib:

example {α ι E : Type*} [TopologicalSpace E] [T2Space E] {x : MeasurableSpace α} {μ : Measure α} {Y Z : α → E} {X : ι → α → E} {l : Filter ι} [l.NeBot]
(hY : ∀ᵐ ω ∂μ, Filter.Tendsto (fun i => X i ω) l (nhds (Y ω))) (hZ
: ∀ᵐ ω ∂μ, Filter.Tendsto (fun i => X i ω) l (nhds (Z ω))) : Y =ᵐ[μ] Z := by
  filter_upwards [hY, hZ] with ω hY1 hZ1
  exact tendsto_nhds_unique hY1 hZ1

[Kevin Buzzard]

Nice proof! Could try loogling for theorems whose conclusion is that two things are almost surely equal if you're wondering if it's there already?

[Yury G. Kudryashov]

As you can see from the proof, it works for any filter.

[Yury G. Kudryashov]

@loogle Filter.Tendsto, T2Space, |- Filter.EventuallyEq _ _ _

[loogle]

:shrug: nothing found

[Yury G. Kudryashov]

Probably, it's not there.