awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 μ)
⊢ ∫⁻ (a : G), φ a ∂μ.withDensity f ∗ₘ μ.withDensity g = ∫⁻ (a : G), φ a ∂μ.withDensity (f ⋆ₘₗ[μ] g)
have hg₂ : AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ φ (z.1 * z.2)) (μ.prod μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 φ
⊢ ∫⁻ (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 ∂μ
have simp : ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a ∂μ
Tactic: simp only [Pi.mul_apply, mul_inv_cancel_left, mlconvolution_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : G) ↦ f y * g (y⁻¹ * a)) μ
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : G) ↦ f y * g (y⁻¹ * a)) μ
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : G) ↦ f y * g (y⁻¹ * a)) μ
have funProp₂ : Measure.map (fun (a_1 : G) ↦ a_1⁻¹ * a) μ ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
| (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a
have rw : ∫⁻ (a_1 : G), f a_1 * g (a_1⁻¹ * a) * φ a ∂μ
Tactic: rw [(lintegral_mul_const'' _ (by fun_prop)).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 φ
⊢ ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a ∂μ
have conv : ∫⁻ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 ∂μ
⊢ ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), (∫⁻ (y : G), f y * g (y⁻¹ * a) ∂μ) * φ a ∂μ
have conv₁ : ∫⁻ (y : G), ∫⁻ (x : G), f x * g (x⁻¹ * y) * φ y ∂μ ∂μ = ∫⁻ (a : G), ∫⁻ (a_1 : G), f a_1 * g (a_1⁻¹ * a) * φ a ∂μ ∂μ
Tactic: conv in (∫⁻ _, _ ∂μ) * φ _ => rw [(lintegral_mul_const'' _ (by fun_prop)).symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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∞)
    (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 μ)
have hf₁ : AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
have funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (Function.uncurry fun (a x : G) ↦ f a * g (a⁻¹ * x) * φ (a * (a⁻¹ * x))) (μ.prod μ)
have funProp₅ : Measure.map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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 (HMul.hMul (α := G × G → ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) fun (z : G × G) ↦ φ (z.1 * z.2))
    (μ.prod μ)
have funProp : mG ≤ mG
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ 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 μ)
have funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp : mG ≤ mG
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₂ : Measure.map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : G × G) ↦ f z.1 * g z.2) (μ.prod μ)
have funProp₅ : Measure.map (fun (a : G × G) ↦ a.2) (μ.prod μ) ≪ μ
Tactic: first | fun_prop | dsimp; fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensityFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ ae (if IsFiniteMeasure μ then μ else ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ
have pos : IsFiniteMeasure μ → ae μ = ae μ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensityFinite (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
pos : IsFiniteMeasure μ → ae μ = ae μ
⊢ ae (if IsFiniteMeasure μ then μ else ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ
have neg : ¬IsFiniteMeasure μ → ae (sorry.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensityFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
⊢ ae (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ
have left : IsFiniteMeasure (sorry.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
Tactic: obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensityFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
left : IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
⊢ ae (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ
have h₁ : μ ≪ sorry.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)
Tactic: obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensityFinite (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
h : ¬IsFiniteMeasure μ
left : IsFiniteMeasure (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ))
h₁ : μ ≪ ⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)
⊢ ae (⋯.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ)) = ae μ
have h₂ : sorry.choose (p := fun (ν : Measure α) ↦ IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ) ≪ μ
Tactic: obtain ⟨_, h₁, h₂⟩ := (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec