no goals
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : T2Space G
inst✝⁵ : TopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
μ : Measure G
inst✝¹ : SigmaFinite μ
inst✝ : IsMulLeftInvariant μ
K₀ : PositiveCompacts G
⊢ (↑↑μ ↑K₀ / ↑↑(haarMeasure K₀) ↑K₀) • haarMeasure K₀ = ↑↑μ ↑K₀ • haarMeasure K₀
rw [haarMeasure_self, div_one]