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

Tactic:
refine ae_of_forall_measure_lt_top_ae_restrict' ν'.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
⊢ ∀ (s_1 : Set G),
    MeasurableSet s_1 → μ' s_1 < ⊤ → ν'.inv s_1 < ⊤ → ∀ᵐ (x : G) ∂μ'.restrict s_1, ν' ((fun x_1 => x_1 * 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 * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j => ν' ((fun x => x * j) ⁻¹' s)) x ∂μ'
⊢ μ' s * ν' A⁻¹ ≠ ⊤

Tactic:
exact ENNReal.mul_ne_top hμs h3A.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
hμs : μ' s ≠ ⊤
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤

Tactic:
wlog sm : MeasurableSet s generalizing s

Result:
case inr
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) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤

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
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 * 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
⊢ ∀ (s_1 : Set G),
    MeasurableSet s_1 → μ' s_1 < ⊤ → ν'.inv s_1 < ⊤ → ∀ᵐ (x : G) ∂μ'.restrict s_1, ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤

Tactic:
intro A hA _ h3A

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 : ν'.inv A < ⊤
⊢ ∀ᵐ (x : G) ∂μ'.restrict A, ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤

Proof state:
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

Tactic:
apply subset_toMeasurable

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

Tactic:
rw [← lintegral_indicator hA, ← 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⁻¹ = ∫⁻ (x : G), A.indicator (fun j => ν' ((fun x => x * j) ⁻¹' s)) x ∂μ'
⊢ μ' s * ν' A⁻¹ ≠ ⊤

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) ∂μ'.restrict A, ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤

Tactic:
apply ae_lt_top (measurable_measure_mul_right ν' sm)

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⁻¹ < ⊤
⊢ ∫⁻ (x : G) in A, ν' ((fun y => y * x) ⁻¹' s) ∂μ' ≠ ⊤

Proof state:
case inr
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) ∂μ', ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤

Tactic:
filter_upwards [this ((measure_toMeasurable _).trans_ne hμs) (measurableSet_toMeasurable ..)]
  with x hx using lt_of_le_of_lt (by gcongr; apply subset_toMeasurable) hx

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

Tactic:
simp only [ν'.inv_apply] at h3A

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⁻¹ < ⊤
⊢ ∀ᵐ (x : G) ∂μ'.restrict A, ν' ((fun x_1 => x_1 * x) ⁻¹' s) < ⊤