G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ↑↑(haarMeasure K₀) ↑K₀ = 1
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
⊢ ↑↑(haarMeasure K₀) ↑K₀ = 1
haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
case h0
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ↑(Content.outerMeasure (haarContent K₀)) ↑K₀ ≠ 0

case hI
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ↑(Content.outerMeasure (haarContent K₀)) ↑K₀ ≠ ⊤
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ↑↑(haarMeasure K₀) ↑K₀ = 1
rw [haarMeasure_apply K₀.isCompact.measurableSet, ENNReal.div_self]
case h0
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ 0 < ↑(Content.outerMeasure (haarContent K₀)) ↑K₀
case h0
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ↑(Content.outerMeasure (haarContent K₀)) ↑K₀ ≠ 0
rw [← pos_iff_ne_zero]
no goals
case h0
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ 0 < ↑(Content.outerMeasure (haarContent K₀)) ↑K₀
exact haarContent_outerMeasure_self_pos
no goals
case hI
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : T2Space G
inst✝² : TopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ↑(Content.outerMeasure (haarContent K₀)) ↑K₀ ≠ ⊤
exact (Content.outerMeasure_lt_top_of_isCompact _ K₀.isCompact).ne