awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [map_apply (measurable_mul_const g) hA]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
⊢ (μ.prod ν).IsMulLeftInvariant
have map_mul_left_eq_self : ∀ (g : G × H), map (fun (x : G × H) ↦ g * x) (μ.prod ν) = μ.prod ν
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
g : G
h : H
⊢ map (fun (x : G × H) ↦ (g, h) * x) (μ.prod ν) = μ.prod ν
have map_mul_left_eq_self : map (Prod.map (fun (x : G) ↦ g * x) fun (x : H) ↦ h * x) (μ.prod ν) = μ.prod ν
Tactic: change map (Prod.map (g * ·) (h * ·)) (μ.prod ν) = μ.prod ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
g : G
h : H
⊢ map (Prod.map (fun (x : G) ↦ g * x) fun (x : H) ↦ h * x) (μ.prod ν) = μ.prod ν
have map_mul_left_eq_self : Measure.prod (map (fun (x : G) ↦ g * x) μ) (map (fun (x : H) ↦ h * x) ν) = μ.prod ν
Tactic: rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),
    map_mul_left_eq_self μ g, map_mul_left_eq_self ν h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_left_eq_self : Measure.prod (map (fun (x : G) ↦ g * x) μ) (map (fun (x : H) ↦ h * x) ν) = μ.prod ν
⊢ map (Prod.map (fun (x : G) ↦ g * x) fun (x : H) ↦ h * x) (μ.prod ν) = μ.prod ν
have map_mul_left_eq_self₁ : μ.prod (map (fun (x : H) ↦ h * x) ν) = μ.prod ν
Tactic: rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),
    map_mul_left_eq_self μ g, map_mul_left_eq_self ν h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_left_eq_self : Measure.prod (map (fun (x : G) ↦ g * x) μ) (map (fun (x : H) ↦ h * x) ν) = μ.prod ν
map_mul_left_eq_self₁ : μ.prod (map (fun (x : H) ↦ h * x) ν) = μ.prod ν
⊢ map (Prod.map (fun (x : G) ↦ g * x) fun (x : H) ↦ h * x) (μ.prod ν) = μ.prod ν
have map_mul_left_eq_self₂ : μ.prod ν = μ.prod ν
Tactic: rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),
    map_mul_left_eq_self μ g, map_mul_left_eq_self ν h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
⊢ (μ.prod ν).IsMulRightInvariant
have map_mul_right_eq_self : ∀ (g : G × H), map (fun (x : G × H) ↦ x * g) (μ.prod ν) = μ.prod ν
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
g : G
h : H
⊢ map (fun (x : G × H) ↦ x * (g, h)) (μ.prod ν) = μ.prod ν
have map_mul_right_eq_self : map (Prod.map (fun (x : G) ↦ x * g) fun (x : H) ↦ x * h) (μ.prod ν) = μ.prod ν
Tactic: change map (Prod.map (· * g) (· * h)) (μ.prod ν) = μ.prod ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
g : G
h : H
⊢ map (Prod.map (fun (x : G) ↦ x * g) fun (x : H) ↦ x * h) (μ.prod ν) = μ.prod ν
have map_mul_right_eq_self : Measure.prod (map (fun (x : G) ↦ x * g) μ) (map (fun (x : H) ↦ x * h) ν) = μ.prod ν
Tactic: rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h),
    map_mul_right_eq_self μ g, map_mul_right_eq_self ν h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_right_eq_self : Measure.prod (map (fun (x : G) ↦ x * g) μ) (map (fun (x : H) ↦ x * h) ν) = μ.prod ν
⊢ map (Prod.map (fun (x : G) ↦ x * g) fun (x : H) ↦ x * h) (μ.prod ν) = μ.prod ν
have map_mul_right_eq_self₁ : μ.prod (map (fun (x : H) ↦ x * h) ν) = μ.prod ν
Tactic: rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h),
    map_mul_right_eq_self μ g, map_mul_right_eq_self ν h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_right_eq_self : Measure.prod (map (fun (x : G) ↦ x * g) μ) (map (fun (x : H) ↦ x * h) ν) = μ.prod ν
map_mul_right_eq_self₁ : μ.prod (map (fun (x : H) ↦ x * h) ν) = μ.prod ν
⊢ map (Prod.map (fun (x : G) ↦ x * g) fun (x : H) ↦ x * h) (μ.prod ν) = μ.prod ν
have map_mul_right_eq_self₂ : μ.prod ν = μ.prod ν
Tactic: rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h),
    map_mul_right_eq_self μ g, map_mul_right_eq_self ν h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ IsMulLeftInvariant.{u_3} (G := H) (Measure.map (⇑f : (a : G) → H) μ)
have refine : ∀ (h : H),
  Eq.{u_3 + 1} (α := Measure H) (Measure.map (fun (x : H) ↦ h * x) (Measure.map (⇑f : (a : G) → H) μ))
    (Measure.map (⇑f : (a : G) → H) μ)
Tactic: refine ⟨fun h => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : H
⊢ Eq.{u_3 + 1} (α := Measure H) (Measure.map (fun (x : H) ↦ h * x) (Measure.map (⇑f : (a : G) → H) μ))
    (Measure.map (⇑f : (a : G) → H) μ)
have rw : Eq.{u_3 + 1} (α := Measure H) (Measure.map ((fun (x : H) ↦ h * x) ∘ (⇑f : (a : G) → H)) μ)
  (Measure.map (⇑f : (a : G) → H) μ)
