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
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)
M :
  ∀ (n : ℕ),
    (μ : (a : Set G) → ℝ≥0∞) (L n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ (μ : (a : Set G) → ℝ≥0∞) (L n)) atTop
    (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)))
have simp_rw : Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞))
  atTop (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)))
Tactic: simp_rw [M]
-- 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)
M :
  ∀ (n : ℕ),
    (μ : (a : Set G) → ℝ≥0∞) (L n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Tendsto
    (fun (n : ℕ) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞))
    atTop (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)))
have apply : Tendsto (β := ℝ≥0∞) (fun (x : ℕ) ↦ (↑(x + 1) : ℝ≥0∞)) atTop (𝓝 ∞)
Tactic: apply ENNReal.Tendsto.mul_const _ (Or.inl ENNReal.top_ne_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
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)
M :
  ∀ (n : ℕ),
    (μ : (a : Set G) → ℝ≥0∞) (L n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have N : Tendsto (fun (n : ℕ) ↦ (μ : (a : Set G) → ℝ≥0∞) (L n)) atTop
  (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)))
Tactic: have N : Tendsto (fun n => μ (L n)) atTop (𝓝 (∞ * μ K)) := by
    simp_rw [M]
    apply ENNReal.Tendsto.mul_const _ (Or.inl ENNReal.top_ne_zero)
    exact ENNReal.tendsto_nat_nhds_top.comp (tendsto_add_atTop_nat _)
-- 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)
M :
  ∀ (n : ℕ),
    (μ : (a : Set G) → ℝ≥0∞) (L n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
N :
  Tendsto (fun (n : ℕ) ↦ (μ : (a : Set G) → ℝ≥0∞) (L n)) atTop
    (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have N₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set G) → ℝ≥0∞) (L n)) atTop (𝓝 ∞)
Tactic: simp only [ENNReal.top_mul', K_pos.ne', if_false] at 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)
Lclosed : ∀ (n : ℕ), IsClosed[inst_1] (L n)
M :
  ∀ (n : ℕ),
    (μ : (a : Set G) → ℝ≥0∞) (L n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
N : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set G) → ℝ≥0∞) (L n)) atTop (𝓝 ∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: apply top_le_iff.1
-- 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
s : Set G
f : ℕ → Set G
h : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), f i * closure[inst_1] {1} = f i
⊢ HMul.hMul (α := Set G) (⋃ (i : ℕ), f i) (closure[inst_1] {1}) = ⋃ (i : ℕ), f i
have iUnion : Eq.{u_1 + 1} (α := Set G) (⋃ (i : ℕ), f i * closure[inst_1] {1}) (⋃ (i : ℕ), f i)
Tactic: simp_rw [iUnion_mul f, ihf]
-- 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
s : Set G
hs : MeasurableSet s
⊢ s * closure[inst_1] {1} = s
have isOpen : ∀ (U : Set G) (hU : IsOpen[inst_1] U), U * closure[inst_1] {1} = U
Tactic: induction s, hs using MeasurableSet.induction_on_open with
  | isOpen U hU => exact hU.mul_closure_one_eq
  | compl t _ iht => exact compl_mul_closure_one_eq_iff.2 iht
  | iUnion f _ _ ihf => simp_rw [iUnion_mul f, ihf]
Cleared hypotheses: hs
-- 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
s : Set G
hs : MeasurableSet s
isOpen : ∀ (U : Set G) (hU : IsOpen[inst_1] U), U * closure[inst_1] {1} = U
⊢ s * closure[inst_1] {1} = s
have compl : ∀ (t : Set G), MeasurableSet t → ∀ (iht : t * closure[inst_1] {1} = t), tᶜ * closure[inst_1] {1} = tᶜ
Tactic: induction s, hs using MeasurableSet.induction_on_open with
  | isOpen U hU => exact hU.mul_closure_one_eq
  | compl t _ iht => exact compl_mul_closure_one_eq_iff.2 iht
  | iUnion f _ _ ihf => simp_rw [iUnion_mul f, ihf]
