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∞))
c : E
s : Set X
s_meas : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : X) ↦ (↑(f x) : ℝ)) (μ.restrict s)

Tactic:
simpa [withDensity_apply _ s_meas, hasFiniteIntegral_iff_enorm] using hs

Premises used: MeasureTheory.hasFiniteIntegral_iff_enorm, MeasureTheory.withDensity_apply
-- 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 u' : X → E
pos :
  Disjoint (Function.support u) (Function.support u') →
    Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) →
      Integrable u' (μ.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 ∂μ))
            u →
          (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 ∂μ))
              u' →
            (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 ∂μ))
              (u + u')
⊢ Disjoint (Function.support u) (Function.support u') →
    Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) →
      Integrable u' (μ.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 ∂μ))
            u →
          (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 ∂μ))
              u' →
            (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 ∂μ))
              (u + u')

Tactic:
_
-- 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 u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
pos :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • (u x + u' x) ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), (u + u') x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • (u + u') x ∂μ)

Tactic:
change
      (∫ x : X, u x + u' x ∂μ.withDensity fun x : X => ↑(f x)) = ∫ x : X, f x • (u x + u' x) ∂μ

Premises used: MeasureTheory.Measure.withDensity, ENNReal.ofNNReal, HAdd.hAdd, MeasureTheory.integral
-- 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 u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
pos :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • u x + f x • u' x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • (u x + u' x) ∂μ)

Tactic:
simp_rw [smul_add]

Premises used: smul_add
-- 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 u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
pos : Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u x) μ
pos₁ : Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u' x) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), u x + u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
    (∫ (x : X), f x • u x + f x • u' x ∂μ)

Tactic:
rw [integral_add u_int u'_int, h, h', integral_add]

Premises used: MeasureTheory.integral_add
-- 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 u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
⊢ Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u x) μ

Tactic:
(integrable_withDensity_iff_integrable_smul f_meas).1 u_int

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul, 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 u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
⊢ Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u x) μ

Tactic:
exact (integrable_withDensity_iff_integrable_smul f_meas).1 u_int

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul, 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 u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
⊢ Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u' x) μ

Tactic:
(integrable_withDensity_iff_integrable_smul f_meas).1 u'_int

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul, 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 u' : X → E
h_1 : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
u'_int : Integrable u' (μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞))
h : Eq.{u_3 + 1} (α := E) (∫ (x : X), u x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u x ∂μ)
h' : Eq.{u_3 + 1} (α := E) (∫ (x : X), u' x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • u' x ∂μ)
⊢ Integrable.{u_3, u_1} (ε := E) (fun (x : X) ↦ f x • u' x) μ

Tactic:
exact (integrable_withDensity_iff_integrable_smul f_meas).1 u'_int

Premises used: MeasureTheory.integrable_withDensity_iff_integrable_smul, 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∞))
⊢ 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
-- 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∞))
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 (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
-- 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∞))
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 (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:
this
-- 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∞))
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 μ)))
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)
⊢ 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:
convert! this with u
-- 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∞))
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 μ)))
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 ∂μ)
    (∫ (x : X),
      (↑(↑(MemLp.toLp (fun (x : X) ↦ f x • (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E) x) ⋯) :
              X →ₘ[μ] E) :
          X → E)
        x ∂μ)

Tactic:
integral_congr_ae (memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp.symm

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.memL1_smul_of_L1_withDensity, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.symm
-- 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∞))
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 μ)))
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 ∂μ)
    (∫ (x : X),
      (↑(↑(MemLp.toLp (fun (x : X) ↦ f x • (↑(↑u : X →ₘ[μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)] E) : X → E) x) ⋯) :
              X →ₘ[μ] E) :
          X → E)
        x ∂μ)

Tactic:
exact integral_congr_ae (memL1_smul_of_L1_withDensity f_meas u).coeFn_toLp.symm

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.memL1_smul_of_L1_withDensity, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.symm
-- 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∞))
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 ∂μ

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
-- 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∞))
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∞)
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 ∂μ
⊢ 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)}

Tactic:
isClosed_eq C1 C2

Premises used: setOf, isClosed_eq
-- 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∞))
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∞)
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 ∂μ
⊢ 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)}

Tactic:
exact isClosed_eq C1 C2

Premises used: isClosed_eq
-- 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
pos :
  Integrable u (μ.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 ∂μ))
        u →
      (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 ∂μ))
        v
⊢ Integrable u (μ.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 ∂μ))
        u →
      (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 ∂μ))
        v

Tactic:
_
-- 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 ∂μ)
pos : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x • u x ∂μ) (∫ (x : X), f x • v x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), v x ∂μ.withDensity fun (x : X) ↦ (↑(f x) : ℝ≥0∞)) (∫ (x : X), f x • v x ∂μ)

Tactic:
rw [← integral_congr_ae huv, hu]

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
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 ∂μ)
pos : Filter.EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (a : X) ↦ f a • u a) fun (a : X) ↦ f a • v a
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x • u x ∂μ) (∫ (x : X), f x • v x ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae