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 : InvolutiveInv G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsInvInvariant
A : Set G
rw : Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (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 [← inv_apply, inv_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
⊢ μ.inv.IsMulRightInvariant
have map_mul_right_eq_self : ∀ (g : G), map (fun (x : G) ↦ x * g) μ.inv = μ.inv
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
| μ.inv
have rw : Measure.inv (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
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ map (fun (x : G) ↦ x * g) μ.inv = μ.inv
have map_mul_right_eq_self : Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (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
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
have map_mul_right_eq_self : Eq (α := Measure G) (map (fun (x : G) ↦ x * g) (map inv μ)) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
Tactic: simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
map_mul_right_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ x * g) (map inv μ)) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
have map_mul_right_eq_self₁ : Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
Tactic: simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
map_mul_right_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ x * g) (map inv μ)) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
map_mul_right_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
have map_mul_right_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ g⁻¹ * x) μ)
Tactic: simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
map_mul_right_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ x * g) (map inv μ)) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
map_mul_right_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
map_mul_right_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ g⁻¹ * x) μ)
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
have map_mul_right_eq_self₃ : Eq (α := Measure G) (map (fun (x : G) ↦ x⁻¹ * g) μ) (map (fun (x : G) ↦ (g⁻¹ * x)⁻¹) μ)
Tactic: simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
map_mul_right_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ x * g) (map inv μ)) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
map_mul_right_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
map_mul_right_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ g⁻¹ * x) μ)
map_mul_right_eq_self₃ : Eq (α := Measure G) (map (fun (x : G) ↦ x⁻¹ * g) μ) (map (fun (x : G) ↦ (g⁻¹ * x)⁻¹) μ)
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
have map_mul_right_eq_self₄ : Eq (α := Measure G) (map (fun (x : G) ↦ x⁻¹ * g) μ) (map (fun (x : G) ↦ x⁻¹ * g⁻¹⁻¹) μ)
Tactic: simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
⊢ μ.inv.IsMulLeftInvariant
have map_mul_left_eq_self : ∀ (g : G), map (fun (x : G) ↦ g * x) μ.inv = μ.inv
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
| μ.inv
have rw : Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ)
Tactic: rw [← map_mul_right_eq_self μ g⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
⊢ map (fun (x : G) ↦ g * x) μ.inv = μ.inv
have map_mul_left_eq_self : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))
Tactic: conv_rhs => rw [← map_mul_right_eq_self μ g⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))
have map_mul_left_eq_self : Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map inv μ)) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
Tactic: simp_rw [Measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
map_mul_left_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map inv μ)) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))
have map_mul_left_eq_self₁ : Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
Tactic: simp_rw [Measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
map_mul_left_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map inv μ)) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
map_mul_left_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))
have map_mul_left_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ x * g⁻¹) μ)
Tactic: simp_rw [Measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
map_mul_left_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map inv μ)) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
map_mul_left_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
map_mul_left_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ x * g⁻¹) μ)
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))
have map_mul_left_eq_self₃ : Eq (α := Measure G) (map (fun (x : G) ↦ g * x⁻¹) μ) (map (fun (x : G) ↦ (x * g⁻¹)⁻¹) μ)
Tactic: simp_rw [Measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulRightInvariant
g : G
map_mul_left_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ g * x) (map inv μ)) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
map_mul_left_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map inv (map (fun (x : G) ↦ x * g⁻¹) μ))
map_mul_left_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ g * x) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ x * g⁻¹) μ)
map_mul_left_eq_self₃ : Eq (α := Measure G) (map (fun (x : G) ↦ g * x⁻¹) μ) (map (fun (x : G) ↦ (x * g⁻¹)⁻¹) μ)
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ g * x) μ.inv) (Measure.inv (map (fun (x : G) ↦ x * g⁻¹) μ))
have map_mul_left_eq_self₄ : Eq (α := Measure G) (map (fun (x : G) ↦ g * x⁻¹) μ) (map (fun (x : G) ↦ g⁻¹⁻¹ * x⁻¹) μ)
Tactic: simp_rw [Measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivisionMonoid G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : μ.IsInvInvariant
inst_5 : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun (t : G) ↦ g / t) μ μ
have simp_rw : MeasurePreserving (fun (t : G) ↦ g * t⁻¹) μ μ
Tactic: simp_rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
⊢ Eq.{u_1 + 1} (α := Measure G) (map (fun (x : G) ↦ g * x) count) count
have h : ∀ (s : Set G) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : ((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_const_mul _) hs,
      count_apply (measurable_const_mul _ hs),
      encard_preimage_of_bijective (Group.mulLeft_bijective _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_const_mul _) hs,
      count_apply (measurable_const_mul _ hs),
      encard_preimage_of_bijective (Group.mulLeft_bijective _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : (↑(encard (α := G) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_const_mul _) hs,
      count_apply (measurable_const_mul _ hs),
      encard_preimage_of_bijective (Group.mulLeft_bijective _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
h₂ : (↑(encard (α := G) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : (↑s.encard : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_const_mul _) hs,
      count_apply (measurable_const_mul _ hs),
      encard_preimage_of_bijective (Group.mulLeft_bijective _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
⊢ Eq.{u_1 + 1} (α := Measure G) (map (fun (x : G) ↦ x * g) count) count
have h : ∀ (s : Set G) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : ((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_mul_const _) hs,
      count_apply (measurable_mul_const _ hs),
      encard_preimage_of_bijective (Group.mulRight_bijective _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_mul_const _) hs,
      count_apply (measurable_mul_const _ hs),
      encard_preimage_of_bijective (Group.mulRight_bijective _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : (↑(encard (α := G) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_mul_const _) hs,
      count_apply (measurable_mul_const _ hs),
      encard_preimage_of_bijective (Group.mulRight_bijective _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
h : ((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' s) = (↑s.encard : ℝ≥0∞)
h₂ : (↑(encard (α := G) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : (↑s.encard : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, map_apply (measurable_mul_const _) hs,
      count_apply (measurable_mul_const _ hs),
      encard_preimage_of_bijective (Group.mulRight_bijective _)]
-- 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 : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
⊢ Eq.{u_1 + 1} (α := Measure G) (map (fun (x : G) ↦ g * x) (comap (⇑f : (a : G) → H) μ)) (comap (⇑f : (a : G) → H) μ)
have h : ∀ (s : Set G) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) (comap (⇑f : (a : G) → H) μ) : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- 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 : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ g * x) (comap (⇑f : (a : G) → H) μ) : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) : ℝ≥0∞)
  (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply (by fun_prop) hs]
-- 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 : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
  (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [hf.comap_apply]
-- 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 : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
  ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
Tactic: rw [hf.comap_apply]
-- 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 : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) : ℝ≥0∞)
  ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
Tactic: repeat rw [hf.comap_apply]