-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_ae_unique [MetricSpace E] {g h : α → E} {f : ι → α → E} {u : Filter ι}
    [NeBot u] [IsCountablyGenerated u] (hg : TendstoInMeasure μ f u g)
    (hh : TendstoInMeasure μ f u h) : g =ᵐ[μ] h

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
⊢ g =ᶠ[ae μ] h

Tactic:
obtain ⟨ns, h1, h1'⟩ := hg.exists_seq_tendsto_ae'

Result:
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ g =ᶠ[ae μ] h

Proof state:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun i => f (ns i) ω) atTop (𝓝 (g ω))
hh1 : Tendsto (fun i => (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))
⊢ g ω = h ω

Tactic:
exact tendsto_nhds_unique (hg1.comp h2) hh1

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
⊢ g =ᶠ[ae μ] h

Tactic:
filter_upwards [h1', h2'] with ω hg1 hh1

Result:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun i => f (ns i) ω) atTop (𝓝 (g ω))
hh1 : Tendsto (fun i => (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))
⊢ g ω = h ω

Proof state:
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ g =ᶠ[ae μ] h

Tactic:
obtain ⟨ns', h2, h2'⟩ := (hh.comp h1).exists_seq_tendsto_ae'

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
⊢ g =ᶠ[ae μ] h