awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : f =ᶠ[ae μ] fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞)
⊢ SigmaFinite (μ.withDensity fun (x : α) ↦ (↑(f x).toNNReal : ℝ≥0∞))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ≥0∞
hf_ne_top : ∀ (x : α), f x ≠ ∞
⊢ SigmaFinite (μ.withDensity f)

Tactic:
SigmaFinite.withDensity_of_ne_top <| ae_of_all _ hf_ne_top

Premises used: MeasureTheory.ae_of_all, MeasureTheory.SigmaFinite.withDensity_of_ne_top
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
obtain :
  ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hgf : g ≤ f)
    (hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

Tactic:
obtain ⟨g, hgm, hgf, hint⟩ := exists_measurable_le_forall_setLIntegral_eq μ f

Premises used: MeasureTheory.exists_measurable_le_forall_setLIntegral_eq
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
right : μ.withDensity g = μ.withDensity f
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

Tactic:
use g, hgm, hgf
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
right :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity g = μ.withDensity f

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [hint, withDensity_apply _ hs]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
inr :
  ∀ (this : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)) (hfm : ¬Measurable f),
    SFinite (μ.withDensity f)
wlog : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)
⊢ SFinite (μ.withDensity f)

Tactic:
wlog hfm : Measurable f generalizing f

Premises used: Measurable
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
this : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)
hfm : ¬Measurable f
inr : ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (h : μ.withDensity g = μ.withDensity f), SFinite (μ.withDensity f)
⊢ SFinite (μ.withDensity f)

Tactic:
rcases exists_measurable_le_withDensity_eq μ f with ⟨g, hgm, -, h⟩

Premises used: MeasureTheory.exists_measurable_le_withDensity_eq
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
this : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
h : μ.withDensity g = μ.withDensity f
⊢ SFinite (μ.withDensity f)

Tactic:
h ▸ this hgm

Premises used: Eq.rec
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
this : ∀ {f : α → ℝ≥0∞} (hfm : Measurable f), SFinite (μ.withDensity f)
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
h : μ.withDensity g = μ.withDensity f
⊢ SFinite (μ.withDensity f)

Tactic:
exact h ▸ this hgm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
inr :
  ∀ (this : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f))
    (hμ : ¬IsFiniteMeasure μ), SFinite (μ.withDensity f)
wlog : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)
⊢ SFinite (μ.withDensity f)

Tactic:
wlog hμ : IsFiniteMeasure μ generalizing μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
inr : SFinite.{u_1} (α := α) (m0 := m0) (sum fun (n : ℕ) ↦ (sfiniteSeq μ n).withDensity f)
⊢ SFinite (μ.withDensity f)

Tactic:
rw [← sum_sfiniteSeq μ, withDensity_sum]

Premises used: MeasureTheory.withDensity_sum, MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
⊢ ∀ (n : ℕ), SFinite ((sfiniteSeq μ n).withDensity f)

Tactic:
have (n : ℕ) : SFinite ((sfiniteSeq μ n).withDensity f) := this inferInstance
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
hfm : Measurable f
this_1 : ∀ {μ : Measure α} [SFinite μ] (hμ : IsFiniteMeasure μ), SFinite (μ.withDensity f)
hμ : ¬IsFiniteMeasure μ
this : ∀ (n : ℕ), SFinite ((sfiniteSeq μ n).withDensity f)
⊢ SFinite.{u_1} (α := α) (m0 := m0) (sum fun (n : ℕ) ↦ (sfiniteSeq μ n).withDensity f)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
⊢ MeasurableSet s

Tactic:
have hs : MeasurableSet s := hfm (measurableSet_singleton _)
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f)

Tactic:
simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]

Premises used: MeasureTheory.withDensity_indicator, MeasureTheory.restrict_withDensity
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
⊢ ∀ (i : ℕ), Measurable (β := ℝ≥0∞) (s.indicator 1)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
rw :
  μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
    μ.withDensity (sᶜ.indicator f) + μ.withDensity (∑' (n : ℕ), s.indicator 1)
⊢ μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
    μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)

