awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h
have symm : modularCharacterFun g * modularCharacterFun h = modularCharacterFun (g * h)
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
⊢ modularCharacterFun h * modularCharacterFun g =
    haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      modularCharacterFun g
have rw : haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
    modularCharacterFun g =
  haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
    modularCharacterFun g
Tactic: rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
⊢ modularCharacterFun g * modularCharacterFun h = modularCharacterFun (g * h)
have modularCharacterFun : modularCharacterFun h * modularCharacterFun g =
  haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
    modularCharacterFun g
Tactic: calc
    modularCharacterFun g * modularCharacterFun h =
      modularCharacterFun h * modularCharacterFun g := mul_comm _ _
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      modularCharacterFun g := by
      rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      haarScalarFactor (map (· * g) ν) ν := rfl
    _ = haarScalarFactor (map (· * (g * h)) ν) ν := by simp only [map_map mul_h_meas mul_g_meas,
      comp_mul_right, ← haarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
modularCharacterFun :
  Measure.modularCharacterFun h * Measure.modularCharacterFun g =
    haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      Measure.modularCharacterFun g
⊢ Measure.modularCharacterFun g * Measure.modularCharacterFun h = Measure.modularCharacterFun (g * h)
have modularCharacterFun₁ : haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
    haarScalarFactor (map (fun (x : G) ↦ x * g) ν) ν =
  haarScalarFactor (map (fun (x : G) ↦ x * (g * h)) ν) ν
Tactic: calc
    modularCharacterFun g * modularCharacterFun h =
      modularCharacterFun h * modularCharacterFun g := mul_comm _ _
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      modularCharacterFun g := by
      rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      haarScalarFactor (map (· * g) ν) ν := rfl
    _ = haarScalarFactor (map (· * (g * h)) ν) ν := by simp only [map_map mul_h_meas mul_g_meas,
      comp_mul_right, ← haarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Pointwise (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet (a • s)
have rw : MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)
Tactic: rw [← preimage_smul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Pointwise (goal)
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : MulAction G₀ α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
have rw : MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)
Tactic: rw [← preimage_smul_inv₀ ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Pointwise (goal)
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero α
inst_2 : MulActionWithZero G₀ α
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G₀ α
inst_5 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
⊢ MeasurableSet (a • s)
have inl : MeasurableSet (HSMul.hSMul.{u_1, u_2, u_2} (α := G₀) 0 s)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Pointwise (goal)
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero α
inst_2 : MulActionWithZero G₀ α
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G₀ α
inst_5 : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
inl : MeasurableSet (HSMul.hSMul.{u_1, u_2, u_2} (α := G₀) 0 s)
⊢ MeasurableSet (a • s)
have inr : ∀ (ha : a ≠ 0), MeasurableSet (a • s)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- 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
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
⊢ Measurable (β := ℝ≥0∞) fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)
have h : Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)) fun (y : G) ↦
  (μ : (a : Set G) → ℝ≥0∞)
    (preimage (β := G × G) (fun (x : G) ↦ (x, y))
      ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
Tactic: convert! this using 1
-- 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
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
⊢ Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
have h : ∀ (x : G),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞)
        (preimage (β := G × G) (fun (x_1 : G) ↦ (x_1, x))
          ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s)) :
      ℝ≥0∞)
Tactic: ext1 x
-- 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
hs : MeasurableSet s
this :
  Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
x : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞)
        (preimage (β := G × G) (fun (x_1 : G) ↦ (x_1, x))
          ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s)) :
      ℝ≥0∞)
