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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
⊢ ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
⊢ ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν
have K : PositiveCompacts G := Classical.arbitrary _
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
⊢ ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
⊢ ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν
have νpos : 0 < ν K := measure_pos_of_nonempty_interior _ K.interior_nonempty
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
⊢ ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν
have νne : ν K ≠ ∞ := K.isCompact.measure_lt_top.ne
case refine'_1
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ ↑↑μ ↑K / ↑↑ν ↑K ≠ 0

case refine'_2
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ ↑↑μ ↑K / ↑↑ν ↑K ≠ ⊤

case refine'_3
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ μ = (↑↑μ ↑K / ↑↑ν ↑K) • ν
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ ∃ c, c ≠ 0 ∧ c ≠ ⊤ ∧ μ = c • ν
refine' ⟨μ K / ν K, _, _, _⟩
no goals
case refine'_1
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ ↑↑μ ↑K / ↑↑ν ↑K ≠ 0
simp only [νne, (μ.measure_pos_of_nonempty_interior K.interior_nonempty).ne', Ne.def,
  ENNReal.div_eq_zero_iff, not_false_iff, or_self_iff]
no goals
case refine'_2
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ ↑↑μ ↑K / ↑↑ν ↑K ≠ ⊤
simp only [div_eq_mul_inv, νpos.ne', (K.isCompact.measure_lt_top (μ := μ)).ne, or_self_iff,
  ENNReal.inv_eq_top, ENNReal.mul_eq_top, Ne.def, not_false_iff, and_false_iff,
  false_and_iff]
no goals
case refine'_3
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ μ = (↑↑μ ↑K / ↑↑ν ↑K) • ν
calc
  μ = μ K • haarMeasure K := haarMeasure_unique μ K
  _ = (μ K / ν K) • ν K • haarMeasure K := by
    rw [smul_smul, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel νpos.ne' νne, mul_one]
  _ = (μ K / ν K) • ν := by rw [← haarMeasure_unique ν K]
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ ↑↑μ ↑K • haarMeasure K = (↑↑μ ↑K / ↑↑ν ↑K) • ↑↑ν ↑K • haarMeasure K
rw [smul_smul, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel νpos.ne' νne, mul_one]
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
inst✝² : LocallyCompactSpace G
μ ν : Measure G
inst✝¹ : IsHaarMeasure μ
inst✝ : IsHaarMeasure ν
K : PositiveCompacts G
νpos : 0 < ↑↑ν ↑K
νne : ↑↑ν ↑K ≠ ⊤
⊢ (↑↑μ ↑K / ↑↑ν ↑K) • ↑↑ν ↑K • haarMeasure K = (↑↑μ ↑K / ↑↑ν ↑K) • ν
rw [← haarMeasure_unique ν K]