awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u v : X → E
huv : u =ᶠ[ae (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))] v
h_1 : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
hu : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h : ∀ (x : X) (hx : (↑(f x) : ℝ≥0∞) ≠ 0 → u x = v x), f x • u x = f x • v x
⊢ Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f a • u a) fun (a : X) ↦ f a • v a

Tactic:
filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 huv] with x hx

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.ae_withDensity_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u v : X → E
huv : u =ᶠ[ae (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))] v
h_1 : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
hu : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
x : X
hx : (↑(f x) : ℝ≥0∞) ≠ 0 → u x = v x
h : ∀ (h'x : f x = 0), f x • u x = f x • v x
h₁ : ∀ (h'x : f x ≠ 0), f x • u x = f x • v x
⊢ f x • u x = f x • v x

Tactic:
rcases eq_or_ne (f x) 0 with (h'x | h'x)

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u v : X → E
huv : u =ᶠ[ae (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))] v
h : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
hu : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
x : X
hx : (↑(f x) : ℝ≥0∞) ≠ 0 → u x = v x
h'x : f x = 0
⊢ f x • u x = f x • v x

Tactic:
simp only [h'x, zero_smul]

Premises used: zero_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u v : X → E
huv : u =ᶠ[ae (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))] v
h : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
hu : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
x : X
hx : (↑(f x) : ℝ≥0∞) ≠ 0 → u x = v x
h'x : f x ≠ 0
rw : (↑(f x) : ℝ≥0∞) ≠ 0
⊢ f x • u x = f x • v x

Tactic:
rw [hx _]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u v : X → E
huv : u =ᶠ[ae (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))] v
h : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
hu : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
x : X
hx : (↑(f x) : ℝ≥0∞) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ (↑(f x) : ℝ≥0∞) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using h'x

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
e_μ : (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) = μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
e_μ : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)
⊢ (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) = μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)

Tactic:
apply withDensity_congr_ae

Premises used: MeasureTheory.withDensity_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
h : ∀ (x : X) (hx : f x = AEMeasurable.mk f hf x), (↑(f x) : ℝ≥0∞) = (↑(f' x) : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
x : X
hx : f x = AEMeasurable.mk f hf x
h h₁ : (↑(AEMeasurable.mk f hf x) : ℝ≥0∞) = (↑(f' x) : ℝ≥0∞)
⊢ (↑(f x) : ℝ≥0∞) = (↑(f' x) : ℝ≥0∞)

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)) (∫ (x : X), f' x • g x ∂μ)

Tactic:
integral_withDensity_eq_integral_smul hf.measurable_mk _

Premises used: integral_withDensity_eq_integral_smul, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
h : Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f' a • g a) fun (a : X) ↦ f a • g a
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f' x • g x ∂μ) (∫ (x : X), f x • g x ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
h : ∀ (x : X) (hx : f x = AEMeasurable.mk f hf x), f' x • g x = f x • g x
⊢ Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f' a • g a) fun (a : X) ↦ f a • g a

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
x : X
hx : f x = AEMeasurable.mk f hf x
h h₁ : f' x • g x = AEMeasurable.mk f hf x • g x
⊢ f' x • g x = f x • g x

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
hf : AEMeasurable f μ
g : X → E
f' : X → ℝ≥0 := AEMeasurable.mk f hf
g₁ :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞))
g₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f' x • g x ∂μ) (∫ (x : X), f x • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)

Tactic:
calc
    ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, g x ∂μ.withDensity fun x => f' x := by
      congr 1
      apply withDensity_congr_ae
      filter_upwards [hf.ae_eq_mk] with x hx
      rw [hx]
    _ = ∫ x, f' x • g x ∂μ := integral_withDensity_eq_integral_smul hf.measurable_mk _
    _ = ∫ x, f x • g x ∂μ := by
      apply integral_congr_ae
      filter_upwards [hf.ae_eq_mk] with x hx
      rw [hx]

Premises used: MeasureTheory.Measure.withDensity, ENNReal.ofNNReal, integral_withDensity_eq_integral_smul, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0∞
f_meas : AEMeasurable f μ
hf_lt_top : ∀ᵐ (x : X) ∂μ, f x < ∞
g : X → E
dsimp : Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toNNReal • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toReal • g x ∂μ)

Tactic:
dsimp only [ENNReal.toReal, ← NNReal.smul_def]

Premises used: NNReal.smul_def, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0∞
f_meas : AEMeasurable f μ
hf_lt_top : ∀ᵐ (x : X) ∂μ, f x < ∞
g : X → E
rw :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f)
    (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x).toNNReal : ℝ≥0∞))
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), g x ∂μ.withDensity f)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toNNReal • g x ∂μ)

Tactic:
rw [← integral_withDensity_eq_integral_smul₀ f_meas.ennreal_toNNReal,
    withDensity_congr_ae (coe_toNNReal_ae_eq hf_lt_top)]

Premises used: AEMeasurable.ennreal_toNNReal, MeasureTheory.coe_toNNReal_ae_eq, MeasureTheory.withDensity_congr_ae, integral_withDensity_eq_integral_smul₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0∞
f_meas : Measurable f
hf_lt_top : ∀ᵐ (x : X) ∂μ, f x < ∞
g : X → E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toReal • g x ∂μ)

Tactic:
integral_withDensity_eq_integral_toReal_smul₀ f_meas.aemeasurable hf_lt_top g

