awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
x : G
⊢ ∫⁻ (y : G),
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, y) ∂μ =
    ∫⁻ (x_1 : G),
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * x_1) ∂μ

Tactic:
apply (lintegral_mul_left_eq_self _ x⁻¹).symm

Premises used: Inv.inv, Eq.symm, MeasureTheory.lintegral_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
rw :
  ∫⁻ (y : G),
      ∫⁻ (x : G),
        HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
          (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ
hf₁ :
  AEMeasurable (β := ℝ≥0∞)
    (Function.uncurry fun (a x : G) ↦
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (a, a⁻¹ * x))
    (μ.prod μ)
hf₂ :
  AEMeasurable (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)
hf₃ : AEMeasurable (f ⋆ₘₗ[μ] g) μ
hg₁ : AEMeasurable φ μ
hf₄ : AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
hg₂ : AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ φ (z.1 * z.2)) (μ.prod μ)
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)

Tactic:
rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]

Premises used: MeasureTheory.prod_withDensity₀, MeasureTheory.lintegral_congr, MeasureTheory.lintegral_prod, MeasureTheory.lintegral_lintegral_swap, MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀, MeasureTheory.Measure.lintegral_mconv_eq_lintegral_prod
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
simp : ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a ∂μ
⊢ ∫⁻ (y : G),
      ∫⁻ (x : G),
        HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
          (fun (z : G × G) ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ

Tactic:
simp only [Pi.mul_apply, mul_inv_cancel_left, mlconvolution_def]

Premises used: Pi.mul_apply, MeasureTheory.mlconvolution_def, mul_inv_cancel_left
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
a : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₂ : Measure.map (fun (a_1 : G) ↦ a_1⁻¹ * a) μ ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : G) ↦ f y * g (y⁻¹ * a)) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
a : G
rw : ∫⁻ (a_1 : G), f a_1 * g (a_1⁻¹ * a) * φ a ∂μ
| (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a

Tactic:
rw [(lintegral_mul_const'' _ (by fun_prop)).symm]

Premises used: MeasureTheory.lintegral_mul_const'', Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
conv : ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a ∂μ
conv₁ :
  ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), ∫⁻ (a_1 : G), f a_1 * g (a_1⁻¹ * a) * φ a ∂μ ∂μ
⊢ ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a ∂μ

Tactic:
conv in (∫⁻ _, _ ∂μ) * φ _ => rw [(lintegral_mul_const'' _ (by fun_prop)).symm]

Premises used: MeasureTheory.lintegral_mul_const'', Eq.symm, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
hf₁ : AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
⊢ AEMeasurable (β := ℝ≥0∞)
    (Function.uncurry fun (a x : G) ↦
      HMul.hMul (α := G × G → ℝ≥0∞) (β := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2)
        (fun (z : G × G) ↦ φ (z.1 * z.2)) (a, a⁻¹ * x))
    (μ.prod μ)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : Measure.map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
⊢ AEMeasurable (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
⊢ AEMeasurable (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)

Tactic:
first | fun_prop | dsimp; fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (f ⋆ₘₗ[μ] g) μ

Tactic:
first | fun_prop | dsimp; fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable φ μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable φ μ

Tactic:
first | fun_prop | dsimp; fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)

Tactic:
first | fun_prop | dsimp; fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ φ (z.1 * z.2)) (μ.prod μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ φ (z.1 * z.2)) (μ.prod μ)

Tactic:
first | fun_prop | dsimp; fun_prop
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
G : Type u_3
inst : Group G
mG : MeasurableSpace G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : SFinite μ
inst_4 : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ μ.withDensity f ∗ₘ μ.withDensity g = μ.withDensity (f ⋆ₘₗ[μ] g)

Tactic:
mconv_withDensity_eq_mlconvolution₀ hf.aemeasurable hg.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.mconv_withDensity_eq_mlconvolution₀
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
pos : IsFiniteMeasure μ → ae μ = ae μ
neg : ¬IsFiniteMeasure μ → ae (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ
⊢ ae (if IsFiniteMeasure μ then μ else ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : IsFiniteMeasure μ
⊢ ae μ = ae μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
⊢ IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))

Tactic:
obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec

Premises used: Exists.choose_spec, MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
left : IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
⊢ μ ≪ ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)

Tactic:
obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec

Premises used: Exists.choose_spec, MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
left : IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
h₁ : μ ≪ ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)
⊢ ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ) ≪ μ

Tactic:
obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec

