case h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
hs : MeasurableSet s
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
t : Set G
ht : MeasurableSet t
⊢ ↑↑μ t = ↑↑((↑↑μ s / ↑↑ν s) • ν) t
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
hs : MeasurableSet s
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ μ = (↑↑μ s / ↑↑ν s) • ν
ext1 t ht
no goals
case h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
hs : MeasurableSet s
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
t : Set G
ht : MeasurableSet t
⊢ ↑↑μ t = ↑↑((↑↑μ s / ↑↑ν s) • ν) t
rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
  measure_mul_measure_eq μ ν hs ht h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel' h2s h3s]