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 : Set G
hK : IsCompact K
h2K : Set.Nonempty (interior K)
hμK : ↑↑μ K ≠ ⊤
⊢ Regular
    (↑↑μ ↑{ toCompacts := { carrier := K, isCompact' := hK }, interior_nonempty' := h2K } •
      haarMeasure { toCompacts := { carrier := K, isCompact' := hK }, interior_nonempty' := h2K })
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 : Set G
hK : IsCompact K
h2K : Set.Nonempty (interior K)
hμK : ↑↑μ K ≠ ⊤
⊢ Regular μ
rw [haarMeasure_unique μ ⟨⟨K, hK⟩, h2K⟩]
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 : Set G
hK : IsCompact K
h2K : Set.Nonempty (interior K)
hμK : ↑↑μ K ≠ ⊤
⊢ Regular
    (↑↑μ ↑{ toCompacts := { carrier := K, isCompact' := hK }, interior_nonempty' := h2K } •
      haarMeasure { toCompacts := { carrier := K, isCompact' := hK }, interior_nonempty' := h2K })
exact Regular.smul hμK