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
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
h₅ :
  ((↑(↑f : X →ₘ[μ] E) : X → E) + (↑(↑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) x + (↑(↑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
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯ = c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯
have h : (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) =ᶠ[ae (μ.restrict s)]
  (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) =ᶠ[ae (μ.restrict s)]
    (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F)
have h : ∀ᵐ (x : X) ∂μ.restrict s,
  (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
    (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x =
      (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x
Tactic: refine (ae_restrict_of_ae (Lp.coeFn_smul c f)).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
      (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x
have h : ∀ᵐ (x : X) ∂μ.restrict s,
  (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x →
    (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
      (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) 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
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x →
      (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
        (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x
have h : ∀ᵐ (x : X) ∂μ.restrict s,
  (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x =
      (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x →
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x →
      (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
        (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x
Tactic: refine (MemLp.coeFn_toLp ((Lp.memLp (c • f)).restrict s)).mp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : IsBoundedSMul 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x →
      (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
          (↑(↑f : X →ₘ[μ] F) : X → F) x →
        (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x →
          (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x =
            (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯) : X →ₘ[μ.restrict s] F) : X → F) x
have h : ∀ (x : X)
  (hx1 :
    (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x =
      (c • (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F)) x)
  (hx2 :
    (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x =
      (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x)
  (hx3 :
    (↑(↑(MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x = (↑(↑f : X →ₘ[μ] F) : X → F) x)
  (hx4 : (↑(↑(c • f) : X →ₘ[μ] F) : X → F) x = (c • (↑(↑f : X →ₘ[μ] F) : X → F)) x),
  (↑(↑(MemLp.toLp (↑(↑(c • f) : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x =
    (↑(↑(c • MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry) : X →ₘ[μ.restrict s] F) : X → F) x
Tactic: refine
    (Lp.coeFn_smul c (MemLp.toLp f ((Lp.memLp f).restrict s))).mono fun x hx1 hx2 hx3 hx4 => ?_
-- 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
s : Set X
f : ↥(Lp E p μ)
⊢ ‖MemLp.toLp (↑(↑f : X →ₘ[μ] E) : X → E) ⋯‖ ≤ ‖f‖
have rw : (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s)).toReal ≤ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ).toReal
Tactic: rw [Lp.norm_def, Lp.norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp _)]
-- 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
s : Set X
f : ↥(Lp E p μ)
⊢ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s)).toReal ≤ (eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ).toReal
have refine : eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p (μ.restrict s) ≤ eLpNorm (↑(↑f : X →ₘ[μ] E) : X → E) p μ
Tactic: refine ENNReal.toReal_mono (Lp.eLpNorm_ne_top _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
F : Type u_4
mX : MeasurableSpace X
inst : NormedAddCommGroup E
𝕜 : Type u_5
inst_1 : NormedRing 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : Module 𝕜 F
inst_4 : IsBoundedSMul 𝕜 F
p_1 : ℝ≥0∞
μ_1 μ : Measure X
p : ℝ≥0∞
hp : Fact (1 ≤ p)
s : Set X
f : ↥(Lp F p μ)
⊢ norm (E := ↥(Lp F p (μ.restrict s)))
      (({ toFun := fun (f : ↥(Lp F p μ)) ↦ MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) ⋯, map_add' := ⋯, map_smul' := ⋯ :
              ↥(Lp F p μ) →ₗ[𝕜] ↥(Lp F p (μ.restrict s)) } :
            (a : ↥(Lp F p μ)) → ↥(Lp F p (μ.restrict s)))
          f :
        ↥(Lp F p (μ.restrict s))) ≤
    1 * ‖f‖
have rw : norm (E := ↥(Lp F p (μ.restrict s)))
    (({ toFun := fun (f : ↥(Lp F p μ)) ↦ MemLp.toLp (↑(↑f : X →ₘ[μ] F) : X → F) sorry, map_add' := sorry, map_smul' := sorry :
            ↥(Lp F p μ) →ₗ[𝕜] ↥(Lp F p (μ.restrict s)) } :
          (a : ↥(Lp F p μ)) → ↥(Lp F p (μ.restrict s)))
        f :
      ↥(Lp F p (μ.restrict s))) ≤
  ‖f‖
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ
have this : Fact (LE.le (α := ℝ≥0∞) 1 1)
Tactic: haveI : Fact ((1 : ℝ≥0∞) ≤ 1) := ⟨le_rfl⟩
-- 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
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
⊢ Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
have h : ∀ (f : ↥(Lp E 1 μ)),
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    ((integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
        (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
          X → E))
      f)
Tactic: ext1 f
-- 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
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
f : ↥(Lp E 1 μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    ((integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
        (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
          X → E))
      f)
have h : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
  (integral (μ.restrict s)
    (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
      X → E))
Tactic: rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]
-- 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
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
f : ↥(Lp E 1 μ)
h :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s)
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    ((integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
        (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
          X → E))
      f)
have h₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
  (∫ (a : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) a ∂μ)
Tactic: rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ
have h_comp : Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
  (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
    (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
      X → E))
Tactic: have h_comp :
    (fun f : X →₁[μ] E => ∫ x in s, f x ∂μ) =
      integral (μ.restrict s) ∘ fun f => LpToLpRestrictCLM X E ℝ μ 1 s f := by
    ext1 f
    rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]
-- 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
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
h_comp :
  Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ
have rw : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
    (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
      X → E))
Tactic: rw [h_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in support F, F x ∂ν) (∫ (x : X), F x ∂ν)
have nth_rw : Eq.{u_5 + 1} (α := M) (∫ (x : X) in support F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)
Tactic: nth_rw 2 [← setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in support F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)
have rw : ∀ x ∈ univ \ support F, F x = 0
Tactic: rw [setIntegral_eq_of_subset_of_forall_diff_eq_zero MeasurableSet.univ (subset_univ (support F))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst_2 : TopologicalSpace X
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in tsupport F, F x ∂ν) (∫ (x : X), F x ∂ν)
have nth_rw : Eq.{u_5 + 1} (α := M) (∫ (x : X) in tsupport F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)
Tactic: nth_rw 2 [← setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst_2 : TopologicalSpace X
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in tsupport F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)
have rw : ∀ x ∈ univ \ tsupport F, F x = 0
Tactic: rw [setIntegral_eq_of_subset_of_forall_diff_eq_zero MeasurableSet.univ (subset_univ (tsupport F))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ (μ : (a : Set X) → ℝ≥0∞) E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ
have h : (μ : (a : Set X) → ℝ≥0∞) E = lintegral μ (E.indicator fun (x : X) ↦ 1)
Tactic: convert_to lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
h : (μ : (a : Set X) → ℝ≥0∞) E = lintegral μ (E.indicator fun (x : X) ↦ 1)
⊢ (μ : (a : Set X) → ℝ≥0∞) E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ
have convert_to : lintegral μ (E.indicator fun (x : X) ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)
Tactic: convert_to lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ (μ : (a : Set X) → ℝ≥0∞) E = lintegral μ (E.indicator fun (x : X) ↦ 1)
have h : (μ : (a : Set X) → ℝ≥0∞) E = ∫⁻ (a : X) in E, 1 ∂μ
Tactic: rw [lintegral_indicator E_mble]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun (x : X) ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)
have hfg : (E.indicator fun (x : X) ↦ 1) ≤ thickenedIndicatorAux δ E
Tactic: apply lintegral_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
⊢ (μ : (a : Set X) → ℝ≥0∞) E ≤
    ∫⁻ (x : X), (↑(((thickenedIndicator δ_pos E : BoundedContinuousFunction X ℝ≥0) : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have h : ∀ (x : X),
  (↑(((thickenedIndicator δ_pos E : BoundedContinuousFunction X ℝ≥0) : (a : X) → ℝ≥0) x) : ℝ≥0∞) =
    thickenedIndicatorAux δ E x
Tactic: convert! measure_le_lintegral_thickenedIndicatorAux μ E_mble δ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
g₁ g₂ : SimpleFunc X ℝ
h : Disjoint (α := Set X) (support (M := ℝ) (⇑g₁ : (a : X) → ℝ)) (support (M := ℝ) (⇑g₂ : (a : X) → ℝ))
h_int₁ : Integrable ((⇑g₁ : (a : X) → ℝ) * f) μ
h_int₂ : Integrable ((⇑g₂ : (a : X) → ℝ) * f) μ
⊢ (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ] (⇑(g₁ + g₂) : (a : X) → ℝ) * f
have rw : (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ]
  HAdd.hAdd (α := (a : X) → ℝ) (⇑g₁ : (a : X) → ℝ) (⇑g₂ : (a : X) → ℝ) * f
Tactic: rw [SimpleFunc.coe_add, add_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
g₁ g₂ : SimpleFunc X ℝ
h : Disjoint (α := Set X) (support (M := ℝ) (⇑g₁ : (a : X) → ℝ)) (support (M := ℝ) (⇑g₂ : (a : X) → ℝ))
h_int₁ : Integrable ((⇑g₁ : (a : X) → ℝ) * f) μ
h_int₂ : Integrable ((⇑g₂ : (a : X) → ℝ) * f) μ
rw :
  (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ]
    HAdd.hAdd (α := (a : X) → ℝ) (⇑g₁ : (a : X) → ℝ) (⇑g₂ : (a : X) → ℝ) * f
⊢ (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ] (⇑(g₁ + g₂) : (a : X) → ℝ) * f
have rw₁ : (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ] (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f
Tactic: rw [SimpleFunc.coe_add, add_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable ((⇑g : (a : X) → ℝ) * f) μ
have c : ∀ (c : ℝ) (s : Set X) (hs : MeasurableSet s),
  Integrable ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) : (a : X) → ℝ) * f) μ
Tactic: refine
    SimpleFunc.induction (fun c s hs => ?_)
      (fun g₁ g₂ _ h_int₁ h_int₂ =>
        (h_int₁.add h_int₂).congr (by rw [SimpleFunc.coe_add, add_mul]))
      g
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ Integrable ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) : (a : X) → ℝ) * f) μ
have simp : Integrable (s.indicator (const X c) * f) μ
Tactic: simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
    SimpleFunc.coe_zero, Set.piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ s.indicator (const X c) * f = s.indicator (c • f)
have h : ∀ (x : X), (s.indicator (const X c) * f) x = s.indicator (c • f) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x
have pos : ∀ (hx : x ∈ s), (s.indicator (const X c) * f) x = s.indicator (c • f) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
pos : ∀ (hx : x ∈ s), (s.indicator (const X c) * f) x = s.indicator (c • f) x
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x
have neg : ∀ (hx : x ∉ s), (s.indicator (const X c) * f) x = s.indicator (c • f) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ Integrable (s.indicator (const X c) * f) μ
have this : s.indicator (const X c) * f = s.indicator (c • f)
Tactic: have : Set.indicator s (Function.const X c) * f = s.indicator (c • f) := by
    ext1 x
    by_cases hx : x ∈ s
    · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, smul_eq_mul,
        ← Function.const_def]
    · simp only [hx, Pi.mul_apply, Set.indicator_of_notMem, not_false_iff, zero_mul]