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 : 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∞)
t : Finset G
hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₁ : Eq (α := ℝ≥0∞) (∑ g ∈ t, (μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' U)) 0
Tactic: calc
    μ K ≤ μ (⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U) := measure_mono hKt
    _ ≤ ∑ g ∈ t, μ ((fun h : G => g * h) ⁻¹' U) := measure_biUnion_finset_le _ _
    _ = 0 := by simp [measure_preimage_mul, 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
inst_6 : μ.Regular
s : Set G
hs : IsOpen[inst_1] s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = ∅ ∨ μ = 0
have inl : ∀ [IsMulLeftInvariant.{u_1} (G := G) 0] [Regular.{u_1} (α := G) 0],
  Eq (α := ℝ≥0∞) (((0 : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    s = ∅ ∨ Eq.{u_1 + 1} (α := Measure G) 0 0
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, inst_5, inst_6
-- 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
inst_6 : μ.Regular
s : Set G
hs : IsOpen[inst_1] s
inl :
  ∀ [IsMulLeftInvariant.{u_1} (G := G) 0] [Regular.{u_1} (α := G) 0],
    Eq (α := ℝ≥0∞) (((0 : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
      s = ∅ ∨ Eq.{u_1 + 1} (α := Measure G) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = ∅ ∨ μ = 0
have inr : ∀ (hμ : NeZero μ), Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s = ∅ ∨ μ = 0
Tactic: rcases eq_zero_or_neZero μ with rfl | 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
U : Set G
hU : IsOpen[inst_1] U
h'U : U.Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : ∀ (h'U : (interior U).Nonempty) (h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) {K : Set G}
  (hK : IsCompact K), LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← hU.interior_eq] at h'U
Cleared hypotheses: h'U, h, K, hK
-- 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
U : Set G
hU : IsOpen[inst_1] U
h'U : (interior U).Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
K : Set G
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have obtain : ∀ (t : Finset G) (hKt : K ⊆ ⋃ g ∈ t, (fun (h : G) ↦ g * h) ⁻¹' U),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ g ∈ t, (fun h : G => g * h) ⁻¹' U :=
    compact_covered_by_mul_left_translates hK h'U
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have obtain : ∀ (K : Set G) (K1 : Membership.mem (γ := Filter G) (𝓝 1) K) (hK : IsCompact K) (Kclosed : IsClosed[inst_1] K),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: obtain ⟨K, K1, hK, Kclosed⟩ : ∃ K ∈ 𝓝 (1 : G), IsCompact K ∧ IsClosed K :=
    exists_mem_nhds_isCompact_isClosed 1
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: have K_pos : 0 < μ K := measure_pos_of_mem_nhds μ K1
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have A : ∀ (L : Set G), IsCompact L → ∃ (g : G), Disjoint L (g • K)
Tactic: have A : ∀ L : Set G, IsCompact L → ∃ g : G, Disjoint L (g • K) := fun L hL =>
    exists_disjoint_smul_of_isCompact hL hK
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
A : ∀ (L : Set G), IsCompact L → ∃ (g : G), Disjoint L (g • K)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have choose! : ∀ (g : (L : Set G) → G) (hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: choose! g hg using A
Cleared hypotheses: A
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (L (n + 1))
have succ : IsCompact (X := G) (((fun (T : Set G) ↦ T ∪ g T • K) ∘ (fun (T : Set G) ↦ T ∪ g T • K)^[n]) K)
Tactic: simp_rw [L, iterate_succ']
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
n : ℕ
⊢ IsCompact (L n)
have zero : IsCompact (L 0)
Tactic: induction n with
    | zero => exact hK
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsCompact.union IH (hK.smul (g (L n)))
Cleared hypotheses: n
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
n : ℕ
zero : IsCompact (L 0)
⊢ IsCompact (L n)
have succ : ∀ (n : ℕ) (IH : IsCompact (L n)), IsCompact (L (n + 1))
Tactic: induction n with
    | zero => exact hK
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsCompact.union IH (hK.smul (g (L n)))
Cleared hypotheses: n
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have Lcompact : ∀ (n : ℕ), IsCompact (L n)
Tactic: have Lcompact : ∀ n, IsCompact (L n) := fun n ↦ by
    induction n with
    | zero => exact hK
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsCompact.union IH (hK.smul (g (L n)))
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed[inst_1] (L n)
⊢ IsClosed[inst_1] (L (n + 1))
have succ : IsClosed[inst_1] (((fun (T : Set G) ↦ T ∪ g T • K) ∘ (fun (T : Set G) ↦ T ∪ g T • K)^[n]) K)
Tactic: simp_rw [L, iterate_succ']
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
⊢ IsClosed[inst_1] (L n)
have zero : IsClosed[inst_1] (L 0)
Tactic: induction n with
    | zero => exact Kclosed
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsClosed.union IH (Kclosed.smul (g (L n)))
Cleared hypotheses: n
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
zero : IsClosed[inst_1] (L 0)
⊢ IsClosed[inst_1] (L n)
have succ : ∀ (n : ℕ) (IH : IsClosed[inst_1] (L n)), IsClosed[inst_1] (L (n + 1))
Tactic: induction n with
    | zero => exact Kclosed
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsClosed.union IH (Kclosed.smul (g (L n)))
Cleared hypotheses: n
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
Tactic: have Lclosed : ∀ n, IsClosed (L n) := fun n ↦ by
    induction n with
    | zero => exact Kclosed
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsClosed.union IH (Kclosed.smul (g (L n)))
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
n : ℕ
IH :
  (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ (μ : (a : Set G) → ℝ≥0∞) (L (n + 1)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (L n) : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) (g (L n) • K) : ℝ≥0∞)
have simp_rw : (μ : (a : Set G) → ℝ≥0∞) (((fun (T : Set G) ↦ T ∪ g T • K) ∘ (fun (T : Set G) ↦ T ∪ g T • K)^[n]) K) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (T : Set G) ↦ T ∪ g T • K)^[n] K) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) (g ((fun (T : Set G) ↦ T ∪ g T • K)^[n] K) • K) : ℝ≥0∞)
Tactic: simp_rw [L, iterate_succ']
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
n : ℕ
IH :
  (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ (μ : (a : Set G) → ℝ≥0∞) (L (n + 1)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1 + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
have μ₁ : (μ : (a : Set G) → ℝ≥0∞) (L (n + 1)) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (L n) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) (g (L n) • K) : ℝ≥0∞)
Tactic: calc
        μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
        _ = (n + 1 + 1 : ℕ) * μ K := by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
n : ℕ
IH :
  (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
μ₁ :
  (μ : (a : Set G) → ℝ≥0∞) (L (n + 1)) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (L n) : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) (g (L n) • K) : ℝ≥0∞)
⊢ (μ : (a : Set G) → ℝ≥0∞) (L (n + 1)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1 + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
have μ₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (L n) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) (g (L n) • K) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1 + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: calc
        μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
        _ = (n + 1 + 1 : ℕ) * μ K := by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
n : ℕ
⊢ (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
have zero : (μ : (a : Set G) → ℝ≥0∞) (L 0) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: induction n with
    | zero => simp only [L, one_mul, Nat.cast_one, iterate_zero, id, Nat.zero_add]
    | succ n IH =>
      calc
        μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
        _ = (n + 1 + 1 : ℕ) * μ K := by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]
Cleared hypotheses: n
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
n : ℕ
zero :
  (μ : (a : Set G) → ℝ≥0∞) (L 0) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
have succ : ∀ (n : ℕ)
  (IH :
    (μ : (a : Set G) → ℝ≥0∞) (L n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)),
  (μ : (a : Set G) → ℝ≥0∞) (L (n + 1)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1 + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: induction n with
    | zero => simp only [L, one_mul, Nat.cast_one, iterate_zero, id, Nat.zero_add]
    | succ n IH =>
      calc
        μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
        _ = (n + 1 + 1 : ℕ) * μ K := by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]
Cleared hypotheses: n
-- 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
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : WeaklyLocallyCompactSpace G
inst_6 : NoncompactSpace G
μ : Measure G
inst_7 : μ.IsOpenPosMeasure
inst_8 : μ.IsMulLeftInvariant
K : Set G
K1 : Membership.mem (γ := Filter G) (𝓝 1) K
hK : IsCompact K
Kclosed : IsClosed[inst_1] K
K_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : (L : Set G) → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun (n : ℕ) ↦ (fun (T : Set G) ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have M : ∀ (n : ℕ),
  (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: have M : ∀ n, μ (L n) = (n + 1 : ℕ) * μ K := fun n ↦ by
    induction n with
    | zero => simp only [L, one_mul, Nat.cast_one, iterate_zero, id, Nat.zero_add]
    | succ n IH =>
      calc
        μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
        _ = (n + 1 + 1 : ℕ) * μ K := by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]