awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp (goal)
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
⊢ False
have inr₄ : True → False
Tactic: order
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (hypothesis)
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 ≠ ∞
⊢ 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
have hp₀ : p ≠ 0
Tactic: have hp₀ : p ≠ 0 := (one_pos.trans_le Fact.out).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (goal)
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
have 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) sorry : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (a, y).1
Tactic: refine continuous_prod_of_dense_continuous_lipschitzWith _ 1
    (MeasureTheory.Lp.simpleFunc.dense hp) ?_ fun f ↦ (isometry_compMeasurePreserving f.2).lipschitz
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (goal)
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 ν))
⊢ 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
have 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) sorry : (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
      ((↑f : ↥(Lp E p ν)), y).1
Tactic: lift f to Lp.simpleFunc E p ν using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (goal)
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) μ ν }) ↦
    (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
have 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 sorry sorry c
Tactic: dsimp only [Lp.simpleFunc.coe_indicatorConst, Lp.indicatorConstLp_compMeasurePreserving]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (goal)
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
have 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)
Tactic: refine continuous_indicatorConstLp_set hp fun f ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (goal)
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) μ ν }
⊢ 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)
have apply : ∀ᶠ (a : { f : C(X, Y) // MeasurePreserving (⇑f : (a : X) → Y) μ ν }) in 𝓝 f,
  MeasurePreserving (⇑(↑a : C(X, Y)) : (a : X) → Y) μ ν
Tactic: apply tendsto_measure_symmDiff_preimage_nhds_zero continuousAt_subtype_val _ f.2
      hs.nullMeasurableSet hνs.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (goal)
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 ν)
⊢ 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
have 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) sorry :
              (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) sorry :
              (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) sorry :
            (a : ↥(Lp E p ν)) → ↥(Lp E p μ))
          ((↑(f.toLp hfp + g.toLp hgp) : ↥(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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (hypothesis)
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 (a : α) ↦
      ((Lp.compMeasurePreserving (⇑(g a) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f a) : ↥(Lp E p μ)))
    l
    (𝓝 ((Lp.compMeasurePreserving (⇑g₀ : (a : X) → Y) hgm₀ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) f₀) : Filter ↥(Lp E p μ))
have 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) sorry : (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)
            sorry :
          (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₀⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving (hypothesis)
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 (β := ↥(Lp E p μ))
    (fun (a : α) ↦
      ((Lp.compMeasurePreserving (⇑(g a) : (a : X) → Y) ⋯ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) (f a) : ↥(Lp E p μ)))
    l
    (𝓝 ((Lp.compMeasurePreserving (⇑g₀ : (a : X) → Y) hgm₀ : (a : ↥(Lp E p ν)) → ↥(Lp E p μ)) f₀) : Filter ↥(Lp E p μ))
have hg₁ : 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) sorry) 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
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
f : α →ᵇ E
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (ContinuousMap.toAEEqFun μ f.toContinuousMap)
have refine : ∀ᵐ (x : α) ∂μ, ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖
Tactic: refine Lp.mem_Lp_of_ae_bound ‖f‖ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ, ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖
have h : ∀ (x : α),
  (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x →
    ‖(↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x‖ ≤ ‖f‖
Tactic: filter_upwards [f.toContinuousMap.coeFn_toAEEqFun μ] with x _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
f : α →ᵇ E
⊢ NNNorm.nnnorm (E := ↥(Lp E p μ))
      (Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
        (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) ≤
    measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊
have hfC : ∀ᵐ (x : α) ∂μ,
  ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                  (ContinuousMap.toAEEqFun μ f.toContinuousMap) sorry) :
              α →ₘ[μ] E) :
          α → E)
        x‖₊ ≤
    ‖f‖₊
Tactic: apply Lp.nnnorm_le_of_ae_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
f : α →ᵇ E
⊢ ∀ᵐ (x : α) ∂μ,
    ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                    (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
                α →ₘ[μ] E) :
            α → E)
          x‖₊ ≤
      ‖f‖₊
