awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y : G
h : Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (b : G) ↦ 1) ((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x)
⊢ Eq (α := ℝ≥0∞) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y) (s.indicator (fun (x : G) ↦ 1) (y * x))

Tactic:
convert! indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2

Premises used: HMul.hMul, Set.indicator_comp_right
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y : G
h : ∀ (x_1 : G), Eq (α := ℝ≥0∞) 1 (((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x) x_1)
⊢ Eq.{u_1 + 1} (α := G → ℝ≥0∞) (fun (b : G) ↦ 1) ((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x)

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
x y x_1 : G
⊢ Eq (α := ℝ≥0∞) 1 (((fun (x : G) ↦ 1) ∘ fun (y : G) ↦ y * x) x_1)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
⊢ ∀ (x y : G),
    Eq (α := ℝ≥0∞) (s.indicator (fun (x : G) ↦ 1) (y * x)) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y)

Tactic:
have : ∀ x y, s.indicator (fun _ : G => (1 : ℝ≥0∞)) (y * x) =
      ((fun z => z * x) ⁻¹' s).indicator (fun b : G => 1) y := by
    intro x y; symm; convert! indicator_comp_right (M := ℝ≥0∞) fun y => y * x using 2; ext1; rfl
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
s : Set G
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable (β := ℝ≥0∞) fun (y : G) ↦ indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y
this :
  ∀ (x y : G),
    Eq (α := ℝ≥0∞) (s.indicator (fun (x : G) ↦ 1) (y * x)) (indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (b : G) ↦ 1) y)
simp_rw :
  ∫⁻ (x : G), ∫⁻ (y : G), indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) y * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
simp_rw₁ :
  ∫⁻ (x : G), (∫⁻ (a : G), indicator ((fun (z : G) ↦ z * x) ⁻¹' s) (fun (x : G) ↦ 1) a ∂ν) * f x⁻¹ ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
simp_rw₂ :
  ∫⁻ (x : G), (∫⁻ (x : G) in (fun (z : G) ↦ z * x) ⁻¹' s, 1 ∂ν) * f x⁻¹ ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ
⊢ ∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun (x : G) ↦ 1) (y * x) * f x⁻¹ ∂ν ∂μ =
    ∫⁻ (x : G), HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞) (f x⁻¹) ∂μ

Tactic:
simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm),
    setLIntegral_one]

Premises used: MeasureTheory.lintegral_mul_const, MeasureTheory.setLIntegral_one, MeasureTheory.lintegral_indicator, MeasurableMul.measurable_mul_const
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
hν : ν ≠ 0
⊢ μ ≪ ν

Tactic:
AbsolutelyContinuous.mk fun s sm hνs => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
hν : ν ≠ 0
refine :
  ∀ (s : Set G) (sm : MeasurableSet s) (hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ ν

Tactic:
refine AbsolutelyContinuous.mk fun s sm hνs => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (y : G), 1 y ∂ν) =
    ∫⁻ (x : G),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (1 x⁻¹ : ℝ≥0∞) ∂μ

Tactic:
have h1 := measure_mul_lintegral_eq μ ν sm 1 measurable_one
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h1 :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (y : G), 1 y ∂ν) =
    ∫⁻ (x : G),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (1 x⁻¹ : ℝ≥0∞) ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [Pi.one_apply, lintegral_one, mul_one, (measure_mul_right_null ν _).mpr hνs,
    lintegral_zero, mul_eq_zero (M₀ := ℝ≥0∞), measure_univ_eq_zero.not.mpr hν, or_false] at h1

