awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (hypothesis)
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∞))
⊢ IsClosed (X := ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))))
    {f_1 : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))) |
      (fun (g : X → E) ↦
          Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ))
        (↑(↑f_1 : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E)}
have C1 : Continuous (Y := E) fun (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) ↦
  ∫ (x : X),
    (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E) x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)
Tactic: have C1 :
      Continuous fun u : Lp E 1 (μ.withDensity fun x => f x) =>
        ∫ x, u x ∂μ.withDensity fun x => f x :=
      continuous_integral
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (hypothesis)
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∞))
C1 :
  Continuous (Y := E) fun (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) ↦
    ∫ (x : X),
      (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E)
        x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)
⊢ Continuous (Y := E) fun (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) ↦
    ∫ (x : X), f x • (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E) x ∂μ
have this : Continuous (X := ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) (Y := E)
  ((fun (u : ↥(Lp E 1 μ)) ↦ ∫ (x : X), (↑(↑u : X →ₘ[μ] E) : X → E) x ∂μ) ∘
    (⇑(withDensitySMulLI μ f_meas) : (a : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) → ↥(Lp E 1 μ)))
Tactic: have : Continuous ((fun u : Lp E 1 μ => ∫ x, u x ∂μ) ∘ withDensitySMulLI (E := E) μ f_meas) :=
        continuous_integral.comp (withDensitySMulLI (E := E) μ f_meas).continuous
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞))
C1 :
  Continuous (Y := E) fun (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) ↦
    ∫ (x : X),
      (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E)
        x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)
this :
  Continuous (X := ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) (Y := E)
    ((fun (u : ↥(Lp E 1 μ)) ↦ ∫ (x : X), (↑(↑u : X →ₘ[μ] E) : X → E) x ∂μ) ∘
      (⇑(withDensitySMulLI μ f_meas) : (a : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) → ↥(Lp E 1 μ)))
⊢ Continuous (Y := E) fun (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) ↦
    ∫ (x : X), f x • (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E) x ∂μ
have h : ∀ (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))),
  Eq.{u_3 + 1} (α := E) (∫ (x : X), f x • (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E) x ∂μ)
    (((fun (u : ↥(Lp E 1 μ)) ↦ ∫ (x : X), (↑(↑u : X →ₘ[μ] E) : X → E) x ∂μ) ∘
        (⇑(withDensitySMulLI μ f_meas) : (a : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) → ↥(Lp E 1 μ)))
      u)
Tactic: convert! this with u
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (hypothesis)
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∞))
C1 :
  Continuous (Y := E) fun (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) ↦
    ∫ (x : X),
      (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E)
        x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)
⊢ IsClosed (X := ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))))
    {f_1 : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))) |
      (fun (g : X → E) ↦
          Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ))
        (↑(↑f_1 : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E)}
have C2 : Continuous (Y := E) fun (u : ↥(Lp E 1 (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)))) ↦
  ∫ (x : X), f x • (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E) x ∂μ