Tactic:
rw [← withDensity_tsum (by measurability)]

Premises used: MeasureTheory.withDensity_tsum
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
e_a : ∀ (x : α), s.indicator f x = (∑' (n : ℕ), s.indicator 1) x
⊢ μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) =
    μ.withDensity (sᶜ.indicator f) + μ.withDensity (∑' (n : ℕ), s.indicator 1)

Tactic:
congr 2 with x
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
x : α
e_a : s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
⊢ s.indicator f x = (∑' (n : ℕ), s.indicator 1) x

Tactic:
rw [ENNReal.tsum_apply]

Premises used: ENNReal.tsum_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x

Tactic:
simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]

Premises used: ENNReal.tsum_const_eq_top_of_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
x : α
if : ∀ (hx : x ∈ s), s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
if₁ : ∀ (hx : x ∉ s), s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
if₂ : ∀ (hx : x ∈ s), s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
if₃ if₄ : ∀ (hx : x ∉ s), s.indicator f x = ∑' (i : ℕ), s.indicator 1 x
⊢ s.indicator f x = ∑' (i : ℕ), s.indicator 1 x

Tactic:
if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]
      else simp [hx]

Premises used: ENNReal.tsum_const_eq_top_of_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
⊢ μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)

Tactic:
have key := calc
    μ.withDensity f = μ.withDensity (sᶜ.indicator f) + μ.withDensity (s.indicator f) := by
      simp (disch := measurability) [withDensity_indicator, ← restrict_withDensity]
    _ = μ.withDensity (sᶜ.indicator f) + .sum fun _ : ℕ ↦ μ.withDensity (s.indicator 1) := by
      rw [← withDensity_tsum (by measurability)]
      congr 2 with x
      rw [ENNReal.tsum_apply]
      if hx : x ∈ s then simpa [hx, ENNReal.tsum_const_eq_top_of_ne_zero]
      else simp [hx]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
⊢ SigmaFinite (μ.withDensity (sᶜ.indicator f))

Tactic:
SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_

Premises used: MeasureTheory.ae_of_all, MeasureTheory.SigmaFinite.withDensity_of_ne_top
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
refine : ∀ (x : α) (hx : sᶜ.indicator f x = ∞), False
⊢ SigmaFinite (μ.withDensity (sᶜ.indicator f))

Tactic:
refine SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_

Premises used: MeasureTheory.ae_of_all, MeasureTheory.SigmaFinite.withDensity_of_ne_top
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
x : α
hx : sᶜ.indicator f x = ∞
⊢ False

Tactic:
simp [indicator_apply, ite_eq_iff, s] at hx

Premises used: Set.indicator_apply, ite_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
⊢ SigmaFinite (μ.withDensity (sᶜ.indicator f))

Tactic:
have : SigmaFinite (μ.withDensity (sᶜ.indicator f)) := by
    refine SigmaFinite.withDensity_of_ne_top <| ae_of_all _ fun x hx ↦ ?_
    simp [indicator_apply, ite_eq_iff, s] at hx
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
rw : SigmaFinite ((μ.restrict s).withDensity 1)
⊢ SigmaFinite (μ.withDensity (s.indicator 1))

Tactic:
rw [withDensity_indicator hs]

Premises used: MeasureTheory.withDensity_indicator
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SigmaFinite ((μ.restrict s).withDensity 1)

Tactic:
SigmaFinite.withDensity 1

Premises used: MeasureTheory.SigmaFinite.withDensity, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SigmaFinite ((μ.restrict s).withDensity 1)

Tactic:
exact SigmaFinite.withDensity 1

Premises used: MeasureTheory.SigmaFinite.withDensity, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SigmaFinite (μ.withDensity (s.indicator 1))

Tactic:
have : SigmaFinite (μ.withDensity (s.indicator 1)) := by
    rw [withDensity_indicator hs]
    exact SigmaFinite.withDensity 1
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this_1 : SigmaFinite (μ.withDensity (sᶜ.indicator f))
this : SigmaFinite (μ.withDensity (s.indicator 1))
rw : SFinite (μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1))
⊢ SFinite (μ.withDensity f)

