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

Tactic:
refine Integrable.induction
  (P := fun g => ∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ) ?_ ?_ ?_ ?_ hg

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

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

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}

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

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

Tactic:
simp only [h'x, zero_smul]

Result:
no goals

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

Tactic:
simp only [Function.comp_apply, withDensitySMulLI_apply]

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 ∂μ = ∫ (x : X), ↑↑(MemLp.toLp (fun x => f x • ↑↑u x) ⋯) x ∂μ

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

Tactic:
by_cases hg : Integrable g (μ.withDensity fun x => f x)

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
hg : Integrable g (μ.withDensity fun x => ↑(f x))
⊢ (∫ (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
hg : ¬Integrable g (μ.withDensity fun x => ↑(f x))
⊢ (∫ (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))
⊢ ∀ ⦃f_1 g : X → E⦄,
    Disjoint (support f_1) (support g) →
      Integrable f_1 (μ.withDensity fun x => ↑(f x)) →
        Integrable g (μ.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 →
              (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) (f_1 + g)

Tactic:
intro u u' _ u_int u'_int h h'

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

Tactic:
rw [integral_undef hg, integral_undef]

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