-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measure_univ_of_isMulLeftInvariant [WeaklyLocallyCompactSpace G] [NoncompactSpace G]
    (μ : Measure G) [IsOpenPosMeasure μ] [μ.IsMulLeftInvariant] : μ univ = ∞

Proof state:
case intro.intro.intro
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
⊢ μ univ = ⊤

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 _)

Result:
case intro.intro.intro
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
N : Tendsto (fun n => μ (L n)) atTop (𝓝 (⊤ * μ K))
⊢ μ univ = ⊤

Proof state:
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
n : ℕ
IH : μ (L n) = ↑(n + 1) * μ K
⊢ μ (((fun T => T ∪ g T • K) ∘ (fun T => T ∪ g T • K)^[n]) K) =
    μ ((fun T => T ∪ g T • K)^[n] K) + μ (g ((fun T => T ∪ g T • K)^[n] K) • K)

Tactic:
exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet

Result:
no goals

Proof state:
case intro.intro.intro
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
N : Tendsto (fun n => μ (L n)) atTop (𝓝 ⊤)
⊢ ⊤ ≤ μ univ

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

Result:
no goals

Proof state:
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n => (fun T => T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed (L n)
M : ∀ (n : ℕ), μ (L n) = ↑(n + 1) * μ K
⊢ Tendsto (fun x => ↑(x + 1)) atTop (𝓝 ⊤)

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

Result:
no goals