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 : 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.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
have h : ∀ (x : H),
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x
Tactic: ext
-- 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
x : H
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x
have h : Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x →
  Membership.mem (γ := Set H)
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x
Tactic: constructor
-- 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
x : H
h :
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x →
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x
have h₁ : Membership.mem (γ := Set H)
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s)) x →
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s)) x
Tactic: constructor
-- 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 : 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∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
have this : Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
  (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
Tactic: have : f '' (g * ·) ⁻¹' s = (f g * ·) ⁻¹' f '' s := by
      ext
      constructor
      · rintro ⟨y, hy, rfl⟩
        exact ⟨g * y, hy, by simp⟩
      · intro ⟨y, yins, hy⟩
        exact ⟨g⁻¹ * y, by simp [yins], by simp [hy]⟩
-- 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
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ g * x) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ((⇑f : (a : G) → H) '' s))
⊢ 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∞)
have h : MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)
Tactic: rw [this, ← map_apply (by fun_prop), IsMulLeftInvariant.map_mul_left_eq_self]
-- 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 : μ.IsMulRightInvariant
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) ↦ x * g) (comap (⇑f : (a : G) → H) μ)) (comap (⇑f : (a : G) → H) μ)
have h : ∀ (s : Set G) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((map (fun (x : G) ↦ x * g) (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 : μ.IsMulRightInvariant
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) ↦ x * g) (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) ↦ x * g) ⁻¹' 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 : μ.IsMulRightInvariant
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) ↦ x * g) ⁻¹' 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) ↦ x * g) ⁻¹' 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 : μ.IsMulRightInvariant
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) ↦ x * g) ⁻¹' 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) ↦ x * g) ⁻¹' 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 : μ.IsMulRightInvariant
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) ↦ x * g) ⁻¹' 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) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
  ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
Tactic: repeat 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 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
have h : ∀ (x : H),
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x
Tactic: ext
-- 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 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x
have h : Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x →
  Membership.mem (γ := Set H)
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x
Tactic: constructor
-- 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 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
h :
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x →
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x
have h₁ : Membership.mem (γ := Set H)
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x →
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x
Tactic: constructor
-- 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 : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
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) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
have this : Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
  (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
Tactic: have : f '' (· * g) ⁻¹' s = (· * f g) ⁻¹' f '' s := by
      ext
      constructor
      · rintro ⟨y, hy, rfl⟩
        exact ⟨y * g, hy, by simp⟩
      · intro ⟨y, yins, hy⟩
        exact ⟨y * g⁻¹, by simp [yins], by simp [hy]⟩
-- 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 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
have h : MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)
Tactic: rw [this, ← map_apply (by fun_prop), IsMulRightInvariant.map_mul_right_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 : Group G
μ : Measure G
inst_3 : MeasurableInv G
⊢ Eq.{u_1 + 1} (α := Measure G) (Measure.inv count) count
have h : ∀ (s : Set G) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.inv 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 : MeasurableInv G
s : Set G
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have h : ((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, inv_apply, count_apply hs.inv, encard_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 : MeasurableInv G
s : Set G
hs : MeasurableSet s
h : ((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.inv 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∞) s⁻¹ = (↑s.encard : ℝ≥0∞)
Tactic: rw [count_apply hs, inv_apply, count_apply hs.inv, encard_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 : MeasurableInv G
s : Set G
hs : MeasurableSet s
h : ((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) s⁻¹ = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.inv 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, inv_apply, count_apply hs.inv, encard_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 : MeasurableInv G
s : Set G
hs : MeasurableSet s
h : ((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) s⁻¹ = (↑s.encard : ℝ≥0∞)
h₂ : (↑s⁻¹.encard : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.inv 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, inv_apply, count_apply hs.inv, encard_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
have obtain : ∀ (U : Set G) (hUk : k ⊆ U) (hU : IsOpen[inst_1] U)
  (hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε),
  ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
Tactic: obtain ⟨U, hUk, hU, hμUk⟩ : ∃ (U : Set G), k ⊆ U ∧ IsOpen U ∧ μ U < μ k + ε :=
    hk.exists_isOpen_lt_add hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
⊢ ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
have obtain : ∀ (V : Set G) (hV1 : Membership.mem (γ := Filter G) (𝓝 1) V) (hVkU : V * k ⊆ U),
  ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
Tactic: obtain ⟨V, hV1, hVkU⟩ : ∃ V ∈ 𝓝 (1 : G), V * k ⊆ U := compact_open_separated_mul_left hk hU hUk
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
⊢ ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
have h : ∀ (g : G) (hg : g ∈ V), (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
Tactic: filter_upwards [hV1] with g hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • k \ k) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (U \ k) : ℝ≥0∞)
have h : g • k ⊆ U
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • k \ k) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (U \ k) : ℝ≥0∞)
Tactic: calc
    μ (g • k \ k) ≤ μ (U \ k) := by
      gcongr
      exact (smul_set_subset_smul hg).trans hVkU
    _ < ε := measure_diff_lt_of_lt_add h'k.nullMeasurableSet hUk hk.measure_lt_top.ne hμUk
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.IsOpenPosMeasure
have refine : ∀ (U : Set G) (hU : IsOpen[inst_1] U) (hne : U.Nonempty), Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨fun U hU hne => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set G
hU : IsOpen[inst_1] U
hne : U.Nonempty
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
have contrapose : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : U.Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (hypothesis)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : U.Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
have hne₁ : (interior U).Nonempty
Tactic: rw [← hU.interior_eq] at hne
Cleared hypotheses: hne, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (goal)
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
U : Set G
hU : IsOpen[inst_1] U
hne : (interior U).Nonempty
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (t : Finset G) (hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U :=
    compact_covered_by_mul_left_translates hK hne