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

Tactic:
rw [← integral_congr_ae 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), f x • u x ∂μ = ∫ (x : X), f x • v 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))
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 ∂μ

Tactic:
convert this with u

Result:
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 ∂μ = ((fun u => ∫ (x : X), ↑↑u x ∂μ) ∘ ⇑(withDensitySMulLI μ f_meas)) u

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

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

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

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

Tactic:
swap

Result:
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 ∂μ

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 ∂μ

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

Tactic:
simp_rw [smul_add]

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 + f x • u' x ∂μ

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

Tactic:
rcases eq_or_ne (f x) 0 with (h'x | h'x)

Result:
case h.inl
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

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