awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (goal)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
this :
  IsLittleO.{u_1, u_2, 0} (E := E) (F := ℝ) l.smallSets (fun (s : Set X) ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b)
    fun (s : Set X) ↦ μ.real s
a : ι
ha : (fun (i : ι) ↦ μ.real (s i)) a = m a
⊢ Eq.{u_2 + 1} (α := E) (((fun (s : Set X) ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b) ∘ s) a)
    ((fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ - m i • b) a)
have dsimp : ∫ (x : X) in s a, f x ∂μ - μ.real (s a) • b = ∫ (x : X) in s a, f x ∂μ - m a • b
Tactic: dsimp only [Function.comp_apply] at ha ⊢
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (goal)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
this :
  IsLittleO.{u_1, u_2, 0} (E := E) (F := ℝ) l.smallSets (fun (s : Set X) ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b)
    fun (s : Set X) ↦ μ.real s
a : ι
ha : μ.real (s a) = m a
⊢ ∫ (x : X) in s a, f x ∂μ - μ.real (s a) • b = ∫ (x : X) in s a, f x ∂μ - m a • b
have rw : ∫ (x : X) in s a, f x ∂μ - m a • b = ∫ (x : X) in s a, f x ∂μ - m a • b
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (goal)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
⊢ IsLittleO.{u_3, u_2, 0} (E := E) li (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ - m i • b) m
have s₁ : IsLittleO.{u_1, u_2, 0} (E := E) (F := ℝ) l.smallSets (fun (s : Set X) ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b)
  fun (s : Set X) ↦ μ.real s
Tactic: suffices
      (fun s => (∫ x in s, f x ∂μ) - μ.real s • b) =o[l.smallSets] fun s => μ.real s from
    (this.comp_tendsto hs).congr'
      (hsμ.mono fun a ha => by dsimp only [Function.comp_apply] at ha ⊢; rw [ha]) hsμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (goal)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
⊢ IsLittleO.{u_1, u_2, 0} (E := E) (F := ℝ) l.smallSets (fun (s : Set X) ↦ ∫ (x : X) in s, f x ∂μ - μ.real s • b)
    fun (s : Set X) ↦ μ.real s
have refine : ∀ (ε : ℝ) (ε₀ : 0 < ε), ∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - μ.real x • b‖ ≤ ε * ‖μ.real x‖
Tactic: refine isLittleO_iff.2 fun ε ε₀ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (hypothesis)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
⊢ ∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - μ.real x • b‖ ≤ ε * ‖μ.real x‖
have this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
Tactic: have : ∀ᶠ s in l.smallSets, ∀ᵐ x ∂μ, x ∈ s → f x ∈ closedBall b ε :=
    eventually_smallSets_eventually.2 (h.eventually <| closedBall_mem_nhds _ ε₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (goal)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
⊢ ∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - μ.real x • b‖ ≤ ε * ‖μ.real x‖
have h₁ : ∀ (a : Set X),
  LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) a : ENNReal) (⊤ : ENNReal) →
    IntegrableOn f a μ →
      AEStronglyMeasurable f (μ.restrict a) →
        (∀ᵐ (x : X) ∂μ, x ∈ a → f x ∈ closedBall b ε) → ‖∫ (x : X) in a, f x ∂μ - μ.real a • b‖ ≤ ε * ‖μ.real a‖
Tactic: filter_upwards [hμ.eventually, (hμ.integrableAtFilter_of_tendsto_ae hfm h).eventually,
    hfm.eventually, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (goal)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s : ι → Set X
li : Filter ι
hs : Tendsto s li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
⊢ ∀ (a : Set X),
    LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) a : ENNReal) (⊤ : ENNReal) →
      IntegrableOn f a μ →
        AEStronglyMeasurable f (μ.restrict a) →
          (∀ᵐ (x : X) ∂μ, x ∈ a → f x ∈ closedBall b ε) → ‖∫ (x : X) in a, f x ∂μ - μ.real a • b‖ ≤ ε * ‖μ.real a‖
have h₁ : ∀ (a : Set X),
  LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) a : ENNReal) (⊤ : ENNReal) →
    IntegrableOn f a μ →
      AEStronglyMeasurable f (μ.restrict a) →
        (∀ᵐ (x : X) ∂μ, x ∈ a → ‖f x - b‖ ≤ ε) → ‖∫ (x : X) in a, f x ∂μ - μ.real a • b‖ ≤ ε * ‖μ.real a‖
