-- Mathlib/MeasureTheory/Group/Prod.lean
theorem ae_measure_preimage_mul_right_lt_top_of_ne_zero (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) :
    ∀ᵐ x ∂μ', ν' ((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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ ν' ≠ 0

Tactic:
refine mt ?_ h2s

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ ν' = 0 → ν' s = 0

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hν : ν' = 0
⊢ ν' s = 0

Tactic:
rw [hν, Measure.coe_zero, Pi.zero_apply]

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ ν' = 0 → ν' s = 0

Tactic:
intro hν

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hν : ν' = 0
⊢ ν' s = 0

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun y => y * x) ⁻¹' s) < ⊤

Tactic:
refine (ae_measure_preimage_mul_right_lt_top ν' ν' h3s).filter_mono ?_

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ ae μ' ≤ ae ν'

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ ae μ' ≤ ae ν'

Tactic:
refine (absolutelyContinuous_of_isMulLeftInvariant μ' ν' ?_).ae_le

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ ν' ≠ 0