have hfC : ∀ (x : α),
  (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x →
    ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                    (ContinuousMap.toAEEqFun μ f.toContinuousMap) sorry) :
                α →ₘ[μ] E) :
            α → E)
          x‖₊ ≤
      ‖f‖₊
Tactic: refine (f.toContinuousMap.coeFn_toAEEqFun μ).mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
f : α →ᵇ E
x : α
hx : (↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) : α → E) x = (f.toContinuousMap : (a : α) → E) x
⊢ ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                  (ContinuousMap.toAEEqFun μ f.toContinuousMap) ⋯) :
              α →ₘ[μ] E) :
          α → E)
        x‖₊ ≤
    ‖f‖₊
have hfC : ‖(↑(↑(Subtype.mk (p := fun (x : α →ₘ[μ] E) ↦ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) x)
                (ContinuousMap.toAEEqFun μ f.toContinuousMap) sorry) :
            α →ₘ[μ] E) :
        α → E)
      x‖ ≤
  ‖f‖
Tactic: rw [← NNReal.coe_le_coe, coe_nnnorm, coe_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
inst_5 : Fact (1 ≤ p)
⊢ Eq (α := AddSubgroup ↥(Lp E p μ)) (NormedAddGroupHom.range (V₁ := α →ᵇ E) (toLpHom p μ))
    (Lp.boundedContinuousFunction E p μ)
have symm : Eq (α := AddSubgroup ↥(Lp E p μ)) (Lp.boundedContinuousFunction E p μ)
  (NormedAddGroupHom.range (V₁ := α →ᵇ E) (toLpHom p μ))
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
⊢ Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
      ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ)) ↔
    f = g
have refine : ∀
  (h :
    Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
      ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))),
  f = g
Tactic: refine ⟨fun h => ?_, by tauto⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
h :
  Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
⊢ f = g
have rw : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
Tactic: rw [← DFunLike.coe_fn_eq, ← (map_continuous f).ae_eq_iff_eq μ (map_continuous g)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
h :
  Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (⇑f : (a : α) → E) (⇑g : (a : α) → E)
have refine : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E)
  (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
Tactic: refine (coeFn_toLp p μ 𝕜 f).symm.trans (EventuallyEq.trans ?_ <| coeFn_toLp p μ 𝕜 g)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_5 : Fact (1 ≤ p)
inst_6 : NormedRing 𝕜
inst_7 : Module 𝕜 E
inst_8 : IsBoundedSMul 𝕜 E
f g : α →ᵇ E
inst_9 : μ.IsOpenPosMeasure
h :
  Eq (α := ↥(Lp E p μ)) ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f : ↥(Lp E p μ))
    ((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g : ↥(Lp E p μ))
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) f) : α →ₘ[μ] E) : α → E)
    (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
have rw : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
  (↑(↑((toLp p μ 𝕜 : (a : α →ᵇ E) → ↥(Lp E p μ)) g) : α →ₘ[μ] E) : α → E)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : SecondCountableTopologyEither α E
inst_4 : CompactSpace α
inst_5 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_6 : Fact (1 ≤ p)
inst_7 : NormedRing 𝕜
inst_8 : Module 𝕜 E
inst_9 : IsBoundedSMul 𝕜 E
⊢ Eq (α := AddSubgroup ↥(Lp E p μ))
    (Submodule.toAddSubgroup (module_M := Lp.instModule)
      (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ))))
    (Lp.boundedContinuousFunction E p μ)
have refine : (↑(Submodule.toAddSubgroup (module_M := Lp.instModule)
        (LinearMap.range (M := C(α, E)) (↑(toLp p μ 𝕜) : C(α, E) →ₗ[𝕜] ↥(Lp E p μ)))) :
    Set ↥(Lp E p μ)) =
  (↑(Lp.boundedContinuousFunction E p μ) : Set ↥(Lp E p μ))
Tactic: refine SetLike.ext' ?_