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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
⊢ ↑↑μ s = 0
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 ν
hν : ν ≠ 0
⊢ μ ≪ ν
refine' AbsolutelyContinuous.mk fun s sm hνs => _
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
h1 : (↑↑μ s * ∫⁻ (y : G), OfNat.ofNat 1 y ∂ν) = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * OfNat.ofNat 1 x⁻¹ ∂μ
⊢ ↑↑μ s = 0
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
⊢ ↑↑μ s = 0
have h1 := measure_mul_lintegral_eq μ ν sm 1 measurable_one
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
h1 : ↑↑μ s = 0
⊢ ↑↑μ s = 0
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
h1 : (↑↑μ s * ∫⁻ (y : G), OfNat.ofNat 1 y ∂ν) = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * OfNat.ofNat 1 x⁻¹ ∂μ
⊢ ↑↑μ s = 0
simp_rw [Pi.one_apply, lintegral_one, mul_one, (measure_mul_right_null ν _).mpr hνs,
  lintegral_zero, mul_eq_zero (M₀ := ℝ≥0∞), measure_univ_eq_zero.not.mpr hν, or_false_iff] at h1
no goals
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 ν
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ↑↑ν s = 0
h1 : ↑↑μ s = 0
⊢ ↑↑μ s = 0
exact h1