Tactic: simp only [mem_closedBall, dist_eq_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (goal)
Goal:
X : Type u_1
E : Type u_2
ι : Type u_3
inst : MeasurableSpace X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
μ : Measure X
l : Filter X
inst_4 : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm_1 : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s_1 : ι → Set X
li : Filter ι
hs : Tendsto s_1 li l.smallSets
m : ι → ℝ
hsμ : (fun (i : ι) ↦ μ.real (s_1 i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : LT.lt (α := ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal) (⊤ : ENNReal)
h_integrable : IntegrableOn f s μ
hfm : AEStronglyMeasurable f (μ.restrict s)
h_norm : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε
⊢ ‖∫ (x : X) in s, f x ∂μ - μ.real s • b‖ ≤ ε * ‖μ.real s‖
have h₁ : Norm.norm.{u_2} (E := E) (∫ (a : X) in s, f a - b ∂μ) ≤ ε * μ.real s
Tactic: rw [← setIntegral_const,
    ← integral_sub h_integrable (integrableOn_const hμs.ne),
    Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
⊢ Eq (α := (s : Set α) → F →L[ℝ] F) (@weightedSMul _ _ _ _ m 0) 0
have h : ∀ (x : Set α), Eq.{u_3 + 1} (α := F →L[ℝ] F) (@weightedSMul _ _ _ _ m 0 x) (0 x)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F) (weightedSMul μ ∅) 0
have h : ∀ (x : F), Eq (α := F) ((weightedSMul μ ∅ : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
x : F
⊢ Eq (α := F) ((weightedSMul μ ∅ : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)
have h : μ.real ∅ • x = (0 : (a : F) → F) x
Tactic: rw [weightedSMul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ weightedSMul (μ + ν) s = HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul ν s)
have h : ∀ (x : F),
  Eq (α := F) ((weightedSMul (μ + ν) s : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul ν s) : (a : F) → F) x : F)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F
⊢ Eq (α := F) ((weightedSMul (μ + ν) s : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul ν s) : (a : F) → F) x : F)
have h : (weightedSMul (μ + ν) s : (a : F) → F) x =
  HAdd.hAdd (α := (a : F) → F) (β := (a : F) → F) (⇑(weightedSMul μ s) : (a : F) → F)
    (⇑(weightedSMul ν s) : (a : F) → F) x
Tactic: push_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F
⊢ (weightedSMul (μ + ν) s : (a : F) → F) x =
    HAdd.hAdd (α := (a : F) → F) (β := (a : F) → F) (⇑(weightedSMul μ s) : (a : F) → F)
      (⇑(weightedSMul ν s) : (a : F) → F) x
have h : (μ + ν).real s • x = μ.real s • x + ν.real s • x
Tactic: simp_rw [Pi.add_apply, weightedSMul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F
⊢ (μ + ν).real s • x = μ.real s • x + ν.real s • x
have h : (μ.real s + ν.real s) • x = μ.real s • x + ν.real s • x
Tactic: rw [measureReal_add_apply, add_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : F
h : (μ.real s + ν.real s) • x = μ.real s • x + ν.real s • x
⊢ (μ + ν).real s • x = μ.real s • x + ν.real s • x
have h₁ : μ.real s • x + ν.real s • x = μ.real s • x + ν.real s • x
Tactic: rw [measureReal_add_apply, add_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ weightedSMul (c • μ) s = HSMul.hSMul (β := F →L[ℝ] F) c.toReal (weightedSMul μ s)
have h : ∀ (x : F),
  Eq (α := F) ((weightedSMul (c • μ) s : (a : F) → F) x : F)
    ((HSMul.hSMul (β := F →L[ℝ] F) c.toReal (weightedSMul μ s) : (a : F) → F) x : F)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t)
have h : ∀ (x : F), Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
x : F
⊢ Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)
have h : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) • x = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) • x
Tactic: simp_rw [weightedSMul_apply, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F) (weightedSMul μ s) 0
have h : ∀ (x : F), Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s : Set α
h_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : F
⊢ Eq (α := F) ((weightedSMul μ s : (a : F) → F) x : F) ((0 : (a : F) → F) x : F)
have h : ENNReal.toReal 0 • x = (0 : (a : F) → F) x
Tactic: rw [weightedSMul_apply, measureReal_def, h_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hdisj : Disjoint s t
⊢ weightedSMul μ (s ∪ t) = HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t)
have h : ∀ (x : F),
  Eq (α := F) ((weightedSMul μ (s ∪ t) : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t) : (a : F) → F) x : F)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hdisj : Disjoint s t
x : F
⊢ Eq (α := F) ((weightedSMul μ (s ∪ t) : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t) : (a : F) → F) x : F)
have h : (weightedSMul μ (s ∪ t) : (a : F) → F) x =
  HAdd.hAdd (α := F) (β := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)
Tactic: simp_rw [add_apply, weightedSMul_apply, measureReal_union hdisj ht, add_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hdisj : Disjoint s t
x : F
h :
  (weightedSMul μ (s ∪ t) : (a : F) → F) x =
    HAdd.hAdd (α := F) (β := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)
⊢ Eq (α := F) ((weightedSMul μ (s ∪ t) : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t) : (a : F) → F) x : F)
have h₁ : μ.real (s ∪ t) • x = μ.real s • x + μ.real t • x
Tactic: simp_rw [add_apply, weightedSMul_apply, measureReal_union hdisj ht, add_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
hs_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hdisj : Disjoint s t
x : F
h :
  (weightedSMul μ (s ∪ t) : (a : F) → F) x =
    HAdd.hAdd (α := F) (β := F) ((weightedSMul μ s : (a : F) → F) x : F) ((weightedSMul μ t : (a : F) → F) x : F)
h₁ : μ.real (s ∪ t) • x = μ.real s • x + μ.real t • x
⊢ Eq (α := F) ((weightedSMul μ (s ∪ t) : (a : F) → F) x : F)
    ((HAdd.hAdd (α := F →L[ℝ] F) (weightedSMul μ s) (weightedSMul μ t) : (a : F) → F) x : F)
have h₂ : (μ.real s + μ.real t) • x = μ.real s • x + μ.real t • x
Tactic: simp_rw [add_apply, weightedSMul_apply, measureReal_union hdisj ht, add_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : SMul 𝕜 F
inst_3 : SMulCommClass ℝ 𝕜 F
c : 𝕜
s : Set α
x : F
⊢ (weightedSMul μ s : (a : F) → F) (c • x) = HSMul.hSMul (β := F) c ((weightedSMul μ s : (a : F) → F) x : F)
have simp_rw : μ.real s • c • x = c • μ.real s • x
Tactic: simp_rw [weightedSMul_apply, smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
⊢ LE.le (α := F) (0 : F) ((weightedSMul μ s : (a : F) → F) x : F)
have simp : 0 ≤ μ.real s • x
Tactic: simp only [weightedSMul, coe_smul', _root_.id, coe_id', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm f.posPart = f.posPart
have H : ∀ (a : α), Eq (α := ℝ) ((map norm f.posPart : (a : α) → ℝ) a : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ Eq (α := ℝ) ((map norm f.posPart : (a : α) → ℝ) a : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)
have H : LE.le (α := ℝ) (0 : ℝ) ((f.posPart : (a : α) → ℝ) a : ℝ)
Tactic: rw [map_apply, Real.norm_eq_abs, abs_of_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ
⊢ HSub.hSub (α := α →ₛ ℝ) (map (fun (b : ℝ) ↦ max b 0) f) (map (fun (b : ℝ) ↦ max b 0) (-f)) = f
have H : ∀ (a : α),
  Eq (α := ℝ)
    ((HSub.hSub (α := α →ₛ ℝ) (map (fun (b : ℝ) ↦ max b 0) f) (map (fun (b : ℝ) ↦ max b 0) (-f)) : (a : α) → ℝ) a : ℝ)
    ((f : (a : α) → ℝ) a : ℝ)
Tactic: ext a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ integral μ f = ∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x
have simp_rw : setToSimpleFunc (weightedSMul μ) f = ∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x
Tactic: simp_rw [integral_def, setToSimpleFunc_eq_sum_filter, weightedSMul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
simp_rw :
  setToSimpleFunc (weightedSMul μ) f =
    ∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x
⊢ integral μ f = ∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x
have simp_rw₁ : Eq (α := F) (∑ x ∈ f.range with x ≠ 0, (weightedSMul μ (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F) x)
  (∑ x ∈ f.range with x ≠ 0, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
Tactic: simp_rw [integral_def, setToSimpleFunc_eq_sum_filter, weightedSMul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
⊢ integral μ f = ∑ x ∈ s, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x
have rw : ∀ x ∈ s, x ∉ {x ∈ f.range | x ≠ 0} → μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
Tactic: rw [SimpleFunc.integral_eq_sum_filter, Finset.sum_subset hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ {x ∈ f.range | x ≠ 0}
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
have hx₁ : x ∉ f.range ∨ x = 0
Tactic: rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
have inl : ∀ (hx : 0 ∉ f.range ∨ Eq.{u_3 + 1} (α := F) 0 0),
  HSMul.hSMul (β := F) (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {0})) 0 = 0
Tactic: rcases hx.symm with (rfl | hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ x = 0
inl :
  ∀ (hx : 0 ∉ f.range ∨ Eq.{u_3 + 1} (α := F) 0 0),
    HSMul.hSMul (β := F) (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {0})) 0 = 0
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
have inr : ∀ (hx : x ∉ f.range), μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
Tactic: rcases hx.symm with (rfl | hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : DecidablePred fun (x : F) ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx_1 : x ∉ f.range ∨ x = 0
hx : x ∉ f.range
⊢ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x = 0
have hx₁ : x ∉ Set.range.{u_3, u_1 + 1} (ι := α) (⇑f : (a : α) → F)
Tactic: rw [SimpleFunc.mem_range] at hx
Cleared hypotheses: hx