Tactic: rw [map_map (measurable_const_mul _) hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : H
⊢ Eq.{u_3 + 1} (α := Measure H) (Measure.map ((fun (x : H) ↦ h * x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (⇑f : (a : G) → H) μ)
have obtain : ∀ (g : G),
  Eq.{u_3 + 1} (α := Measure H)
    (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (⇑f : (a : G) → H) μ)
Tactic: obtain ⟨g, rfl⟩ := h_surj h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
| Measure.map (⇑f : (a : G) → H) μ
have rw : Measure.map (α := G) (⇑f : (a : G) → H) (Measure.map (fun (x : G) ↦ g * x) μ)
Tactic: rw [← map_mul_left_eq_self μ g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
⊢ Eq.{u_3 + 1} (α := Measure H)
    (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (⇑f : (a : G) → H) μ)
have conv_rhs : Eq.{u_3 + 1} (α := Measure H)
  (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
  (Measure.map (α := G) (⇑f : (a : G) → H) (Measure.map (fun (x : G) ↦ g * x) μ))
Tactic: conv_rhs => rw [← map_mul_left_eq_self μ g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
⊢ Eq.{u_3 + 1} (α := Measure H)
    (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (α := G) (⇑f : (a : G) → H) (Measure.map (fun (x : G) ↦ g * x) μ))
have rw : Eq.{u_3 + 1} (α := Measure H)
  (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
  (Measure.map (comp (β := G) (⇑f : (a : G) → H) fun (x : G) ↦ g * x) μ)
Tactic: rw [map_map hf (measurable_const_mul _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
⊢ Eq.{u_3 + 1} (α := Measure H)
    (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (comp (β := G) (⇑f : (a : G) → H) fun (x : G) ↦ g * x) μ)
have e_f : Eq (α := G → H) ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H))
  (comp (β := G) (⇑f : (a : G) → H) fun (x : G) ↦ g * x)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
⊢ Eq (α := G → H) ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H))
    (comp (β := G) (⇑f : (a : G) → H) fun (x : G) ↦ g * x)
have e_f : ∀ (y : G),
  Eq.{u_3 + 1} (α := H) (((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) y)
    (comp (β := G) (⇑f : (a : G) → H) (fun (x : G) ↦ g * x) y)
Tactic: ext y
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivInvMonoid G
μ : Measure G
inst_2 : μ.IsMulRightInvariant
g : G
⊢ Measure.map (fun (x : G) ↦ x / g) μ = μ
have simp_rw : Measure.map (fun (x : G) ↦ x * g⁻¹) μ = μ
Tactic: simp_rw [div_eq_mul_inv, map_mul_right_eq_self μ g⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun (x : G) ↦ x / g) μ μ
have simp_rw : MeasurePreserving (fun (x : G) ↦ x * g⁻¹) μ μ
Tactic: simp_rw [div_eq_mul_inv, measurePreserving_mul_right μ g⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
g : G
A : Set G
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (h : G) ↦ g * h) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [map_mul_left_eq_self μ g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
g : G
A : Set G
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (h : G) ↦ h * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [map_mul_right_eq_self μ g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
t : G
p : G → Prop
| ∀ᵐ (x : G) ∂μ, p x
have rw : Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ t * h) (ae μ)) {x : G | p x}
Tactic: rw [Filter.Eventually, ← map_mul_left_ae μ t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x
have conv_rhs : (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ t * h) (ae μ)) {x : G | p x}
Tactic: conv_rhs => rw [Filter.Eventually, ← map_mul_left_ae μ t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
| ∀ᵐ (x : G) ∂μ, p x
have rw : Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ h * t) (ae μ)) {x : G | p x}
Tactic: rw [Filter.Eventually, ← map_mul_right_ae μ t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x
have conv_rhs : (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ h * t) (ae μ)) {x : G | p x}
Tactic: conv_rhs => rw [Filter.Eventually, ← map_mul_right_ae μ t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
| ∀ᵐ (x : G) ∂μ, p x
have rw : Membership.mem (γ := Filter G) (Filter.map (fun (t_1 : G) ↦ t_1 / t) (ae μ)) {x : G | p x}
Tactic: rw [Filter.Eventually, ← map_div_right_ae μ t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x
have conv_rhs : (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ Membership.mem (γ := Filter G) (Filter.map (fun (t_1 : G) ↦ t_1 / t) (ae μ)) {x : G | p x}
Tactic: conv_rhs => rw [Filter.Eventually, ← map_div_right_ae μ t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
have obtain : ∀ (s : Set G) (hs : Subgroup.IsComplement s (↑H : Set G)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
Tactic: obtain ⟨s, hs, -⟩ := H.exists_isComplement_left 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (hypothesis)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
have hs' : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have hs' : Finite s := hs.finite_left_iff.mpr inferInstance
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Eq (α := ℝ≥0∞) (∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G)) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (⋃ (i : (↑s : Type u_1)), (↑i : G) • (↑H : Set G)) : ℝ≥0∞)
  ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (⋃ (i : (↑s : Type u_1)), (↑i : G) • (↑H : Set G)) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G)) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : Pairwise.{u_1} (α := (↑s : Type u_1)) (onFun (β := Set G) Disjoint fun (x : (↑s : Type u_1)) ↦ (↑x : G) • (↑H : Set G))
Tactic: rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
have μ₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
  ∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G))
Tactic: calc
    H.index * μ H = ∑' a : s, μ (a.val • H) := by simp [measure_smul, hs.encard_left]
    _ = μ univ := by
      rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
      · simp [hs.mul_eq]
      · exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
μ₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    ∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G))
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
have μ₂ : Eq (α := ℝ≥0∞) (∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G)) : ℝ≥0∞)
  ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: calc
    H.index * μ H = ∑' a : s, μ (a.val • H) := by simp [measure_smul, hs.encard_left]
    _ = μ univ := by
      rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
      · simp [hs.mul_eq]
      · exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : InvolutiveInv G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsInvInvariant
A : Set G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [← inv_apply, inv_eq_self]