-- Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
μ : Measure X
ν : Measure Y
inst_8 : μ.InnerRegularCompactLTTop
inst_9 : IsLocallyFiniteMeasure ν
E : Type u_3
inst_10 : NormedAddCommGroup E
p : ℝ≥0∞
inst_11 : Fact (1 ≤ p)
hp : p ≠ ∞
hp₀ : p ≠ 0
f : ↥(simpleFunc E p ν)
add :
  ∀ ⦃f g : SimpleFunc Y E⦄ (hfp : MemLp.{u_2, u_3} (ε := E) (⇑f : (a : Y) → E) p ν)
    (hgp : MemLp.{u_2, u_3} (ε := E) (⇑g : (a : Y) → E) p ν),
    Disjoint.{u_2} (α := Set Y) (Function.support.{u_2, u_3} (M := E) (⇑f : (a : Y) → E))
        (Function.support.{u_2, u_3} (M := E) (⇑g : (a : Y) → E)) →
      ∀
        (ihf :
          Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
            fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
            (compMeasurePreserving (⇑(↑((↑(f.toLp hfp) : ↥(Lp E p ν)), y).2 : C(X, Y)) : (a : X) → Y) ⋯ :
                (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
              ((↑(f.toLp hfp) : ↥(Lp E p ν)), y).1)
        (ihg :
          Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
            fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
            (compMeasurePreserving (⇑(↑((↑(g.toLp hgp) : ↥(Lp E p ν)), y).2 : C(X, Y)) : (a : X) → Y) ⋯ :
                (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
              ((↑(g.toLp hgp) : ↥(Lp E p ν)), y).1),
        Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
          fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
          (compMeasurePreserving (⇑(↑((↑(f.toLp hfp + g.toLp hgp) : ↥(Lp E p ν)), y).2 : C(X, Y)) : (a : X) → Y) ⋯ :
              (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
            ((↑(f.toLp hfp + g.toLp hgp) : ↥(Lp E p ν)), y).1
indicatorConst :
  ∀ (c : E) {s : Set Y} (hs : MeasurableSet s) (hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
      (compMeasurePreserving
            (⇑(↑((↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp E p ν)), y).2 : C(X, Y)) : (a : X) → Y) ⋯ :
          (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
        ((↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp E p ν)), y).1
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
    (compMeasurePreserving (⇑(↑((↑f : ↥(Lp E p ν)), y).2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
      ((↑f : ↥(Lp E p ν)), y).1

Tactic:
induction f using Lp.simpleFunc.induction hp₀ hp with
  | add hfp hgp _ ihf ihg => exact ihf.add ihg
  | @indicatorConst 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

Premises used: MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving, MeasureTheory.continuous_indicatorConstLp_set, MeasureTheory.Lp.simpleFunc.coe_indicatorConst