-- 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_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) μ

Tactic:
exact (integrable_withDensity_iff_integrable_smul f_meas).1 u_int

Result:
no goals

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 + u') x ∂μ.withDensity fun x => ↑(f x)) = ∫ (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) ∂μ

Result:
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 + u' x) ∂μ

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

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

Result:
no goals

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

Tactic:
simp [integral, hE]

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))
⊢ ∀ ⦃f_1 g : X → E⦄,
    f_1 =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g →
      Integrable f_1 (μ.withDensity fun x => ↑(f x)) →
        (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) f_1 →
          (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) g

Tactic:
intro u v huv _ hu

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

Tactic:
simp only [s_meas, integral_const, Measure.restrict_apply', univ_inter, withDensity_apply]

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

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

Tactic:
intro c s s_meas hs

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

Proof state:
case h.inr
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 • u x = f x • v x

Tactic:
rw [hx _]

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))
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