awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst : Countable ι
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : TopologicalSpace X
inst_3 : BorelSpace X
inst_4 : T2Space X
inst_5 : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
i : ι
⊢ ∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ ≤
    ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
have rw : norm (E := ℝ) (∫ (x : X) in (↑(s i) : Set X), norm.{u_3} (E := E) ((f : (a : X) → E) x : E) ∂μ) ≤
  ‖ContinuousMap.restrict (↑(s i) : Set X) f‖ * μ.real (↑(s i) : Set X)
Tactic: rw [← (Real.norm_of_nonneg (integral_nonneg fun x => norm_nonneg _) : ‖_‖ = ∫ x in s i, ‖f x‖ ∂μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯ =
    MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯
have h : (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) =ᶠ[ae (μ.restrict s)]
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) :
    X → E)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) =ᶠ[ae (μ.restrict s)]
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
      X → E)
have h : ∀ᵐ (x : X) ∂μ.restrict s,
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
    (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x =
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) :
              X →ₘ[μ.restrict s] E) :
          X → E)
        x
Tactic: refine (ae_restrict_of_ae (Lp.coeFn_add f g)).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
      (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                X →ₘ[μ.restrict s] E) :
            X → E)
          x
have h : ∀ᵐ (x : X) ∂μ.restrict s,
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) :
          X → E)
        x =
      ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) +
          (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E))
        x →
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
      (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x =
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) :
                X →ₘ[μ.restrict s] E) :
            X → E)
          x
Tactic: refine
    (Lp.coeFn_add (MemLp.toLp f ((Lp.memLp f).restrict s))
          (MemLp.toLp g ((Lp.memLp g).restrict s))).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
            X → E)
          x =
        ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
            (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
          x →
      (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
        (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x
have h : ∀ᵐ (x : X) ∂μ.restrict s,
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x →
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) :
            X → E)
          x =
        ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) +
            (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E))
          x →
      (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
        (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x
Tactic: refine (MemLp.coeFn_toLp ((Lp.memLp f).restrict s)).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x =
          ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
              (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
            x →
        (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
          (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
            (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x
have h : ∀ᵐ (x : X) ∂μ.restrict s,
  (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x →
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) :
                  X →ₘ[μ.restrict s] E) :
              X → E)
            x =
          ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) +
              (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E))
            x →
        (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
          (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x =
            (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x
Tactic: refine (MemLp.coeFn_toLp ((Lp.memLp g).restrict s)).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
          (↑(↑f : X →ₘ[μ] E) : X → E) x →
        (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                    X →ₘ[μ.restrict s] E) :
                X → E)
              x =
            ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
                (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
              x →
          (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x →
            (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
              (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) :
                      X →ₘ[μ.restrict s] E) :
                  X → E)
                x
have h : ∀ (x : X)
  (hx1 :
    (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x =
      (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x)
  (hx2 :
    (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x)
  (hx3 :
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x)
  (hx4 :
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) :
          X → E)
        x =
      ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) +
          (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E))
        x)
  (hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x),
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) :
        X → E)
      x
Tactic: refine (MemLp.coeFn_toLp ((Lp.memLp (f + g)).restrict s)).mono fun x hx1 hx2 hx3 hx4 hx5 => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x
hx2 : (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x
hx4 :
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x
have h : (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x =
  ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) +
      (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E))
    x
Tactic: rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x
hx2 : (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x
hx4 :
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x
h :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x
have h₁ : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
  ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) +
      (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E))
    x
Tactic: rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x
hx2 : (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x
hx4 :
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x
h :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
h₁ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x
have h₂ : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x +
    (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x
Tactic: rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x
hx2 : (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x
hx4 :
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x
h :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
h₁ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
h₂ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x +
      (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x
have h₃ : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) sorry) : X →ₘ[μ.restrict s] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
Tactic: rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x
hx2 : (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x
hx4 :
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x
h :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
h₁ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
h₂ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x +
      (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x
h₃ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x
have h₄ : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
Tactic: rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x
hx2 : (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑g : X →ₘ[μ] E) : X → E) x
hx3 : (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x
hx4 :
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
hx5 : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x
h :
  (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
h₁ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    ((↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) +
        (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E))
      x
h₂ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x +
      (↑(↑(MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x
h₃ :
  (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
h₄ : (↑(↑(f + g) : X →ₘ[μ] E) : X → E) x = (↑(↑f : X →ₘ[μ] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
⊢ (↑(↑(MemLp.toLp (↑(↑(f + g) : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) : X → E) x =
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯ + MemLp.toLp (↑(↑g : X →ₘ[μ] E) : X → E) ⋯) : X →ₘ[μ.restrict s] E) :
        X → E)
      x
have h₅ : ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑g : X →ₘ[μ] E) : X → E)) x =
  (↑(↑f : X →ₘ[μ] E) : X → E) x + (↑(↑g : X →ₘ[μ] E) : X → E) x
Tactic: rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]