Premises used: Iff.mpr, MeasureTheory.measure_mul_right_null, Pi.one_apply, MeasureTheory.lintegral_zero, Iff.not, mul_eq_zero, or_false, MeasureTheory.Measure.measure_univ_eq_zero, mul_one, MeasureTheory.lintegral_one
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h1 : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h1
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
μ ν : Measure G
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulLeftInvariant
inst_7 : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h1 : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact h1
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inr :
  ∀
    (this :
      ∀ {s : Set G} (hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (sm : MeasurableSet s),
        ∀ᵐ (x : G) ∂μ',
          LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (sm : ¬MeasurableSet s),
    ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
wlog :
  ∀ {s : Set G} (hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (sm : MeasurableSet s),
    ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
wlog sm : MeasurableSet s generalizing s

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ {s : Set G} (hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (sm : MeasurableSet s),
    ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : ¬MeasurableSet s
x : G
hx : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' toMeasurable μ' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : s ⊆ toMeasurable μ' s
⊢ LE.le (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞)
    ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' toMeasurable μ' s) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ {s : Set G} (hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (sm : MeasurableSet s),
    ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : ¬MeasurableSet s
x : G
hx : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' toMeasurable μ' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s ⊆ toMeasurable μ' s

Tactic:
apply subset_toMeasurable

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ {s : Set G} (hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (sm : MeasurableSet s),
    ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : ¬MeasurableSet s
h :
  ∀ (a : G),
    Membership.mem (γ := Set G)
      {x : G |
        Membership.mem (γ := Set G)
            {x : G |
              (fun (x : G) ↦
                  LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' toMeasurable μ' s) : ℝ≥0∞)
                    (∞ : ℝ≥0∞))
                x}
            x →
          Membership.mem (γ := Set G)
            {x : G |
              (fun (x : G) ↦
                  LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞))
                x}
            x}
      a
h₁ h₂ :
  ∀ (x : G)
    (hx :
      LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' toMeasurable μ' s) : ℝ≥0∞)
        (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable, Eq.trans_ne
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ae_of_forall_measure_lt_top_ae_restrict' ν'.inv _ ?_

Premises used: MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict', MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
refine :
  ∀ (s_2 : Set G),
    MeasurableSet s_2 →
      LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s_2 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν'.inv : (a : Set G) → ℝ≥0∞) s_2 : ℝ≥0∞) (∞ : ℝ≥0∞) →
          ∀ᵐ (x : G) ∂μ'.restrict s_2,
            LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine ae_of_forall_measure_lt_top_ae_restrict' ν'.inv _ ?_

Premises used: MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict', MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
_ :
  LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞) →
    LT.lt (α := ℝ≥0∞) ((ν'.inv : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∀ᵐ (x : G) ∂μ'.restrict A,
        LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞) →
    LT.lt (α := ℝ≥0∞) ((ν'.inv : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∀ᵐ (x : G) ∂μ'.restrict A,
        LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
h : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
h3A : LT.lt (α := ℝ≥0∞) ((ν'.inv : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: MeasureTheory.Measure.inv_apply
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
h : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
h3A : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
apply : ∫⁻ (x : G) in A, (ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
⊢ ∀ᵐ (x : G) ∂μ'.restrict A,
    LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply ae_lt_top (measurable_measure_mul_right ν' sm)

Premises used: MeasureTheory.measurable_measure_mul_right, MeasureTheory.ae_lt_top
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
h : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
h3A : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (y : G), A⁻¹.indicator 1 y ∂ν') =
    ∫⁻ (x : G),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (A⁻¹.indicator 1 x⁻¹ : ℝ≥0∞) ∂μ'

Tactic:
have h1 := measure_mul_lintegral_eq μ' ν' sm (A⁻¹.indicator 1) (measurable_one.indicator hA.inv)
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
h : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
h3A : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
h1 :
  HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (y : G), A⁻¹.indicator 1 y ∂ν') =
    ∫⁻ (x : G),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (A⁻¹.indicator 1 x⁻¹ : ℝ≥0∞) ∂μ'
⊢ HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (a : G) in A⁻¹, 1 a ∂ν') =
    ∫⁻ (x : G),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (A⁻¹.indicator 1 x⁻¹ : ℝ≥0∞) ∂μ'

Tactic:
rw [lintegral_indicator hA.inv] at h1

Premises used: MeasureTheory.lintegral_indicator, MeasurableSet.inv
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
h : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
h3A : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
h1 :
  HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∫⁻ (a : G) in A⁻¹, 1 a ∂ν') =
    ∫⁻ (x : G),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (A⁻¹.indicator 1 x⁻¹ : ℝ≥0∞) ∂μ'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) =
    ∫⁻ (x : G), A.indicator (fun (j : G) ↦ (ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * j) ⁻¹' s)) x ∂μ'

Tactic:
simp_rw [Pi.one_apply, setLIntegral_one, ← image_inv_eq_inv, indicator_image inv_injective,
    image_inv_eq_inv, ← indicator_mul_right _ fun x => ν' ((· * x) ⁻¹' s), Function.comp,
    Pi.one_apply, mul_one] at h1

Premises used: HMul.hMul, Pi.one_apply, Set.indicator_image, Function.comp, MeasureTheory.setLIntegral_one, Set.preimage, inv_injective, mul_one, Set.indicator_mul_right, Set.image_inv_eq_inv, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
h : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
h3A : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
h1 :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) =
    ∫⁻ (x : G), A.indicator (fun (j : G) ↦ (ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * j) ⁻¹' s)) x ∂μ'
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) ≠ ∞
⊢ ∫⁻ (x : G) in A, (ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
rw [← lintegral_indicator hA, ← h1]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s_1 : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
hμs : Ne (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
h : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
h3A : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
h1 :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) =
    ∫⁻ (x : G), A.indicator (fun (j : G) ↦ (ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * j) ⁻¹' s)) x ∂μ'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Group.Prod
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul₂ G
s : Set G
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

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

Premises used: Filter.Eventually.filter_mono, MeasureTheory.ae_measure_preimage_mul_right_lt_top