have h : ∀ (y : G),
  Membership.mem (γ := Set G) ((fun (y : G) ↦ y * x) ⁻¹' s) y ↔
    Membership.mem (γ := Set G)
      (preimage (β := G × G) (fun (x_1 : G) ↦ (x_1, x))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
      y
Tactic: congr 1 with y : 1
-- 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
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (x : G) ↦ (μ : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s)
have Measurable : Measurable (β := ℝ≥0∞) fun (y : G) ↦
  (μ : (a : Set G) → ℝ≥0∞)
    (preimage (β := G × G) (fun (x : G) ↦ (x, y))
      ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
Tactic: suffices
    Measurable fun y =>
      μ ((fun x => (x, y)) ⁻¹' ((fun z : G × G => ((1 : G), z.1 * z.2)) ⁻¹' univ ×ˢ s))
    by convert! this using 1; ext1 x; congr 1 with y : 1; simp
-- 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
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (y : G) ↦
    (μ : (a : Set G) → ℝ≥0∞)
      (preimage (β := G × G) (fun (x : G) ↦ (x, y))
        ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s))
have hs₁ : MeasurableSet (α := G × G) ((fun (z : G × G) ↦ (1, z.1 * z.2)) ⁻¹' SProd.sprod (α := Set G) univ s)
Tactic: apply measurable_measure_prodMk_right
-- 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
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
have h : Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹))
  ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1))
Tactic: convert!
    (measurePreserving_prod_inv_mul_swap ν μ).comp (measurePreserving_prod_mul_swap μ ν) using 1
-- 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
⊢ Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹))
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1))
have h : ∀ (x y : G),
  ((x, y).2 * (x, y).1, (x, y).1⁻¹) =
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
Tactic: ext1 ⟨x, y⟩
-- 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
x y : G
⊢ ((x, y).2 * (x, y).1, (x, y).1⁻¹) =
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
have h : (y * x, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
Tactic: simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]
-- 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
x y : G
h h₁ : (y * x, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
⊢ ((x, y).2 * (x, y).1, (x, y).1⁻¹) =
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
have h₂ : (y * x, x⁻¹) = (y * x, (y * x)⁻¹ * y)
Tactic: simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]
-- 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
x y : G
h h₁ : (y * x, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
h₂ : (y * x, x⁻¹) = (y * x, (y * x)⁻¹ * y)
⊢ ((x, y).2 * (x, y).1, (x, y).1⁻¹) =
    ((fun (z : G × G) ↦ (z.2, z.2⁻¹ * z.1)) ∘ fun (z : G × G) ↦ (z.2, z.2 * z.1)) (x, y)
have h₃ : (y * x, x⁻¹) = (y * x, x⁻¹ * y⁻¹ * y)
Tactic: simp_rw [Function.comp_apply, mul_inv_rev, inv_mul_cancel_right]
-- 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
⊢ QuasiMeasurePreserving Inv.inv μ μ
have refine : ∀ (s : Set G) (hsm : MeasurableSet s) (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) (((map Inv.inv μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨measurable_inv, AbsolutelyContinuous.mk fun s hsm hμ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
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map Inv.inv μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [map_apply measurable_inv hsm, inv_preimage]
-- 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
s : Set G
hsm : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
have hf : Measurable (β := G × G) fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)
Tactic: have hf : 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 (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⁻¹)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
have suffices : 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∞)
Tactic: suffices map (fun z : G × G => (z.2 * z.1, z.1⁻¹)) (μ.prod μ) (s⁻¹ ×ˢ s⁻¹) = 0 by
    simpa only [(measurePreserving_mul_prod_inv μ μ).map_eq, prod_prod, mul_eq_zero (M₀ := ℝ≥0∞),
      or_self_iff] using this
-- 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
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⁻¹)
⊢ 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 hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
Tactic: have hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹) := hsm.inv.prod hsm.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
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⁻¹)
⊢ 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 : Eq (α := ℝ≥0∞) ((μ.prod μ : (a : Set (G × G)) → ℝ≥0∞) ((fun (z : G × G) ↦ (z.2 * z.1, z.1⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) : ℝ≥0∞)
  (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 μ
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∞)
⊢ 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),
    (μ : (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
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 μ
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
⊢ 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), (μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ (y * x, x⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) ∂μ = 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 μ
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
⊢ 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), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ Inv.inv ⁻¹' s⁻¹) ∂μ = 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 μ
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
⊢ 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), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ s⁻¹⁻¹) ∂μ = 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 μ
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
⊢ 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), (μ : (a : Set G) → ℝ≥0∞) (HMul.hMul y ⁻¹' s⁻¹ ∩ s) ∂μ = 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]