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
s : Set G
hs : MeasurableSet s
⊢ (↑(Content.outerMeasure (haarContent K₀)) ↑K₀)⁻¹ * ↑↑(Content.measure (haarContent K₀)) s =
    ↑(Content.outerMeasure (haarContent K₀)) s / ↑(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
s : Set G
hs : MeasurableSet s
⊢ ↑↑(haarMeasure K₀) s = ↑(Content.outerMeasure (haarContent K₀)) s / ↑(Content.outerMeasure (haarContent K₀)) ↑K₀
change ((haarContent K₀).outerMeasure K₀)⁻¹ * (haarContent K₀).measure s = _
no goals
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
s : Set G
hs : MeasurableSet s
⊢ (↑(Content.outerMeasure (haarContent K₀)) ↑K₀)⁻¹ * ↑↑(Content.measure (haarContent K₀)) s =
    ↑(Content.outerMeasure (haarContent K₀)) s / ↑(Content.outerMeasure (haarContent K₀)) ↑K₀
simp only [hs, div_eq_mul_inv, mul_comm, Content.measure_apply]