Premises used: Measurable.aemeasurable, integral_withDensity_eq_integral_toReal_smul₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
s : Set X
hf : AEMeasurable f (μ.restrict s)
g : X → E
hs : MeasurableSet s
rw :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂(μ.restrict s).withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X) in s, f x • g x ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x • g x ∂μ) (∫ (x : X) in s, f x • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X) in s, f x • g x ∂μ)

Tactic:
rw [restrict_withDensity hs, integral_withDensity_eq_integral_smul₀ hf]

Premises used: MeasureTheory.restrict_withDensity, integral_withDensity_eq_integral_smul₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0∞
s : Set X
hf : AEMeasurable f (μ.restrict s)
hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ∞
g : X → E
hs : MeasurableSet s
rw :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂(μ.restrict s).withDensity fun (x : X) ↦ f x)
    (∫ (x : X) in s, (f x).toReal • g x ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (f x).toReal • g x ∂μ) (∫ (x : X) in s, (f x).toReal • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) ↦ f x) (∫ (x : X) in s, (f x).toReal • g x ∂μ)

Tactic:
rw [restrict_withDensity hs, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]

Premises used: MeasureTheory.restrict_withDensity, integral_withDensity_eq_integral_toReal_smul₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
s : Set X
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X) in s, f x • g x ∂μ)

Tactic:
setIntegral_withDensity_eq_setIntegral_smul₀ f_meas.aemeasurable _ hs

Premises used: setIntegral_withDensity_eq_setIntegral_smul₀, Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : X → ℝ≥0∞
s : Set X
hf : Measurable f
hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ∞
g : X → E
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) ↦ f x) (∫ (x : X) in s, (f x).toReal • g x ∂μ)

Tactic:
setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hf.aemeasurable hf_top g hs

Premises used: Measurable.aemeasurable, setIntegral_withDensity_eq_setIntegral_toReal_smul₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
f : X → ℝ≥0
s : Set X
hf : AEMeasurable f (μ.restrict s)
g : X → E
rw :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂(μ.restrict s).withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X) in s, f x • g x ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x • g x ∂μ) (∫ (x : X) in s, f x • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X) in s, f x • g x ∂μ)

Tactic:
rw [restrict_withDensity' s, integral_withDensity_eq_integral_smul₀ hf]

Premises used: integral_withDensity_eq_integral_smul₀, MeasureTheory.restrict_withDensity'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
f : X → ℝ≥0∞
s : Set X
hf : AEMeasurable f (μ.restrict s)
hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ∞
g : X → E
rw : Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂(μ.restrict s).withDensity f) (∫ (x : X) in s, (f x).toReal • g x ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (f x).toReal • g x ∂μ) (∫ (x : X) in s, (f x).toReal • g x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity f) (∫ (x : X) in s, (f x).toReal • g x ∂μ)

Tactic:
rw [restrict_withDensity' s, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]

Premises used: integral_withDensity_eq_integral_toReal_smul₀, MeasureTheory.restrict_withDensity'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
Goal:
X : Type u_1
E : Type u_3
inst : MeasurableSpace X
μ : Measure X
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : SFinite μ
f : X → ℝ≥0∞
s : Set X
hf : Measurable f
hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ∞
g : X → E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity f) (∫ (x : X) in s, (f x).toReal • g x ∂μ)

Tactic:
setIntegral_withDensity_eq_setIntegral_toReal_smul₀' s hf.aemeasurable hf_top g

Premises used: Measurable.aemeasurable, setIntegral_withDensity_eq_setIntegral_toReal_smul₀'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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
dsimp : ∫ (x : X) in s a, f x ∂μ - μ.real (s a) • b = ∫ (x : X) in s a, f x ∂μ - m a • b
⊢ 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)

Tactic:
dsimp only [Function.comp_apply] at ha ⊢

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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
rw rw₁ : ∫ (x : X) in s a, f x ∂μ - m a • b = ∫ (x : X) in s a, f x ∂μ - m a • b
⊢ ∫ (x : X) in s a, f x ∂μ - μ.real (s a) • b = ∫ (x : X) in s a, f x ∂μ - m a • b

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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
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
⊢ IsLittleO.{u_3, u_2, 0} (E := E) li (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ - m i • b) m

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μ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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

Tactic:
isLittleO_iff.2 fun ε ε₀ => ?_

Premises used: Iff.mpr, Asymptotics.isLittleO_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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
refine : ∀ (ε : ℝ) (ε₀ : 0 < ε), ∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - μ.real x • b‖ ≤ ε * ‖μ.real x‖
⊢ 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:
refine isLittleO_iff.2 fun ε ε₀ => ?_

Premises used: Iff.mpr, Asymptotics.isLittleO_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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 < ε
⊢ ∀ᶠ (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 _ ε₀)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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 ε
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‖
⊢ ∀ᶠ (x : Set X) in l.smallSets, ‖∫ (x : X) in x, f x ∂μ - μ.real x • b‖ ≤ ε * ‖μ.real x‖

Tactic:
filter_upwards [hμ.eventually, (hμ.integrableAtFilter_of_tendsto_ae hfm h).eventually,
    hfm.eventually, this]

Premises used: MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter_of_tendsto_ae, StronglyMeasurableAtFilter.eventually, MeasureTheory.Measure.FiniteAtFilter.eventually, MeasureTheory.IntegrableAtFilter.eventually
-- Module: Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
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 ε
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‖
⊢ ∀ (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:
simp only [mem_closedBall, dist_eq_norm]

Premises used: dist_eq_norm, Metric.mem_closedBall