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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 :
  (↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂ν
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν 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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
have h1 :=
  measure_lintegral_div_measure ν ν hs h2s h3s (t.indicator fun _ => 1)
    (measurable_const.indicator ht)
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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 :
  (↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂ν
h2 :
  (↑↑μ s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂μ
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν 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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 :
  (↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂ν
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
have h2 :=
  measure_lintegral_div_measure μ ν hs h2s h3s (t.indicator fun _ => 1)
    (measurable_const.indicator ht)
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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 : (↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) = ↑↑ν t
h2 : (↑↑μ s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) = ↑↑μ t
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν 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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 :
  (↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂ν
h2 :
  (↑↑μ s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) =
    ∫⁻ (x : G), indicator t (fun x => 1) x ∂μ
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
rw [lintegral_indicator _ ht, set_lintegral_one] at h1 h2
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 ν
s t : Set G
hs : MeasurableSet s
ht : MeasurableSet t
h2s : ↑↑ν s ≠ 0
h3s : ↑↑ν s ≠ ⊤
h1 : (↑↑ν s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) = ↑↑ν t
h2 : (↑↑μ s * ∫⁻ (y : G), indicator t (fun x => 1) y⁻¹ / ↑↑ν ((fun x => x * y⁻¹) ⁻¹' s) ∂ν) = ↑↑μ t
⊢ ↑↑μ s * ↑↑ν t = ↑↑ν s * ↑↑μ t
rw [← h1, mul_left_comm, h2]