-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measure_mul_measure_eq (s t : Set G) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) :
    μ' s * ν' t = ν' s * μ' t

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 :
  ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x => 1) x ∂ν'
h2 :
  μ' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x => 1) x ∂μ'
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rw [lintegral_indicator ht, setLIntegral_one] at h1 h2

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 : ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ν' t
h2 : μ' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = μ' t
⊢ μ' s * ν' t = ν' s * μ' t

Proof state:
case inr.intro.intro.intro.intro
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : μ' t' = μ' t
hν : ν' t' = ν' t
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rw [← hμ, ← hν, this _ hm]

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ⊤ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rw [← hμ, ← hν, this s' _ _ hm] <;> rwa [hν]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
wlog hs : MeasurableSet s generalizing s

Result:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ⊤ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
⊢ μ' s * ν' t = ν' s * μ' t

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
⊢ μ' s * ν' t = ν' s * μ' t

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 : ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ν' t
h2 : μ' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = μ' t
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rw [← h1, mul_left_comm, h2]

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rcases exists_measurable_superset₂ μ' ν' t with ⟨t', -, hm, hμ, hν⟩

Result:
case inr.intro.intro.intro.intro
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : μ' t' = μ' t
hν : ν' t' = ν' t
⊢ μ' s * ν' t = ν' s * μ' t

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
wlog ht : MeasurableSet t generalizing t

Result:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t

Proof state:
case inr
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ⊤ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
rcases exists_measurable_superset₂ μ' ν' s with ⟨s', -, hm, hμ, hν⟩

Result:
case inr.intro.intro.intro.intro
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ⊤ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ μ' s * ν' t = ν' s * μ' t