-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_withDensity_eq_integral_smul {f : X → ℝ≥0} (f_meas : Measurable f) (g : X → E) :
    ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ

Proof state:
case pos.refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : X) in s, c ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • s.indicator (fun x => c) x ∂μ

Tactic:
simp_rw [← indicator_smul_apply, integral_indicator s_meas]

Result:
case pos.refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : X) in s, c ∂μ.withDensity fun x => ↑(f x)) = ∫ (a : X) in s, f a • c ∂μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
⊢ (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
⊢ (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

case neg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : ¬CompleteSpace E
⊢ (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ

Proof state:
case pos.refine_2
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
u u' : X → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u (μ.withDensity fun x => ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x => ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ (∫ (x : X), u x + u' x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u x + f x • u' x ∂μ

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

Result:
case pos.refine_2.hf
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
u u' : X → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u (μ.withDensity fun x => ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x => ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ Integrable (fun x => f x • u x) μ

case pos.refine_2.hg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
u u' : X → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u (μ.withDensity fun x => ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x => ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ Integrable (fun x => f x • u' x) μ

Proof state:
case pos.refine_1.hfi
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x => ↑(f x)) s < ⊤
⊢ Integrable (fun x => ↑(f x)) (μ.restrict s)

Tactic:
refine ⟨f_meas.coe_nnreal_real.aemeasurable.aestronglyMeasurable, ?_⟩

Result:
case pos.refine_1.hfi
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x => ↑(f x)) s < ⊤
⊢ HasFiniteIntegral (fun x => ↑(f x)) (μ.restrict s)

Proof state:
case h.e'_5.h
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
C1 : Continuous fun u => ∫ (x : X), ↑↑u x ∂μ.withDensity fun x => ↑(f x)
this : Continuous ((fun u => ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas))
u : ↥(Lp E 1 (μ.withDensity fun x => ↑(f x)))
⊢ ∫ (x : X), f x • ↑↑u x ∂μ = ∫ (x : X), ↑↑(MemLp.toLp (fun x => f x • ↑↑u x) ⋯) x ∂μ

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

Result:
no goals

Proof state:
case pos.refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
c : E
s : Set X
s_meas : MeasurableSet s
hs : (μ.withDensity fun x => ↑(f x)) s < ⊤
⊢ ∫ (x : X) in s, ↑(f x) • c ∂μ = ∫ (a : X) in s, f a • c ∂μ

Tactic:
rfl

Result:
no goals

Proof state:
case pos.refine_4
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
u v : X → E
huv : u =ᶠ[ae (μ.withDensity fun x => ↑(f x))] v
a✝ : Integrable u (μ.withDensity fun x => ↑(f x))
hu : (∫ (x : X), u x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u x ∂μ
⊢ ∫ (x : X), f x • u x ∂μ = ∫ (x : X), f x • v x ∂μ

Tactic:
apply integral_congr_ae

Result:
case pos.refine_4.h
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
u v : X → E
huv : u =ᶠ[ae (μ.withDensity fun x => ↑(f x))] v
a✝ : Integrable u (μ.withDensity fun x => ↑(f x))
hu : (∫ (x : X), u x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • u x ∂μ
⊢ (fun a => f a • u a) =ᶠ[ae μ] fun a => f a • v a

Proof state:
case pos.refine_3
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
C1 : Continuous fun u => ∫ (x : X), ↑↑u x ∂μ.withDensity fun x => ↑(f x)
C2 : Continuous fun u => ∫ (x : X), f x • ↑↑u x ∂μ
⊢ IsClosed {f_1 | (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) ↑↑f_1}

Tactic:
exact isClosed_eq C1 C2

Result:
no goals