-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
theorem absolutelyContinuous_isHaarMeasure [LocallyCompactSpace G]
    [SecondCountableTopology G] (μ ν : Measure G)
    [SigmaFinite μ] [IsMulLeftInvariant μ] [IsHaarMeasure ν] : μ ≪ ν

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
inst✝³ : SecondCountableTopology G
μ ν : Measure G
inst✝² : SigmaFinite μ
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsHaarMeasure
K : PositiveCompacts G
h : haarMeasure K = ↑((haarMeasure K).haarScalarFactor ν) • ν
⊢ (μ ↑K * ↑((haarMeasure K).haarScalarFactor ν)) • ν ≪ ν

Tactic:
exact smul_absolutelyContinuous

Result:
no goals

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
inst✝³ : SecondCountableTopology G
μ ν : Measure G
inst✝² : SigmaFinite μ
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsHaarMeasure
K : PositiveCompacts G
⊢ μ ≪ ν

Tactic:
have h : haarMeasure K = (haarScalarFactor (haarMeasure K) ν : ℝ≥0∞) • ν :=
  isMulLeftInvariant_eq_smul (haarMeasure K) ν

Result:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
inst✝³ : SecondCountableTopology G
μ ν : Measure G
inst✝² : SigmaFinite μ
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsHaarMeasure
K : PositiveCompacts G
h : haarMeasure K = ↑((haarMeasure K).haarScalarFactor ν) • ν
⊢ μ ≪ ν

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
inst✝³ : SecondCountableTopology G
μ ν : Measure G
inst✝² : SigmaFinite μ
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsHaarMeasure
K : PositiveCompacts G
h : haarMeasure K = ↑((haarMeasure K).haarScalarFactor ν) • ν
⊢ μ ≪ ν

Tactic:
rw [haarMeasure_unique μ K, h, smul_smul]

Result:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
inst✝³ : SecondCountableTopology G
μ ν : Measure G
inst✝² : SigmaFinite μ
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsHaarMeasure
K : PositiveCompacts G
h : haarMeasure K = ↑((haarMeasure K).haarScalarFactor ν) • ν
⊢ (μ ↑K * ↑((haarMeasure K).haarScalarFactor ν)) • ν ≪ ν

Proof state:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
inst✝³ : SecondCountableTopology G
μ ν : Measure G
inst✝² : SigmaFinite μ
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsHaarMeasure
⊢ μ ≪ ν

Tactic:
have K : PositiveCompacts G := Classical.arbitrary _

Result:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
inst✝³ : SecondCountableTopology G
μ ν : Measure G
inst✝² : SigmaFinite μ
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsHaarMeasure
K : PositiveCompacts G
⊢ μ ≪ ν