-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean
theorem compMeasurePreserving_continuous (hp : p ≠ ∞) :
    Continuous fun gf : Lp E p ν × {f : C(X, Y) // MeasurePreserving f μ ν} ↦
      compMeasurePreserving gf.2.1 gf.2.2 gf.1

Proof state:
case intro.h_ind
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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ⊤
f : { f // MeasurePreserving (⇑f) μ ν }
⊢ Tendsto (fun y => μ ((⇑↑y ⁻¹' s) ∆ (⇑↑f ⁻¹' s))) (𝓝 f) (𝓝 0)

Tactic:
apply tendsto_measure_symmDiff_preimage_nhds_zero continuousAt_subtype_val _ f.2
  hs.nullMeasurableSet hνs.ne

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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ⊤
f : { f // MeasurePreserving (⇑f) μ ν }
⊢ ∀ᶠ (a : { f // MeasurePreserving (⇑f) μ ν }) in 𝓝 f, MeasurePreserving (⇑↑a) μ ν

Proof state:
case intro.h_ind
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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ⊤
⊢ Continuous fun y => indicatorConstLp p ⋯ ⋯ c

Tactic:
refine continuous_indicatorConstLp_set hp fun f ↦ ?_

Result:
case intro.h_ind
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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ⊤
f : { f // MeasurePreserving (⇑f) μ ν }
⊢ Tendsto (fun y => μ ((⇑↑y ⁻¹' s) ∆ (⇑↑f ⁻¹' s))) (𝓝 f) (𝓝 0)

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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
⊢ Continuous fun gf => (compMeasurePreserving ⇑↑gf.2 ⋯) gf.1

Tactic:
refine continuous_prod_of_dense_continuous_lipschitzWith _ 1
  (MeasureTheory.Lp.simpleFunc.dense hp) ?_ fun f ↦ (isometry_compMeasurePreserving f.2).lipschitz

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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
⊢ ∀ a ∈ ↑(simpleFunc E p ν), Continuous fun y => (compMeasurePreserving ⇑↑(a, y).2 ⋯) (a, y).1

Proof state:
case intro
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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
f : ↥(simpleFunc E p ν)
⊢ Continuous fun y => (compMeasurePreserving ⇑↑(↑f, y).2 ⋯) (↑f, y).1

Tactic:
induction f using Lp.simpleFunc.induction hp₀ hp with
| h_add hfp hgp _ ihf ihg => exact ihf.add ihg
| @h_ind c s hs hνs =>
  dsimp only [Lp.simpleFunc.coe_indicatorConst, Lp.indicatorConstLp_compMeasurePreserving]
  refine continuous_indicatorConstLp_set hp fun f ↦ ?_
  apply tendsto_measure_symmDiff_preimage_nhds_zero continuousAt_subtype_val _ f.2
    hs.nullMeasurableSet hνs.ne
  exact .of_forall Subtype.property

Result:
no goals

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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ⊤
f : { f // MeasurePreserving (⇑f) μ ν }
⊢ ∀ᶠ (a : { f // MeasurePreserving (⇑f) μ ν }) in 𝓝 f, MeasurePreserving (⇑↑a) μ ν

Tactic:
exact .of_forall Subtype.property

Result:
no goals

Proof state:
case intro.h_add
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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
f✝ g✝ : SimpleFunc Y E
hfp : MemLp (⇑f✝) p ν
hgp : MemLp (⇑g✝) p ν
a✝ : Disjoint (Function.support ⇑f✝) (Function.support ⇑g✝)
ihf : Continuous fun y => (compMeasurePreserving ⇑↑(↑(simpleFunc.toLp f✝ hfp), y).2 ⋯) (↑(simpleFunc.toLp f✝ hfp), y).1
ihg : Continuous fun y => (compMeasurePreserving ⇑↑(↑(simpleFunc.toLp g✝ hgp), y).2 ⋯) (↑(simpleFunc.toLp g✝ hgp), y).1
⊢ Continuous fun y =>
    (compMeasurePreserving ⇑↑(↑(simpleFunc.toLp f✝ hfp + simpleFunc.toLp g✝ hgp), y).2 ⋯)
      (↑(simpleFunc.toLp f✝ hfp + simpleFunc.toLp g✝ hgp), y).1

Tactic:
exact ihf.add ihg

Result:
no goals

Proof state:
case intro.h_ind
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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ⊤
⊢ Continuous fun y =>
    (compMeasurePreserving ⇑↑(↑(simpleFunc.indicatorConst p hs ⋯ c), y).2 ⋯)
      (↑(simpleFunc.indicatorConst p hs ⋯ c), y).1

Tactic:
dsimp only [Lp.simpleFunc.coe_indicatorConst, Lp.indicatorConstLp_compMeasurePreserving]

Result:
case intro.h_ind
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)
hp : p ≠ ⊤
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ⊤
⊢ Continuous fun y => indicatorConstLp p ⋯ ⋯ c