awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hzero : Eq (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
⊢ norm (E := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0

Tactic:
have : ‖indicatorConstLp p s_meas s_top.ne (1 : ℝ)‖ = ‖(0 : Lp ℝ p μ)‖ := by rw [hzero]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hzero : Eq (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
this : norm (E := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) = norm.{u_1} (E := ↥(Lp ℝ p μ)) 0
⊢ μ.real s ^ p.toReal⁻¹ = 0

Tactic:
simp only [norm_indicatorConstLp hp h'p.ne, norm_one, one_div, one_mul, Lp.norm_zero] at this

Premises used: MeasureTheory.norm_indicatorConstLp, MeasureTheory.Lp.norm_zero, NormOneClass.norm_one, one_div, one_mul, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hzero : Eq (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
this : μ.real s ^ p.toReal⁻¹ = 0
⊢ 0 ≤ μ.real s

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hzero : Eq (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
this : μ.real s ^ p.toReal⁻¹ = 0
⊢ p.toReal⁻¹ ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, hp, h'p.ne]

Premises used: ENNReal.toReal_eq_zero_iff, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hzero : Eq (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
this : μ.real s ^ p.toReal⁻¹ = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Real.rpow_eq_zero (by positivity) (by simp [ENNReal.toReal_eq_zero_iff, hp, h'p.ne]),
      measureReal_eq_zero_iff] at this

Premises used: Real.rpow_eq_zero, MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst_1 : Nontrivial ↥(Lp E p μ)
f : ↥(Lp E p μ)
hf : f ≠ 0
hfne : ¬(↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
h'p : p < ∞
hp : p ≠ 0
h'f : AEFinStronglyMeasurable (↑(↑f : α →ₘ[μ] E) : α → E) μ
s : Set α
s_meas : MeasurableSet s
s_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
s_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hzero : Eq (α := ↥(Lp ℝ p μ)) (indicatorConstLp (s := s) p s_meas ⋯ 1) 0
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
inr inr₁ inr₂ inr₃ : ¬False → False
inr₄ inr₅ inr₆ inr₇ inr₈ inr₉ inr₁₀ inr₁₁ : True → False
⊢ False

Tactic:
order
-- 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 ≠ ∞
⊢ p ≠ 0

Tactic:
have hp₀ : p ≠ 0 := (one_pos.trans_le Fact.out).ne'
-- 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
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (gf : ↥(Lp E p ν) × { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
    (compMeasurePreserving (⇑(↑gf.2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) gf.1

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

Premises used: Isometry.lipschitz, continuous_prod_of_dense_continuous_lipschitzWith, OfNat.ofNat, MeasureTheory.Lp.isometry_compMeasurePreserving, MeasureTheory.Lp.simpleFunc.dense, Subtype.property
-- 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
refine :
  ∀ a ∈ (↑(simpleFunc E p ν) : Set ↥(Lp E p ν)),
    Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
      (compMeasurePreserving (⇑(↑(a, y).2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (a, y).1
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (gf : ↥(Lp E p ν) × { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
    (compMeasurePreserving (⇑(↑gf.2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) gf.1

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

Premises used: continuous_prod_of_dense_continuous_lipschitzWith, OfNat.ofNat, MeasureTheory.Lp.simpleFunc.dense
-- 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 : ↥(Lp E p ν)
hf : f ∈ (↑(simpleFunc E p ν) : Set ↥(Lp E p ν))
⊢ Membership.mem (γ := AddSubgroup ↥(Lp E p ν)) (simpleFunc E p ν) f

Tactic:
hf
-- 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 : ↥(Lp E p ν)
hf : f ∈ (↑(simpleFunc E p ν) : Set ↥(Lp E p ν))
lift :
  ∀ (f : ↥(simpleFunc E p ν)),
    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
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
    (compMeasurePreserving (⇑(↑(f, y).2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f, y).1

Tactic:
lift f to Lp.simpleFunc E p ν using hf

Premises used: MeasureTheory.Lp.simpleFunc
-- 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 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 ν
h :
  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

Tactic:
ihf.add ihg

Premises used: Quotient.liftOn', Set.Mem, MeasureTheory.AEEqFun.compMeasurePreserving, MeasureTheory.AEEqFun.comp₂, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, Continuous.add, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.comp
-- 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 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 ν
h :
  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

Tactic:
exact ihf.add ihg

Premises used: Continuous.add
-- 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
c : E
s : Set Y
hs : MeasurableSet s
hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
indicatorConst :
  Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
    indicatorConstLp (s := (⇑(↑y : C(X, Y)) : (a : X) → Y) ⁻¹' s) p ⋯ ⋯ c
⊢ 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

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

Premises used: MeasureTheory.Lp.indicatorConstLp_compMeasurePreserving, MeasureTheory.Lp.simpleFunc.coe_indicatorConst
-- 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
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) μ ν }) ↦
    indicatorConstLp (s := (⇑(↑y : C(X, Y)) : (a : X) → Y) ⁻¹' s) p ⋯ ⋯ c

Tactic:
continuous_indicatorConstLp_set hp fun f ↦ ?_

Premises used: MeasureTheory.continuous_indicatorConstLp_set
-- 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
c : E
s : Set Y
hs : MeasurableSet s
hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
indicatorConst :
  ∀ (f : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }),
    Tendsto (β := ℝ≥0∞)
      (fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
        (μ : (a : Set X) → ℝ≥0∞) (((⇑(↑y : C(X, Y)) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(↑f : C(X, Y)) : (a : X) → Y) ⁻¹' s)))
      (𝓝 f) (𝓝 0)
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
    indicatorConstLp (s := (⇑(↑y : C(X, Y)) : (a : X) → Y) ⁻¹' s) p ⋯ ⋯ c

Tactic:
refine continuous_indicatorConstLp_set hp fun f ↦ ?_

Premises used: MeasureTheory.continuous_indicatorConstLp_set
-- 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
c : E
s : Set Y
hs : MeasurableSet s
hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }
apply :
  ∀ᶠ (a : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) in 𝓝 f,
    MeasurePreserving (⇑(↑a : C(X, Y)) : (a : X) → Y) μ ν
⊢ Tendsto (β := ℝ≥0∞)
    (fun (y : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
      (μ : (a : Set X) → ℝ≥0∞) (((⇑(↑y : C(X, Y)) : (a : X) → Y) ⁻¹' s) ∆ ((⇑(↑f : C(X, Y)) : (a : X) → Y) ⁻¹' s)))
    (𝓝 f) (𝓝 0)

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

Premises used: continuousAt_subtype_val, MeasurableSet.nullMeasurableSet, MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero, LT.lt.ne, Subtype.property
-- 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
c : E
s : Set Y
hs : MeasurableSet s
hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }
⊢ ∀ᶠ (a : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) in 𝓝 f,
    MeasurePreserving (⇑(↑a : C(X, Y)) : (a : X) → Y) μ ν

Tactic:
.of_forall Subtype.property

Premises used: Filter.Eventually.of_forall, Subtype.property
-- 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
c : E
s : Set Y
hs : MeasurableSet s
hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }
⊢ ∀ᶠ (a : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) in 𝓝 f,
    MeasurePreserving (⇑(↑a : C(X, Y)) : (a : X) → Y) μ ν

Tactic:
exact .of_forall Subtype.property
-- 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)
α : 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) : (a : X) → Y) μ ν
hgm₀ : MeasurePreserving (⇑g₀ : (a : X) → Y) μ ν
hp : p ≠ ∞
⊢ Tendsto (β := ↥(Lp E p μ))
    (fun (gf : ↥(Lp E p ν) × { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
      ((Lp.compMeasurePreserving (⇑(↑gf.2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) gf.1 :
        ↥(Lp E p μ)))
    (𝓝 (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀))
    (𝓝
        ((Lp.compMeasurePreserving
              (⇑(↑(f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).2 :
                    C(X, Y)) :
                (a : X) → Y)
              ⋯ :
            (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
          (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).1) :
      Filter ↥(Lp E p μ))

Tactic:
have := (Lp.compMeasurePreserving_continuous μ ν E hp).tendsto ⟨f₀, g₀, hgm₀⟩
-- 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)
α : 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) : (a : X) → Y) μ ν
hgm₀ : MeasurePreserving (⇑g₀ : (a : X) → Y) μ ν
hp : p ≠ ∞
this :
  Tendsto (β := ↥(Lp E p μ))
    (fun (gf : ↥(Lp E p ν) × { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) ↦
      ((Lp.compMeasurePreserving (⇑(↑gf.2 : C(X, Y)) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) gf.1 :
        ↥(Lp E p μ)))
    (𝓝 (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀))
    (𝓝
        ((Lp.compMeasurePreserving
              (⇑(↑(f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).2 :
                    C(X, Y)) :
                (a : X) → Y)
              ⋯ :
            (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
          (f₀, Subtype.mk (p := fun (f : C(X, Y)) ↦ MeasurePreserving (⇑f : (a : X) → Y) μ ν) g₀ hgm₀).1) :
      Filter ↥(Lp E p μ))
⊢ Tendsto (β := { g : C(X, Y) // MeasurePreserving (⇑g : (a : X) → Y) μ ν })
    (fun (a : α) ↦ Subtype.mk (p := fun (g : C(X, Y)) ↦ MeasurePreserving (⇑g : (a : X) → Y) μ ν) (g a) ⋯) l
    (𝓝 (Subtype.mk (p := fun (g : C(X, Y)) ↦ MeasurePreserving (⇑g : (a : X) → Y) μ ν) g₀ hgm₀))

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