G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ 1 ≤ ↑(Content.outerMeasure (haarContent K₀)) ↑K₀
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ 0 < ↑(Content.outerMeasure (haarContent K₀)) ↑K₀
refine' zero_lt_one.trans_le _
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ 1 ≤
    ⨅ (U : Set G) (hU : IsOpen U) (_ : ↑K₀ ⊆ U), Content.innerContent (haarContent K₀) { carrier := U, is_open' := hU }
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ 1 ≤ ↑(Content.outerMeasure (haarContent K₀)) ↑K₀
rw [Content.outerMeasure_eq_iInf]
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
U : Set G
hU : IsOpen U
hK₀ : ↑K₀ ⊆ U
⊢ 1 ≤ (fun s => ↑(Content.toFun (haarContent K₀) s)) K₀.toCompacts
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ 1 ≤
    ⨅ (U : Set G) (hU : IsOpen U) (_ : ↑K₀ ⊆ U), Content.innerContent (haarContent K₀) { carrier := U, is_open' := hU }
refine' le_iInf₂ fun U hU => le_iInf fun hK₀ => le_trans _ <| le_iSup₂ K₀.toCompacts hK₀
no goals
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
U : Set G
hU : IsOpen U
hK₀ : ↑K₀ ⊆ U
⊢ 1 ≤ (fun s => ↑(Content.toFun (haarContent K₀) s)) K₀.toCompacts
exact haarContent_self.ge