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
n : ℕ
IH : IsCompact (L n)
⊢ IsCompact (X := G) (((fun (T : Set G) ↦ T ∪ g T • K) ∘ (fun (T : Set G) ↦ T ∪ g T • K)^[n]) K)

Tactic:
apply IsCompact.union IH (hK.smul (g (L n)))

Premises used: IsCompact.union, IsCompact.smul
-- 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
n : ℕ
zero : IsCompact (L 0)
succ : ∀ (n : ℕ) (IH : IsCompact (L n)), IsCompact (L (n + 1))
⊢ IsCompact (L n)

Tactic:
induction n with
    | zero => exact hK
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsCompact.union IH (hK.smul (g (L n)))

Premises used: Function.iterate_succ'
-- 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
⊢ ∀ (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)))
-- 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)
⊢ IsClosed[inst_1] (L 0)

Tactic:
Kclosed

Premises used: Nat.iterate
-- 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)
⊢ IsClosed[inst_1] (L 0)

Tactic:
exact Kclosed
-- 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)
n : ℕ
IH : IsClosed[inst_1] (L n)
succ : IsClosed[inst_1] (((fun (T : Set G) ↦ T ∪ g T • K) ∘ (fun (T : Set G) ↦ T ∪ g T • K)^[n]) K)
⊢ IsClosed[inst_1] (L (n + 1))

Tactic:
simp_rw [L, iterate_succ']

Premises used: Function.iterate_succ'
-- 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)
n : ℕ
IH : IsClosed[inst_1] (L n)
⊢ IsClosed[inst_1] (((fun (T : Set G) ↦ T ∪ g T • K) ∘ (fun (T : Set G) ↦ T ∪ g T • K)^[n]) K)

Tactic:
apply IsClosed.union IH (Kclosed.smul (g (L n)))

Premises used: IsClosed.union, IsClosed.smul
-- 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)
n : ℕ
zero : IsClosed[inst_1] (L 0)
succ : ∀ (n : ℕ) (IH : IsClosed[inst_1] (L n)), IsClosed[inst_1] (L (n + 1))
⊢ IsClosed[inst_1] (L n)

Tactic:
induction n with
    | zero => exact Kclosed
    | succ n IH =>
      simp_rw [L, iterate_succ']
      apply IsClosed.union IH (Kclosed.smul (g (L n)))

Premises used: Function.iterate_succ'
-- 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)
⊢ ∀ (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)))
-- 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)
⊢ (μ : (a : Set G) → ℝ≥0∞) (L 0) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
simp only [L, one_mul, Nat.cast_one, iterate_zero, id, Nat.zero_add]

Premises used: Function.iterate_zero, id, Nat.zero_add, Nat.cast_one, one_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)
n : ℕ
IH :
  (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
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∞)
⊢ (μ : (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:
simp_rw [L, iterate_succ']

Premises used: Function.iterate_succ'
-- 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)
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∞) (((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:
measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.measure_union'
-- 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)
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∞) (((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:
exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet

Premises used: IsClosed.measurableSet, MeasureTheory.measure_union'
-- 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)
n : ℕ
IH :
  (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ 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:
simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]

Premises used: add_mul, Nat.cast_add, MeasureTheory.measure_smul, Nat.cast_one, one_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)
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∞)
μ₂ :
  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∞)
⊢ (μ : (a : Set G) → ℝ≥0∞) (L (n + 1)) =
    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]

Premises used: HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- 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)
n : ℕ
zero :
  (μ : (a : Set G) → ℝ≥0∞) (L 0) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
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∞)
⊢ (μ : (a : Set G) → ℝ≥0∞) (L n) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(n + 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]

Premises used: Function.iterate_zero, id, HAdd.hAdd, HSMul.hSMul, Nat.zero_add, OfNat.ofNat, Nat.cast_one, DFunLike.coe, one_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)
⊢ ∀ (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]
-- 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∞)
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∞)))
⊢ Tendsto (fun (n : ℕ) ↦ (μ : (a : Set G) → ℝ≥0∞) (L n)) atTop
    (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)))

Tactic:
simp_rw [M]
-- 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∞)
apply : Tendsto (β := ℝ≥0∞) (fun (x : ℕ) ↦ (↑(x + 1) : ℝ≥0∞)) atTop (𝓝 ∞)
⊢ 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:
apply ENNReal.Tendsto.mul_const _ (Or.inl ENNReal.top_ne_zero)

Premises used: ENNReal.Tendsto.mul_const, Or.inl, ENNReal.top_ne_zero
-- 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 (β := ℝ≥0∞) (fun (x : ℕ) ↦ (↑(x + 1) : ℝ≥0∞)) atTop (𝓝 ∞)

Tactic:
ENNReal.tendsto_nat_nhds_top.comp (tendsto_add_atTop_nat _)

Premises used: ENNReal.tendsto_nat_nhds_top, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp
-- 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 (β := ℝ≥0∞) (fun (x : ℕ) ↦ (↑(x + 1) : ℝ≥0∞)) atTop (𝓝 ∞)

Tactic:
exact ENNReal.tendsto_nat_nhds_top.comp (tendsto_add_atTop_nat _)

Premises used: ENNReal.tendsto_nat_nhds_top, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp