-- Mathlib/MeasureTheory/Group/Prod.lean
theorem ae_measure_preimage_mul_right_lt_top (hμs : μ' s ≠ ∞) :
    ∀ᵐ x ∂μ', ν' ((· * x) ⁻¹' s) < ∞

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
s : Set G
hμs : μ' s ≠ ⊤
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ⊤
h3A : ν' A⁻¹ < ⊤
⊢ ∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤

Tactic:
have h1 := measure_mul_lintegral_eq μ' ν' sm (A⁻¹.indicator 1) (measurable_one.indicator hA.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
s : Set G
hμs : μ' s ≠ ⊤
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ⊤
h3A : ν' A⁻¹ < ⊤
h1 : μ' s * ∫⁻ (y : G), A⁻¹.indicator 1 y ∂ν' = ∫⁻ (x : G), ν' ((fun z => z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤

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
s : Set G
hμs : μ' s ≠ ⊤
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ⊤
h3A : ν' A⁻¹ < ⊤
h1 : μ' s * ∫⁻ (y : G), A⁻¹.indicator 1 y ∂ν' = ∫⁻ (x : G), ν' ((fun z => z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤

Tactic:
rw [lintegral_indicator hA.inv] at h1

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
s : Set G
hμs : μ' s ≠ ⊤
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ⊤
h3A : ν' A⁻¹ < ⊤
h1 : μ' s * ∫⁻ (a : G) in A⁻¹, 1 a ∂ν' = ∫⁻ (x : G), ν' ((fun z => z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤

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
hμs : μ' s ≠ ⊤
this : ∀ {s : Set G}, μ' s ≠ ⊤ → MeasurableSet s → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
sm : ¬MeasurableSet s
x : G
hx : ν' ((fun x_1 => x_1 * x) ⁻¹' toMeasurable μ' s) < ⊤
⊢ ν' ((fun x_1 => x_1 * x) ⁻¹' s) ≤ ν' ((fun x_1 => x_1 * x) ⁻¹' toMeasurable μ' s)

Tactic:
gcongr

Result:
case h.h
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
hμs : μ' s ≠ ⊤
this : ∀ {s : Set G}, μ' s ≠ ⊤ → MeasurableSet s → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤
sm : ¬MeasurableSet s
x : G
hx : ν' ((fun x_1 => x_1 * x) ⁻¹' toMeasurable μ' s) < ⊤
⊢ s ⊆ toMeasurable μ' s