awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hf : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
simp_rw :
  Eq (α := ℝ≥0∞) ((μ.prod μ : (a : Set (G × G)) → ℝ≥0∞) ((fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) : ℝ≥0∞)
    (0 : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (y : G),
      (μ : (a : Set G) → ℝ≥0∞)
        (preimage (β := G × G) (fun (x : G) ↦ (x, y)) ((fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹)) ∂μ =
    0
simp_rw₂ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ (y * x, x⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) ∂μ = 0
simp_rw₃ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ Inv.inv ⁻¹' s⁻¹) ∂μ = 0
simp_rw₄ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ s⁻¹⁻¹) ∂μ = 0
simp_rw₅ : ∫⁻ (y : G), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ s) ∂μ = 0
⊢ Eq (α := ℝ≥0∞)
    (((map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ) : Measure (G × G)) : (a : Set (G × G)) → ℝ≥0∞)
        (s⁻¹ ×ˢ s⁻¹) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have simp_rw₆ : ∫⁻ (y : G), 0 ∂μ = 0
Tactic: simp_rw [map_apply hf hsm', prod_apply_symm (μ := μ) (ν := μ) (hf hsm'), preimage_preimage,
    mk_preimage_prod, inv_preimage, inv_inv, measure_mono_null inter_subset_right hμs,
    lintegral_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨fun hs => ?_, (quasiMeasurePreserving_inv μ).preimage_null⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← inv_inv s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ (ae μ)⁻¹ = ae μ
have refine : ae μ ≤ (ae μ)⁻¹
Tactic: refine le_antisymm (quasiMeasurePreserving_inv μ).tendsto_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ ae μ ≤ (ae μ)⁻¹
have nth_rewrite : (ae μ)⁻¹⁻¹ ≤ (ae μ)⁻¹
Tactic: nth_rewrite 1 [← inv_inv (ae μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)
have rw : EventuallyConst (Inv.inv ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
Tactic: rw [← inv_preimage, eventuallyConst_preimage, Filter.map_inv, inv_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
rw : EventuallyConst (Inv.inv ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
⊢ EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)
have rw₁ : EventuallyConst s (Filter.map Inv.inv (ae μ)) ↔ EventuallyConst s (ae μ)
Tactic: rw [← inv_preimage, eventuallyConst_preimage, Filter.map_inv, inv_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
rw : EventuallyConst (Inv.inv ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
rw₁ : EventuallyConst s (Filter.map Inv.inv (ae μ)) ↔ EventuallyConst s (ae μ)
⊢ EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)
have rw₂ : EventuallyConst s (ae μ)⁻¹ ↔ EventuallyConst s (ae μ)
Tactic: rw [← inv_preimage, eventuallyConst_preimage, Filter.map_inv, inv_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
rw : EventuallyConst (Inv.inv ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
rw₁ : EventuallyConst s (Filter.map Inv.inv (ae μ)) ↔ EventuallyConst s (ae μ)
rw₂ : EventuallyConst s (ae μ)⁻¹ ↔ EventuallyConst s (ae μ)
⊢ EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)
have rw₃ : EventuallyConst s (ae μ) ↔ EventuallyConst s (ae μ)
Tactic: rw [← inv_preimage, eventuallyConst_preimage, Filter.map_inv, inv_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
⊢ μ ≪ μ.inv
have refine : ∀ (s : Set G),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk fun s _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
s : Set G
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [inv_apply μ s, measure_inv_null, imp_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
s : Set G
h : MeasurableSet s
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [inv_apply μ s, measure_inv_null, imp_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
have h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
Tactic: have h : Measurable fun z : G × G => (z.2 * z.1, z.1⁻¹) :=
    (measurable_snd.mul measurable_fst).prodMk measurable_fst.inv
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
have h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
Tactic: have h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν) :=
    hf.comp_quasiMeasurePreserving (measurePreserving_mul_prod_inv μ ν).quasiMeasurePreserving
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
have simp_rw : ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν
Tactic: simp_rw [lintegral_lintegral h2f, lintegral_lintegral hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
| ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν
have rw : ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)
Tactic: rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν
have conv_rhs : ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν =
  ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)
Tactic: conv_rhs => rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν =
    ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν)
have symm : ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) =
  ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
y : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (Inv.inv ⁻¹' (fun (x : G) ↦ y⁻¹ * x) ⁻¹' Inv.inv ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
y : G
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (Inv.inv ⁻¹' (fun (x : G) ↦ y⁻¹ * x) ⁻¹' Inv.inv ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ (y⁻¹ * x⁻¹)⁻¹) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
s : Set G
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
y : G
simp_rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (Inv.inv ⁻¹' (fun (x : G) ↦ y⁻¹ * x) ⁻¹' Inv.inv ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ (y⁻¹ * x⁻¹)⁻¹) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x⁻¹⁻¹ * y⁻¹⁻¹) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [← inv_preimage, preimage_preimage, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun (x : G) ↦ x * g) μ
have refine : ∀ (s : Set G) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun (h : G) ↦ g / h) μ
have simp_rw : μ ≪ map (fun (h : G) ↦ g * h⁻¹) μ
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun (h : G) ↦ g * h⁻¹) μ
have this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map ((fun (x : G) ↦ g * x) ∘ Inv.inv) μ)
Tactic: have := map_map (μ := μ) (measurable_const_mul g) measurable_inv
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
⊢ μ ≪ map (fun (h : G) ↦ g * h⁻¹) μ
have rw : μ ≪ map (fun (x : G) ↦ g * x) (map Inv.inv μ)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
| μ
have rw : map (fun (x : G) ↦ g * x) μ
Tactic: rw [← map_mul_left_eq_self μ g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ : Measure G
inst_3 : SFinite μ
inst_4 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
this : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map Inv.inv μ)) (map (fun (x : G) ↦ g * x⁻¹) μ)
⊢ μ ≪ map (fun (x : G) ↦ g * x) (map Inv.inv μ)
have conv_lhs : AbsolutelyContinuous (α := G) (_m0 := inst) (map (fun (x : G) ↦ g * x) μ) (map (fun (x : G) ↦ g * x) (map Inv.inv μ))
Tactic: conv_lhs => rw [← map_mul_left_eq_self μ g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (y : G), f y ∂ν) =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
have rw : ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun (x : G) ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
  ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
Tactic: rw [← setLIntegral_one, ← lintegral_indicator sm,
    ← lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable,
    ← lintegral_lintegral_mul_inv μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun (x : G) ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (y : G), f y ∂ν) =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
have hf₁ : AEMeasurable (β := ℝ≥0∞) (uncurry fun (x y : G) ↦ s.indicator (fun (x : G) ↦ 1) x * f y) (μ.prod ν)
Tactic: rw [← setLIntegral_one, ← lintegral_indicator sm,
    ← lintegral_lintegral_mul (measurable_const.indicator sm).aemeasurable hf.aemeasurable,
    ← lintegral_lintegral_mul_inv μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun (x : G) ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
have ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
Tactic: have ms :
    ∀ x : G, Measurable fun y => ((fun z => z * x) ⁻¹' s).indicator (fun _ => (1 : ℝ≥0∞)) y :=
    fun x => measurable_const.indicator (measurable_mul_const _ sm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y : G
⊢ Eq (α := ℝ≥0∞) (s.indicator (fun (x : G) ↦ 1) (y * x)) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y)
have symm : Eq (α := ℝ≥0∞) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y) (s.indicator (fun (x : G) ↦ 1) (y * x))
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y : G
⊢ Eq (α := ℝ≥0∞) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y) (s.indicator (fun (x : G) ↦ 1) (y * x))
have h : Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (b : G) ↦ 1) ((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x)
Tactic: convert! indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y : G
⊢ Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (b : G) ↦ 1) ((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x)
have h : ∀ (x_1 : G), Eq (α := ℝ≥0∞) 1 (((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x) x_1)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun (x : G) ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
have this : ∀ (x y : G),
  Eq (α := ℝ≥0∞) (s.indicator (fun (x : G) ↦ 1) (y * x)) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y)
Tactic: have : ∀ x y, s.indicator (fun _ : G => (1 : ℝ≥0∞)) (y * x) =
      ((fun z => z * x) ⁻¹' s).indicator (fun b : G => 1) y := by
    intro x y; symm; convert! indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2; ext1; rfl