G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ { val := 1, property := (_ : (fun r => 0 ≤ r) 1) } = 1
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ (fun s => ↑(Content.toFun (haarContent K₀) s)) K₀.toCompacts = 1
simp_rw [← ENNReal.coe_one, haarContent_apply, ENNReal.coe_eq_coe, chaar_self]
no goals
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
⊢ { val := 1, property := (_ : (fun r => 0 ≤ r) 1) } = 1
rfl