-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean
theorem Filter.Tendsto.compMeasurePreservingLp {α : Type*} {l : Filter α}
    {f : α → Lp E p ν} {f₀ : Lp E p ν} {g : α → C(X, Y)} {g₀ : C(X, Y)}
    (hf : Tendsto f l (𝓝 f₀)) (hg : Tendsto g l (𝓝 g₀))
    (hgm : ∀ a, MeasurePreserving (g a) μ ν) (hgm₀ : MeasurePreserving g₀ μ ν) (hp : p ≠ ∞) :
    Tendsto (fun a ↦ Lp.compMeasurePreserving (g a) (hgm a) (f a)) l
      (𝓝 (Lp.compMeasurePreserving g₀ hgm₀ f₀))

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hg : Tendsto g l (𝓝 g₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν
hgm₀ : MeasurePreserving (⇑g₀) μ ν
hp : p ≠ ⊤
this :
  Tendsto (fun gf => (Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1) (𝓝 (f₀, ⟨g₀, hgm₀⟩))
    (𝓝 ((Lp.compMeasurePreserving ⇑↑(f₀, ⟨g₀, hgm₀⟩).2 ⋯) (f₀, ⟨g₀, hgm₀⟩).1))
⊢ Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))

Tactic:
replace hg : Tendsto (fun a ↦ ⟨g a, hgm a⟩ : α → {g : C(X, Y) // MeasurePreserving g μ ν})
    l (𝓝 ⟨g₀, hgm₀⟩) :=
  tendsto_subtype_rng.2 hg

Result:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν
hgm₀ : MeasurePreserving (⇑g₀) μ ν
hp : p ≠ ⊤
this :
  Tendsto (fun gf => (Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1) (𝓝 (f₀, ⟨g₀, hgm₀⟩))
    (𝓝 ((Lp.compMeasurePreserving ⇑↑(f₀, ⟨g₀, hgm₀⟩).2 ⋯) (f₀, ⟨g₀, hgm₀⟩).1))
hg : Tendsto (fun a => ⟨g a, ⋯⟩) l (𝓝 ⟨g₀, hgm₀⟩)
⊢ Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hg : Tendsto g l (𝓝 g₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν
hgm₀ : MeasurePreserving (⇑g₀) μ ν
hp : p ≠ ⊤
⊢ Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))

Tactic:
have := (Lp.compMeasurePreserving_continuous μ ν E hp).tendsto ⟨f₀, g₀, hgm₀⟩

Result:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hg : Tendsto g l (𝓝 g₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν
hgm₀ : MeasurePreserving (⇑g₀) μ ν
hp : p ≠ ⊤
this :
  Tendsto (fun gf => (Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1) (𝓝 (f₀, ⟨g₀, hgm₀⟩))
    (𝓝 ((Lp.compMeasurePreserving ⇑↑(f₀, ⟨g₀, hgm₀⟩).2 ⋯) (f₀, ⟨g₀, hgm₀⟩).1))
⊢ Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
α : Type u_4
l : Filter α
f : α → ↥(Lp E p ν)
f₀ : ↥(Lp E p ν)
g : α → C(X, Y)
g₀ : C(X, Y)
hf : Tendsto f l (𝓝 f₀)
hgm : ∀ (a : α), MeasurePreserving (⇑(g a)) μ ν
hgm₀ : MeasurePreserving (⇑g₀) μ ν
hp : p ≠ ⊤
this :
  Tendsto (fun gf => (Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1) (𝓝 (f₀, ⟨g₀, hgm₀⟩))
    (𝓝 ((Lp.compMeasurePreserving ⇑↑(f₀, ⟨g₀, hgm₀⟩).2 ⋯) (f₀, ⟨g₀, hgm₀⟩).1))
hg : Tendsto (fun a => ⟨g a, ⋯⟩) l (𝓝 ⟨g₀, hgm₀⟩)
⊢ Tendsto (fun a => (Lp.compMeasurePreserving ⇑(g a) ⋯) (f a)) l (𝓝 ((Lp.compMeasurePreserving (⇑g₀) hgm₀) f₀))

Tactic:
convert this.comp (hf.prod_mk_nhds hg)

Result:
no goals