Premises used: Exists.choose_spec, MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
left : IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
h₁ : μ ≪ ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)
h₂ : ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ) ≪ μ
⊢ ae (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ

Tactic:
h₂.ae_le.antisymm h₁.ae_le

Premises used: LE.le.antisymm, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
left : IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
h₁ : μ ≪ ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)
h₂ : ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ) ≪ μ
⊢ ae (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ

Tactic:
exact h₂.ae_le.antisymm h₁.ae_le

Premises used: LE.le.antisymm, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
pos : IsFiniteMeasure μ → IsFiniteMeasure μ
neg : ¬IsFiniteMeasure μ → IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
⊢ IsFiniteMeasure
    (if IsFiniteMeasure μ then μ else ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : IsFiniteMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
⊢ IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))

Tactic:
(exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec.1

Premises used: Exists.choose_spec, And.left, MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
⊢ IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))

Tactic:
exact (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec.1

Premises used: Exists.choose_spec, And.left, MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ ae μ.toFinite = ae μ

Tactic:
simp [Measure.toFinite, ProbabilityTheory.cond]

Premises used: ProbabilityTheory.cond, MeasureTheory.Measure.toFinite
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ.toFinite : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [← compl_mem_ae_iff, ae_toFinite]

Premises used: MeasureTheory.ae_toFinite, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
simp_rw :
  Eq (α := ℝ≥0∞) ((μ.toFinite : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.toFinite = 0 ↔ μ = 0

Tactic:
simp_rw [← Measure.measure_univ_eq_zero, toFinite_apply_eq_zero_iff]

Premises used: MeasureTheory.Measure.measure_univ_eq_zero, MeasureTheory.toFinite_apply_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (Measure.toFinite 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
hc : IsFiniteMeasure μ
⊢ μ.toFinite = μ

Tactic:
rw [Measure.toFinite, Measure.toFiniteAux, if_pos, ProbabilityTheory.cond_univ]

Premises used: if_pos, ProbabilityTheory.cond_univ, MeasureTheory.Measure.toFinite, MeasureTheory.Measure.toFiniteAux
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ IsFiniteMeasure μ.toFiniteAux[|univ]

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
inst_1 : NeZero μ
hcs : Ne (α := ℝ≥0∞) ((μ.toFiniteAux : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsProbabilityMeasure μ.toFinite

Tactic:
apply ProbabilityTheory.cond_isProbabilityMeasure

Premises used: ProbabilityTheory.cond_isProbabilityMeasure
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
inst_1 : NeZero μ
⊢ Ne (α := ℝ≥0∞) ((μ.toFiniteAux : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [ne_eq, ← compl_mem_ae_iff, ae_toFiniteAux]

Premises used: ne_eq, MeasureTheory.ae_toFiniteAux, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ μ ≪ μ.toFinite

Tactic:
Measure.ae_le_iff_absolutelyContinuous.mp ae_toFinite.ge

Premises used: Eq.ge, MeasureTheory.ae_toFinite, MeasureTheory.Measure.ae_le_iff_absolutelyContinuous, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
n : ℕ
⊢ sfiniteSeq μ n ≪ μ.toFinite

Tactic:
(sfiniteSeq_le μ n).absolutelyContinuous.trans (absolutelyContinuous_toFinite μ)

Premises used: MeasureTheory.absolutelyContinuous_toFinite, MeasureTheory.sfiniteSeq_le, MeasureTheory.Measure.AbsolutelyContinuous.trans, LE.le.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ μ.toFinite ≪ μ

Tactic:
Measure.ae_le_iff_absolutelyContinuous.mp ae_toFinite.le

Premises used: MeasureTheory.ae_toFinite, Eq.le, MeasureTheory.Measure.ae_le_iff_absolutelyContinuous, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
rw :
  HSMul.hSMul (α := ℝ≥0∞) ∞ (μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) =
    HSMul.hSMul (α := ℝ≥0∞) ∞ (μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ)
⊢ μ.restrict μ.sigmaFiniteSetᶜ = HSMul.hSMul (α := ℝ≥0∞) ∞ (μ.toFinite.restrict μ.sigmaFiniteSetᶜ)

Tactic:
rw [Measure.sigmaFiniteSet,
    restrict_compl_sigmaFiniteSetWRT (Measure.AbsolutelyContinuous.refl μ)]

Premises used: MeasureTheory.Measure.sigmaFiniteSet, MeasureTheory.restrict_compl_sigmaFiniteSetWRT, MeasureTheory.Measure.AbsolutelyContinuous.refl
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h :
  ∀ (t : Set α) (ht : MeasurableSet t),
    Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := ℝ≥0∞) ∞ (μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) ∞ (μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HSMul.hSMul (α := ℝ≥0∞) ∞ (μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) =
    HSMul.hSMul (α := ℝ≥0∞) ∞ (μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ)

Tactic:
ext t ht
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
t : Set α
ht : MeasurableSet t
h :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply ht, Measure.restrict_apply ht]

Premises used: MeasureTheory.Measure.restrict_apply