Tactic: have C2 : Continuous fun u : Lp E 1 (μ.withDensity fun x => f x) => ∫ x, f x • u x ∂μ := by
      have : Continuous ((fun u : Lp E 1 μ => ∫ x, u x ∂μ) ∘ withDensitySMulLI (E := E) μ f_meas) :=
        continuous_integral.comp (withDensitySMulLI (E := E) μ f_meas).continuous
      convert! this with u
      simp only [Function.comp_apply, withDensitySMulLI_apply]
      exact integral_congr_ae (memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), v x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • v x ∂μ)
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x • u x ∂μ) (∫ (x : X), f x • v x ∂μ)
Tactic: rw [← integral_congr_ae huv, hu]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x • u x ∂μ) (∫ (x : X), f x • v x ∂μ)
have pos : Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f a • u a) fun (a : X) ↦ f a • v a
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f a • u a) fun (a : X) ↦ f a • v a
have h : ∀ (x : X) (hx : (↑(f x) : ℝ≥0∞) ≠ 0 → u x = v x), f x • u x = f x • v x
Tactic: filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 huv] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ f x • u x = f x • v x
have h : ∀ (h'x : f x = 0), f x • u x = f x • v x
Tactic: rcases eq_or_ne (f x) 0 with (h'x | h'x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ f x • u x = f x • v x
have h₁ : ∀ (h'x : f x ≠ 0), f x • u x = f x • v x
Tactic: rcases eq_or_ne (f x) 0 with (h'x | h'x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
have rw : (↑(f x) : ℝ≥0∞) ≠ 0
Tactic: rw [hx _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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), g x ∂μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞))
have e_μ : (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) = μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) = μ.withDensity fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)
have e_μ : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)
Tactic: apply withDensity_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) fun (x : X) ↦ (↑(f' x) : ℝ≥0∞)
have h : ∀ (x : X) (hx : f x = AEMeasurable.mk f hf x), (↑(f x) : ℝ≥0∞) = (↑(f' x) : ℝ≥0∞)
Tactic: filter_upwards [hf.ae_eq_mk] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ (↑(f x) : ℝ≥0∞) = (↑(f' x) : ℝ≥0∞)
have h : (↑(AEMeasurable.mk f hf x) : ℝ≥0∞) = (↑(f' x) : ℝ≥0∞)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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), f' x • g x ∂μ) (∫ (x : X), f x • g x ∂μ)
have h : Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f' a • g a) fun (a : X) ↦ f a • g a
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f' a • g a) fun (a : X) ↦ f a • g a
have h : ∀ (x : X) (hx : f x = AEMeasurable.mk f hf x), f' x • g x = f x • g x
Tactic: filter_upwards [hf.ae_eq_mk] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ f' x • g x = f x • g x
have h : f' x • g x = AEMeasurable.mk f hf x • g x
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
have 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∞))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • g x ∂μ)
have g₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f' x • g x ∂μ) (∫ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toReal • g x ∂μ)
have dsimp : Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toNNReal • g x ∂μ)
Tactic: dsimp only [ENNReal.toReal, ← NNReal.smul_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toNNReal • g x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f)
  (∫ (x : X), g x ∂μ.withDensity fun (x : X) ↦ (↑(f x).toNNReal : ℝ≥0∞))
Tactic: rw [← integral_withDensity_eq_integral_smul₀ f_meas.ennreal_toNNReal,
    withDensity_congr_ae (coe_toNNReal_ae_eq hf_lt_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), (f x).toNNReal • g x ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂μ.withDensity f) (∫ (x : X), g x ∂μ.withDensity f)
Tactic: rw [← integral_withDensity_eq_integral_smul₀ f_meas.ennreal_toNNReal,
    withDensity_congr_ae (coe_toNNReal_ae_eq hf_lt_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [restrict_withDensity hs, integral_withDensity_eq_integral_smul₀ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ 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 ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x • g x ∂μ) (∫ (x : X) in s, f x • g x ∂μ)
Tactic: rw [restrict_withDensity hs, integral_withDensity_eq_integral_smul₀ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [restrict_withDensity hs, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ 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 ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (f x).toReal • g x ∂μ) (∫ (x : X) in s, (f x).toReal • g x ∂μ)
Tactic: rw [restrict_withDensity hs, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [restrict_withDensity' s, integral_withDensity_eq_integral_smul₀ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ 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 ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x • g x ∂μ) (∫ (x : X) in s, f x • g x ∂μ)
Tactic: rw [restrict_withDensity' s, integral_withDensity_eq_integral_smul₀ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity f) (∫ (x : X) in s, (f x).toReal • g x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X), g x ∂(μ.restrict s).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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, g x ∂μ.withDensity f) (∫ (x : X) in s, (f x).toReal • g x ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (f x).toReal • g x ∂μ) (∫ (x : X) in s, (f x).toReal • g x ∂μ)
Tactic: rw [restrict_withDensity' s, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]