awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Measure
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∞)))

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 _)
-- Module: Mathlib.MeasureTheory.Group.Measure
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∞)))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set G) → ℝ≥0∞) (L n)) atTop (𝓝 ∞)

Tactic:
simp only [ENNReal.top_mul', K_pos.ne', if_false] at N

Premises used: if_false, LT.lt.ne', ENNReal.top_mul'
-- Module: Mathlib.MeasureTheory.Group.Measure
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 (𝓝 ∞)
apply : LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply top_le_iff.1

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Group.Measure
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 (𝓝 ∞)
⊢ LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
le_of_tendsto' N fun n => measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono, le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Group.Measure
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 (𝓝 ∞)
⊢ LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact le_of_tendsto' N fun n => measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono, le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Group.Measure
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 U : Set G
hU : IsOpen[inst_1] U
⊢ U * closure[inst_1] {1} = U

Tactic:
hU.mul_closure_one_eq

Premises used: IsOpen.mul_closure_one_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
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 U : Set G
hU : IsOpen[inst_1] U
⊢ U * closure[inst_1] {1} = U

Tactic:
exact hU.mul_closure_one_eq

Premises used: IsOpen.mul_closure_one_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
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 t : Set G
ht : MeasurableSet t
iht : t * closure[inst_1] {1} = t
⊢ tᶜ * closure[inst_1] {1} = tᶜ

Tactic:
compl_mul_closure_one_eq_iff.2 iht

Premises used: Iff.mpr, compl_mul_closure_one_eq_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
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 t : Set G
ht : MeasurableSet t
iht : t * closure[inst_1] {1} = t
⊢ tᶜ * closure[inst_1] {1} = tᶜ

Tactic:
exact compl_mul_closure_one_eq_iff.2 iht

Premises used: Iff.mpr, compl_mul_closure_one_eq_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
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
iUnion : Eq.{u_1 + 1} (α := Set G) (⋃ (i : ℕ), f i * closure[inst_1] {1}) (⋃ (i : ℕ), f i)
⊢ HMul.hMul (α := Set G) (⋃ (i : ℕ), f i) (closure[inst_1] {1}) = ⋃ (i : ℕ), f i

Tactic:
simp_rw [iUnion_mul f, ihf]

Premises used: Set.iUnion_mul
-- Module: Mathlib.MeasureTheory.Group.Measure
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ᶜ
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
⊢ s * closure[inst_1] {1} = s

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]

Premises used: Compl.compl, Set.iUnion
-- Module: Mathlib.MeasureTheory.Group.Measure
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
apply :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥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))

Premises used: le_antisymm, subset_mul_closure_one, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Group.Measure
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
rw : ⨅ (t : Set G), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set G) → ℝ≥0∞) t
| ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [measure_eq_iInf]

Premises used: MeasureTheory.measure_eq_iInf
-- Module: Mathlib.MeasureTheory.Group.Measure
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
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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
conv_rhs => rw [measure_eq_iInf]

Premises used: MeasureTheory.measure_eq_iInf
-- Module: Mathlib.MeasureTheory.Group.Measure
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
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∞)
⊢ 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:
simp only [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
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
h : s * closure[inst_1] {1} ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (s * closure[inst_1] {1}) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
apply measure_mono

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Group.Measure
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
h : s * closure[inst_1] {1} ⊆ t * closure[inst_1] {1}
⊢ s * closure[inst_1] {1} ⊆ t

Tactic:
rw [← t_meas.mul_closure_one_eq]

Premises used: MeasurableSet.mul_closure_one_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
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 * closure[inst_1] {1}

Tactic:
smul_subset_smul_right kt

Premises used: Set.smul_subset_smul_right
-- Module: Mathlib.MeasureTheory.Group.Measure
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 * closure[inst_1] {1}

Tactic:
exact smul_subset_smul_right kt

Premises used: Set.smul_subset_smul_right
-- Module: Mathlib.MeasureTheory.Group.Measure
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
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
⊢ (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

Tactic:
⟨s_meas, μs⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
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
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
⊢ ∃ 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⟩

Premises used: MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular, And.intro
-- Module: Mathlib.MeasureTheory.Group.Measure
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

Tactic:
⟨closure K, ?_, ⟨K_comp.closure, isClosed_closure⟩, ?_⟩

Premises used: IsCompact.closure, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.MeasureTheory.Group.Measure
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
refine_2 : r < (μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] K)
⊢ ∃ K ⊆ s, (fun (s : Set G) ↦ IsCompact s ∧ IsClosed[inst_1] s) K ∧ r < (μ : (a : Set G) → ℝ≥0∞) K

Tactic:
refine ⟨closure K, ?_, ⟨K_comp.closure, isClosed_closure⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
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
⊢ closure[inst_1] K ⊆ s

Tactic:
IsCompact.closure_subset_measurableSet K_comp s_meas Ks

Premises used: IsCompact.closure_subset_measurableSet
-- Module: Mathlib.MeasureTheory.Group.Measure
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
⊢ closure[inst_1] K ⊆ s

Tactic:
exact IsCompact.closure_subset_measurableSet K_comp s_meas Ks

Premises used: IsCompact.closure_subset_measurableSet
-- Module: Mathlib.MeasureTheory.Group.Measure
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 refine_2 refine_2₁ refine_2₂ refine_2₃ : r < (μ : (a : Set G) → ℝ≥0∞) K
⊢ r < (μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] K)