Tactic:
rw [key]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x : α | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1)
this_1 : SigmaFinite (μ.withDensity (sᶜ.indicator f))
this : SigmaFinite (μ.withDensity (s.indicator 1))
⊢ SFinite (μ.withDensity (sᶜ.indicator f) + sum fun (x : ℕ) ↦ μ.withDensity (s.indicator 1))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℝ≥0∞
rw : SFinite (μ.withDensity fun (x : α) ↦ c)
⊢ SFinite (c • μ)

Tactic:
rw [← withDensity_const]

Premises used: MeasureTheory.withDensity_const
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℝ≥0∞
⊢ SFinite (μ.withDensity fun (x : α) ↦ c)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
rw : SFinite (μ.restrict (μ.sigmaFiniteSetWRT ν) + HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ))
⊢ SFinite μ

Tactic:
rw [← Measure.restrict_add_restrict_compl (μ := μ) measurableSet_sigmaFiniteSetWRT,
    restrict_compl_sigmaFiniteSetWRT hμν]

Premises used: MeasureTheory.Measure.restrict_add_restrict_compl, MeasureTheory.restrict_compl_sigmaFiniteSetWRT, MeasureTheory.measurableSet_sigmaFiniteSetWRT
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
⊢ SFinite (μ.restrict (μ.sigmaFiniteSetWRT ν) + HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
obtain :
  ∀ (s : Set α)
    (h :
      μ =
        sum fun (x : (↑s : Type u_1)) ↦
          HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
            (dirac (↑x : α))),
    SFinite μ
⊢ SFinite μ

Tactic:
obtain ⟨s, h⟩ := exists_sum_smul_dirac μ

Premises used: MeasureTheory.Measure.exists_sum_smul_dirac
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
s : Set α
h :
  μ =
    sum fun (x : (↑s : Type u_1)) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
        (dirac (↑x : α))
rw :
  SFinite.{u_1} (α := α) (m0 := m0)
    (sum fun (x : (↑s : Type u_1)) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
        (dirac (↑x : α)))
⊢ SFinite μ

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
s : Set α
h :
  μ =
    sum fun (x : (↑s : Type u_1)) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
        (dirac (↑x : α))
⊢ SFinite.{u_1} (α := α) (m0 := m0)
    (sum fun (x : (↑s : Type u_1)) ↦
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom (↑x : α)) : ℝ≥0∞)
        (dirac (↑x : α)))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1

Tactic:
ext_of_lintegral _ fun φ hφ ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
refine :
  ∀ (φ : α × β → ℝ≥0∞) (hφ : Measurable φ),
    ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ f z.1
⊢ (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun (z : α × β) ↦ f z.1

Tactic:
refine ext_of_lintegral _ fun φ hφ ↦ ?_

Premises used: MeasureTheory.Measure.ext_of_lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ
hf₁ : AEMeasurable ((fun (z : α × β) ↦ f z.1) * φ) (μ.prod ν)
rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1) (μ.prod ν)
rw₂ : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ
⊢ ∫⁻ (a : α × β), φ a ∂(μ.withDensity f).prod ν = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun (z : α × β) ↦ f z.1

Tactic:
rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ hf,
    lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ

Tactic:
lintegral_congr (fun x ↦ ?_)

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
refine :
  ∀ (x : α),
    HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) x =
      ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν
⊢ ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ =
    ∫⁻ (x : α), ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν ∂μ

Tactic:
refine lintegral_congr (fun x ↦ ?_)

Premises used: MeasureTheory.lintegral_congr
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : β) ↦ φ (x, y)) ν

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
rw : ∫⁻ (a : β), f x * φ (x, a) ∂ν = ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν
⊢ HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ∫⁻ (y : β), φ (x, y) ∂ν) x =
    ∫⁻ (y : β), HMul.hMul (α := α × β → ℝ≥0∞) (fun (z : α × β) ↦ f z.1) φ (x, y) ∂ν

Tactic:
rw [Pi.mul_apply, ← lintegral_const_mul'' _ (by fun_prop)]

Premises used: Pi.mul_apply, MeasureTheory.lintegral_const_mul''