G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ (s_1 : Set G),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ → ↑↑(Measure.inv ν) s_1 < ⊤ → ∀ᵐ (x : G) ∂Measure.restrict μ s_1, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : G) ∂μ, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
refine' ae_of_forall_measure_lt_top_ae_restrict' ν.inv _ _
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑(Measure.inv ν) A < ⊤
⊢ ∀ᵐ (x : G) ∂Measure.restrict μ A, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ (s_1 : Set G),
    MeasurableSet s_1 →
      ↑↑μ s_1 < ⊤ → ↑↑(Measure.inv ν) s_1 < ⊤ → ∀ᵐ (x : G) ∂Measure.restrict μ s_1, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
intro A hA _ h3A
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
⊢ ∀ᵐ (x : G) ∂Measure.restrict μ A, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑(Measure.inv ν) A < ⊤
⊢ ∀ᵐ (x : G) ∂Measure.restrict μ A, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
simp only [ν.inv_apply] at h3A
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
⊢ ∀ᵐ (x : G) ∂Measure.restrict μ A, ↑↑ν ((fun y => y * x) ⁻¹' s) < ⊤
apply ae_lt_top (measurable_measure_mul_right ν sm)
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : (↑↑μ s * ∫⁻ (y : G), indicator A⁻¹ 1 y ∂ν) = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * indicator A⁻¹ 1 x⁻¹ ∂μ
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
have h1 := measure_mul_lintegral_eq μ ν sm (A⁻¹.indicator 1) (measurable_one.indicator hA.inv)
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : (↑↑μ s * ∫⁻ (a : G) in A⁻¹, OfNat.ofNat 1 a ∂ν) = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * indicator A⁻¹ 1 x⁻¹ ∂μ
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : (↑↑μ s * ∫⁻ (y : G), indicator A⁻¹ 1 y ∂ν) = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * indicator A⁻¹ 1 x⁻¹ ∂μ
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
rw [lintegral_indicator _ hA.inv] at h1
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ↑↑ν A⁻¹ = ∫⁻ (x : G), indicator A (fun a => ↑↑ν ((fun y => y * a) ⁻¹' s)) x ∂μ
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : (↑↑μ s * ∫⁻ (a : G) in A⁻¹, OfNat.ofNat 1 a ∂ν) = ∫⁻ (x : G), ↑↑ν ((fun z => z * x) ⁻¹' s) * indicator A⁻¹ 1 x⁻¹ ∂μ
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
simp_rw [Pi.one_apply, set_lintegral_one, ← image_inv, indicator_image inv_injective, image_inv, ←
  indicator_mul_right _ fun x => ν ((fun y => y * x) ⁻¹' s), Function.comp, Pi.one_apply,
  mul_one] at h1
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ↑↑ν A⁻¹ = ∫⁻ (x : G), indicator A (fun a => ↑↑ν ((fun y => y * a) ⁻¹' s)) x ∂μ
⊢ ↑↑μ s * ↑↑ν A⁻¹ ≠ ⊤
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ↑↑ν A⁻¹ = ∫⁻ (x : G), indicator A (fun a => ↑↑ν ((fun y => y * a) ⁻¹' s)) x ∂μ
⊢ (∫⁻ (x : G) in A, ↑↑ν ((fun y => y * x) ⁻¹' s) ∂μ) ≠ ⊤
rw [← lintegral_indicator _ hA, ← h1]
no goals
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SigmaFinite ν
inst✝³ : SigmaFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulLeftInvariant ν
sm : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
A : Set G
hA : MeasurableSet A
a✝ : ↑↑μ A < ⊤
h3A : ↑↑ν A⁻¹ < ⊤
h1 : ↑↑μ s * ↑↑ν A⁻¹ = ∫⁻ (x : G), indicator A (fun a => ↑↑ν ((fun y => y * a) ⁻¹' s)) x ∂μ
⊢ ↑↑μ s * ↑↑ν A⁻¹ ≠ ⊤
exact ENNReal.mul_ne_top hμs h3A.ne