-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem lintegral_withDensity_eq_lintegral_mul_non_measurable (μ : Measure α) {f : α → ℝ≥0∞}
    (f_meas : Measurable f) (hf : ∀ᵐ x ∂μ, f x < ∞) (g : α → ℝ≥0∞) :
    ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, (f * g) a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = f x * ((f x)⁻¹ * i x)

Tactic:
rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]

Result:
no goals

Proof state:
case h.inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x

Tactic:
have := hi x

Result:
case h.inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
this : i x ≤ (f * g) x
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f

Tactic:
have A : (fun x => (f x)⁻¹ * i x) ≤ g := by
  intro x
  dsimp
  rw [mul_comm, ← div_eq_mul_inv]
  exact div_le_of_le_mul' (hi x)

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = (f * fun a => (f a)⁻¹ * i a) x

Tactic:
dsimp

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = f x * ((f x)⁻¹ * i x)

Proof state:
case h.inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
this : i x ≤ (f * g) x
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x

Tactic:
simp only [hx, zero_mul, Pi.mul_apply, nonpos_iff_eq_zero] at this

Result:
case h.inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
this : i x = 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x

Proof state:
case h.inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x

Tactic:
apply le_of_eq _

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = (f * fun a => (f a)⁻¹ * i a) x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ i x / f x ≤ g x

Tactic:
exact div_le_of_le_mul' (hi x)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), (f * fun a => (f a)⁻¹ * i a) a ∂μ

Tactic:
apply lintegral_mono_ae

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ ∀ᵐ (a : α) ∂μ, i a ≤ (f * fun a => (f a)⁻¹ * i a) a