-- 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_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))
⊢ IsClosed {f_1 | (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) ↑↑f_1}

Tactic:
have C1 :
  Continuous fun u : Lp E 1 (μ.withDensity fun x => f x) =>
    ∫ x, u x ∂μ.withDensity fun x => f x :=
  continuous_integral

Result:
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)
⊢ IsClosed {f_1 | (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) ↑↑f_1}

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) ∂μ).toReal • c = ∫ (a : X) in s, f a • c ∂μ

Tactic:
rw [lintegral_coe_eq_integral, ENNReal.toReal_ofReal, ← integral_smul_const]

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, ↑(f x) • c ∂μ = ∫ (a : X) in s, f a • c ∂μ

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 < ⊤
⊢ 0 ≤ ∫ (a : X) in s, ↑(f a) ∂μ

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)

Proof state:
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

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

Result:
case 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 ∂μ
x : X
hx : ↑(f x) ≠ 0 → u x = v x
⊢ f x • u x = f x • v x

Proof state:
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
hg : ¬Integrable g (μ.withDensity fun x => ↑(f x))
⊢ ¬Integrable (fun x => f x • g x) μ

Tactic:
rwa [← integrable_withDensity_iff_integrable_smul f_meas]

Result:
no goals

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
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x => ↑(f x))
C1 : Continuous fun u => ∫ (x : X), ↑↑u x ∂μ.withDensity fun x => ↑(f x)
⊢ Continuous fun u => ∫ (x : X), f x • ↑↑u x ∂μ

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

Result:
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))
⊢ Continuous fun u => ∫ (x : X), f x • ↑↑u x ∂μ

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
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
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ ↑(f x) ≠ 0

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

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), s.indicator (fun x => c) x ∂μ.withDensity fun x => ↑(f x)) =
    ∫ (x : X), f x • s.indicator (fun x => c) x ∂μ

Tactic:
rw [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)) = ∫ (x : X), f x • s.indicator (fun x => c) 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 < ⊤
⊢ HasFiniteIntegral (fun x => ↑(f x)) (μ.restrict s)

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

Result:
no goals