-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measure_lintegral_div_measure (sm : MeasurableSet s) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞)
    (f : G → ℝ≥0∞) (hf : Measurable f) :
    (μ' s * ∫⁻ y, f y⁻¹ / ν' ((· * y⁻¹) ⁻¹' s) ∂ν') = ∫⁻ x, f x ∂μ'

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
x : G
hx : ν' ((fun y => y * x) ⁻¹' s) < ⊤
⊢ (fun x => ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s))) x = f x

Tactic:
simp_rw [ENNReal.mul_div_cancel (measure_mul_right_ne_zero ν' h2s _) hx.ne]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ (fun x => ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s))) =ᶠ[ae μ'] f

Tactic:
refine (ae_measure_preimage_mul_right_lt_top_of_ne_zero μ' ν' h2s h3s).mono fun x hx => ?_

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
x : G
hx : ν' ((fun y => y * x) ⁻¹' s) < ⊤
⊢ (fun x => ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s))) x = f x

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ∫⁻ (x : G), ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s)) ∂μ' = ∫⁻ (x : G), f x ∂μ'

Tactic:
refine lintegral_congr_ae ?_

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ (fun x => ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s))) =ᶠ[ae μ'] f

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
⊢ μ' s * ∫⁻ (y : G), f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' = ∫⁻ (x : G), f x ∂μ'

Tactic:
set g := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Tactic:
have hg : Measurable g :=
  (hf.comp measurable_inv).div ((measurable_measure_mul_right ν' sm).comp measurable_inv)

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Tactic:
simp_rw [measure_mul_lintegral_eq μ' ν' sm g hg, g, inv_inv]

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y => f y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ∫⁻ (x : G), ν' ((fun x_1 => x_1 * x) ⁻¹' s) * (f x / ν' ((fun x_1 => x_1 * x) ⁻¹' s)) ∂μ' = ∫⁻ (x : G), f x ∂μ'