Cleared hypotheses: hs
-- 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
s : Set G
hs : MeasurableSet s
isOpen : ∀ (U : Set G) (hU : IsOpen[inst_1] U), U * closure[inst_1] {1} = U
compl : ∀ (t : Set G), MeasurableSet t → ∀ (iht : t * closure[inst_1] {1} = t), tᶜ * closure[inst_1] {1} = tᶜ
⊢ s * closure[inst_1] {1} = s
have iUnion : ∀ (f : ℕ → Set G),
  Pairwise (Disjoint on f) →
    (∀ (i : ℕ), MeasurableSet (f i)) →
      ∀ (ihf : ∀ (i : ℕ), f i * closure[inst_1] {1} = f i),
        HMul.hMul (α := Set G) (⋃ (i : ℕ), f i) (closure[inst_1] {1}) = ⋃ (i : ℕ), f i
Tactic: induction s, hs using MeasurableSet.induction_on_open with
  | isOpen U hU => exact hU.mul_closure_one_eq
  | compl t _ iht => exact compl_mul_closure_one_eq_iff.2 iht
  | iUnion f _ _ ihf => simp_rw [iUnion_mul f, ihf]
Cleared hypotheses: hs
-- 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
s : Set G
μ : Measure G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm ?_ (measure_mono (subset_mul_closure_one s))
-- 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
s : Set G
μ : Measure G
| ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ⨅ (t : Set G), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set G) → ℝ≥0∞) t
Tactic: rw [measure_eq_iInf]
-- 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
s : Set G
μ : Measure G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
have conv_rhs : LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞)
  (⨅ (t : Set G), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: conv_rhs => rw [measure_eq_iInf]
-- 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
s : Set G
μ : Measure G
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞)
    (⨅ (t : Set G), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have simp : ∀ (i : Set G) (i_1 : s ⊆ i) (i_2 : MeasurableSet i),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: simp only [le_iInf_iff]
-- 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
s : Set G
μ : Measure G
t : Set G
kt : s ⊆ t
t_meas : MeasurableSet t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have h : s * closure[inst_1] {1} ⊆ t
Tactic: apply measure_mono
-- 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
s : Set G
μ : Measure G
t : Set G
kt : s ⊆ t
t_meas : MeasurableSet t
⊢ s * closure[inst_1] {1} ⊆ t
have h : s * closure[inst_1] {1} ⊆ t * closure[inst_1] {1}
Tactic: rw [← t_meas.mul_closure_one_eq]
-- 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
h : μ.InnerRegularCompactLTTop
s : Set G
⊢ (fun (s : Set G) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) s →
    ∀ r < (μ : (a : Set G) → ℝ≥0∞) s,
      ∃ K ⊆ s, (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K ∧ r < (μ : (a : Set G) → ℝ≥0∞) K
have this : ∀ (s_meas : MeasurableSet s) (μs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∀ r < (μ : (a : Set G) → ℝ≥0∞) s,
    ∃ K ⊆ s, (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K ∧ r < (μ : (a : Set G) → ℝ≥0∞) K
Tactic: ⟨s_meas, μs⟩
-- 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
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K ∧ r < (μ : (a : Set G) → ℝ≥0∞) K
have rcases : ∀ (K : Set G) (Ks : K ⊆ s) (K_comp : IsCompact K) (hK : r < (μ : (a : Set G) → ℝ≥0∞) K),
  ∃ K ⊆ s, (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K ∧ r < (μ : (a : Set G) → ℝ≥0∞) K
Tactic: rcases h.innerRegular ⟨s_meas, μs⟩ r hr with ⟨K, Ks, K_comp, 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
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) s
K : Set G
Ks : K ⊆ s
K_comp : IsCompact K
hK : r < (μ : (a : Set G) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K ∧ r < (μ : (a : Set G) → ℝ≥0∞) K
have refine_1 : closure[inst_1] K ⊆ s
Tactic: refine ⟨closure K, ?_, ⟨K_comp.closure, isClosed_closure⟩, ?_⟩
-- 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
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) s
K : Set G
Ks : K ⊆ s
K_comp : IsCompact K
hK : r < (μ : (a : Set G) → ℝ≥0∞) K
refine_1 : closure[inst_1] K ⊆ s
⊢ ∃ K ⊆ s, (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K ∧ r < (μ : (a : Set G) → ℝ≥0∞) K
have refine_2 : r < (μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] K)
Tactic: refine ⟨closure K, ?_, ⟨K_comp.closure, isClosed_closure⟩, ?_⟩
-- 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 : CommSemigroup G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun (x : G) ↦ x * g) μ = μ
have simp_rw : Measure.map (fun (x : G) ↦ g * x) μ = μ
Tactic: simp_rw [mul_comm, 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 : TopologicalSpace G
μ : Measure G
inst_3 : μ.IsHaarMeasure
inst_4 : ContinuousMul G
inst_5 : BorelSpace G
g : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) {g} : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) {1} : ℝ≥0∞)
have h : Eq (α := Set G) {g} (preimage (β := G) (fun (h : G) ↦ g⁻¹ * h) {1})
Tactic: convert! measure_preimage_mul μ 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 : TopologicalSpace G
μ : Measure G
inst_3 : μ.IsHaarMeasure
inst_4 : BorelSpace G
inst_5 : ContinuousMul G
H : Type u_3
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : MeasurableSpace H
inst_9 : BorelSpace H
inst_10 : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst_2, inst_7] (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h_prop : Tendsto (⇑f : (a : G) → H) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) (((map (⇑f : (a : G) → H) μ : Measure H) : (a : Set H) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑f : (a : G) → H) ⁻¹' closure[inst_7] K) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← hK.measure_closure, map_apply hf.measurable isClosed_closure.measurableSet]
-- 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
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
α : Type u_3
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
inst_7 : Group α
inst_8 : MulAction α G
inst_9 : SMulCommClass α G G
inst_10 : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := Homeomorph.toMeasurableEquiv (Homeomorph.smul a)
⊢ LT.lt (α := ℝ≥0∞) (((map (fun (x : G) ↦ a • x) μ : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have change : LT.lt (α := ℝ≥0∞) (((map (⇑F : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: change map F μ K < ∞
-- 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
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
α : Type u_3
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
inst_7 : Group α
inst_8 : MulAction α G
inst_9 : SMulCommClass α G G
inst_10 : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := Homeomorph.toMeasurableEquiv (Homeomorph.smul a)
⊢ LT.lt (α := ℝ≥0∞) (((map (⇑F : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑F : (a : G) → G) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [F.map_apply K]
-- 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
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NoAtoms μ
have inl : ∀ (x : G), Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
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 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NoAtoms μ
have inr : ∀ (K : Set G) (K_compact : IsCompact K) (K_nhds : Membership.mem (γ := Filter G) (𝓝 1) K), NoAtoms μ
Tactic: obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
K : Set G
K_compact : IsCompact K
K_nhds : Membership.mem (γ := Filter G) (𝓝 1) K
⊢ NoAtoms μ
have K_inf : K.Infinite
Tactic: have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Measure (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
⊢ NoAtoms μ
have x : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞) ∨
  Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: cases eq_or_ne (μ 1) 0 with
  | inl h => constructor; simpa
  | inr h =>
    obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1
    have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds
    exact absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩)
      K_compact.measure_lt_top.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.InnerRegular
g : G
⊢ map (fun (x : G) ↦ x * g) μ = modularCharacterFun g • μ
have rw : map (fun (x : G) ↦ x * g) μ = haarScalarFactor (map (fun (x : G) ↦ x * g) μ) μ • μ
Tactic: rw [modularCharacterFun_eq_haarScalarFactor μ _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g : G
⊢ 0 < modularCharacterFun g
have this : let this := borel G;
BorelSpace G
Tactic: borelize G
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ 0 < modularCharacterFun g
have rw : 0 < haarScalarFactor.{u_1} (G := G) (map (fun (x : G) ↦ x * g) haar) haar
Tactic: rw [modularCharacterFun_eq_haarScalarFactor MeasureTheory.Measure.haar g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h
have this : let this := borel G;
BorelSpace G
Tactic: borelize G
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h
have mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
Tactic: have mul_g_meas : Measurable (· * g) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) g
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.ModularCharacter (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h
have mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
Tactic: have mul_h_meas : Measurable (· * h) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) h