Tactic:
rwa [K_comp.measure_closure]

Premises used: IsCompact.measure_closure
-- Module: Mathlib.MeasureTheory.Group.Measure
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
simp_rw : Measure.map (fun (x : G) ↦ g * x) μ = μ
⊢ Measure.map (fun (x : G) ↦ x * g) μ = μ

Tactic:
simp_rw [mul_comm, map_mul_left_eq_self]

Premises used: MeasureTheory.map_mul_left_eq_self, mul_comm
-- Module: Mathlib.MeasureTheory.Group.Measure
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∞) (preimage (β := G) (fun (h : G) ↦ g⁻¹ * h) {1}) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) {1} : ℝ≥0∞)

Tactic:
measure_preimage_mul μ g⁻¹ _

Premises used: MeasureTheory.measure_preimage_mul, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
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
h : Eq (α := Set G) {g} (preimage (β := G) (fun (h : G) ↦ g⁻¹ * h) {1})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) {g} : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) {1} : ℝ≥0∞)

Tactic:
convert! measure_preimage_mul μ g⁻¹ _

Premises used: MeasureTheory.measure_preimage_mul, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
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 (α := Set G) {g} (preimage (β := G) (fun (h : G) ↦ g⁻¹ * h) {1})

Tactic:
simp only [mul_one, preimage_mul_left_singleton, inv_inv]

Premises used: inv_inv, Set.preimage_mul_left_singleton, mul_one
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
μ : Measure G
inst_3 : μ.IsHaarMeasure
c : ℝ≥0∞
cpos : c ≠ 0
ctop : c ≠ ∞
⊢ (c • μ).IsHaarMeasure

Tactic:
{ lt_top_of_isCompact := fun _K hK => ENNReal.mul_lt_top ctop.lt_top hK.measure_lt_top
    toIsOpenPosMeasure := isOpenPosMeasure_smul μ cpos }

Premises used: MeasureTheory.Measure.IsHaarMeasure.mk, MeasureTheory.Measure.isOpenPosMeasure_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
μ : Measure G
inst_3 : μ.IsHaarMeasure
c : ℝ≥0
hc : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simp [hc]
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h'K : (interior K).Nonempty
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.IsHaarMeasure

Tactic:
{ lt_top_of_isCompact := fun _L hL =>
      measure_lt_top_of_isCompact_of_isMulLeftInvariant' h'K h' hL
    toIsOpenPosMeasure := isOpenPosMeasure_of_mulLeftInvariant_of_compact K hK h }

Premises used: MeasureTheory.Measure.IsHaarMeasure.mk, MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact
-- Module: Mathlib.MeasureTheory.Group.Measure
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
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑f : (a : G) → H) ⁻¹' closure[inst_7] K) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((map (⇑f : (a : G) → H) μ : Measure H) : (a : Set H) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← hK.measure_closure, map_apply hf.measurable isClosed_closure.measurableSet]

Premises used: IsCompact.measure_closure, MeasureTheory.Measure.map_apply, IsClosed.measurableSet, Continuous.measurable, isClosed_closure
-- Module: Mathlib.MeasureTheory.Group.Measure
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
g : CocompactMap G H := { toFun := (⇑f : (a : G) → H), continuous_toFun := hf, cocompact_tendsto' := h_prop }
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑f : (a : G) → H) ⁻¹' closure[inst_7] K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
IsCompact.measure_lt_top (g.isCompact_preimage_of_isClosed hK.closure isClosed_closure)

Premises used: CocompactMap.isCompact_preimage_of_isClosed, IsCompact.closure, IsCompact.measure_lt_top, isClosed_closure
-- Module: Mathlib.MeasureTheory.Group.Measure
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
g : CocompactMap G H := { toFun := (⇑f : (a : G) → H), continuous_toFun := hf, cocompact_tendsto' := h_prop }
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑f : (a : G) → H) ⁻¹' closure[inst_7] K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact IsCompact.measure_lt_top (g.isCompact_preimage_of_isClosed hK.closure isClosed_closure)

Premises used: CocompactMap.isCompact_preimage_of_isClosed, IsCompact.closure, IsCompact.measure_lt_top, isClosed_closure