awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have rw : ∫⁻ (a : α) in s, (↑‖g a‖₊ : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
Tactic: rw [lintegral_congr_ae hg_nnnorm_eq.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ ∫⁻ (a : α) in s, (↑‖g a‖₊ : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have refine_1 : IntegrableOn (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) s μ
Tactic: refine lintegral_enorm_le_of_forall_fin_meas_integral_eq
    hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
refine_1 : IntegrableOn (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) s μ
refine_2 : StronglyMeasurable g
⊢ ∫⁻ (a : α) in s, (↑‖g a‖₊ : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have refine_3 : IntegrableOn g s μ
Tactic: refine lintegral_enorm_le_of_forall_fin_meas_integral_eq
    hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
refine_1 : IntegrableOn (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) s μ
refine_2 : StronglyMeasurable g
refine_3 : IntegrableOn g s μ
⊢ ∫⁻ (a : α) in s, (↑‖g a‖₊ : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have refine_4 : ∀ (t : Set α),
  MeasurableSet t →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)
Tactic: refine lintegral_enorm_le_of_forall_fin_meas_integral_eq
    hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ IntegrableOn g s μ
have refine_3 : Integrable (ε := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
  (μ.restrict s)
Tactic: rw [IntegrableOn, integrable_congr hg_eq_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)
have refine_4 : Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ)
  (∫ (x : α) in t,
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)
Tactic: rw [← integral_condExpL2_eq_of_fin_meas_real (hm := hm) f ht hμt.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ =
    0
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0
have rw : ∀
  (h_nnnorm_eq_zero :
    (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
      (fun (x : α) ↦
        (↑(nnnorm (E := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
                  α → ℝ)
                x)) :
          ℝ≥0∞))
      0),
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0
Tactic: rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero
Cleared hypotheses: h_nnnorm_eq_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ =
    0
rw :
  ∀
    (h_nnnorm_eq_zero :
      (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
        (fun (x : α) ↦
          (↑(nnnorm (E := ℝ)
                ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
                    α → ℝ)
                  x)) :
            ℝ≥0∞))
        0),
    (ae (μ.restrict s)).EventuallyEq (β := ℝ)
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0
have rw₁ : Measurable (β := ℝ≥0∞) fun (x : α) ↦
  (↑(nnnorm (E := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
          x)) :
    ℝ≥0∞)
Tactic: rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞))
    0
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0
have refine : ∀ (x : α)
  (hx :
    Eq (α := ℝ≥0∞)
      ((fun (x : α) ↦
          (↑(nnnorm (E := ℝ)
                ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
                    α → ℝ)
                  x)) :
            ℝ≥0∞))
        x)
      (0 x)),
  Eq (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x)
    (0 x)
Tactic: refine h_nnnorm_eq_zero.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞))
    0
x : α
hx :
  (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) =
    0 x
⊢ Eq (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x)
    (0 x)
have hx₁ : (↑(nnnorm (E := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
          x)) :
    ℝ≥0∞) =
  0
Tactic: rw [Pi.zero_apply] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞))
    0
x : α
hx :
  (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) =
    0
⊢ Eq (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0
have rwa : ∀
  (hx :
    nnnorm (E := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
          x) =
      0),
  Eq (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0
Tactic: rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞))
    0
x : α
hx :
  (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) =
    0
rwa :
  ∀
    (hx :
      nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x) =
        0),
    Eq (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0
⊢ Eq (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0
have rwa₁ : ∀
  (hx :
    Eq (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x)
      0),
  Eq (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0
Tactic: rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ =
    0
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
have refine : Measurable.{u_1, 0} (α := α) (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
Tactic: refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0
have suffices : ∫⁻ (x : α) in s,
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) ∂μ =
  0
Tactic: suffices h_nnnorm_eq_zero : ∫⁻ x in s, ‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ ∂μ = 0 by
    rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero
    · refine h_nnnorm_eq_zero.mono fun x hx => ?_
      dsimp only at hx
      rw [Pi.zero_apply] at hx ⊢
      · rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
    · refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)
      exact (Lp.stronglyMeasurable _).measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ =
    0
have rw : ∫⁻ (x : α) in s,
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) ∂μ ≤
  0
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    0
have refine : ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ = 0
Tactic: refine (lintegral_nnnorm_condExpL2_le hs hμs f).trans (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
⊢ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ = 0
have rw : (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) 0
Tactic: rw [lintegral_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
rw : (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) 0
⊢ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ = 0
have rw₁ : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)
Tactic: rw [lintegral_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) 0
have refine : ∀ (x : α) (hx : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x = 0 x),
  Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) x) (0 x)
Tactic: refine hf.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x = 0 x
⊢ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) = 0 x
have rw : (↑(nnnorm (E := ℝ) (0 x)) : ℝ≥0∞) = 0 x
Tactic: rw [hx]