awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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)
⊢ ∫⁻ (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⁻¹) ∂μ
have 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⁻¹) ∂μ
Tactic: simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm),
    setLIntegral_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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⁻¹) ∂μ
⊢ ∫⁻ (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⁻¹) ∂μ
have 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⁻¹) ∂μ
Tactic: simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm),
    setLIntegral_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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⁻¹) ∂μ
⊢ ∫⁻ (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⁻¹) ∂μ
have 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⁻¹) ∂μ
Tactic: simp_rw [this, lintegral_mul_const _ (ms _), lintegral_indicator (measurable_mul_const _ sm),
    setLIntegral_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
⊢ μ ≪ ν
have 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 => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞) ∂μ
Tactic: have h1 := measure_mul_lintegral_eq μ ν sm 1 measurable_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
Tactic: wlog sm : MeasurableSet s generalizing s
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
Tactic: wlog sm : MeasurableSet s generalizing s
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
⊢ 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∞)
have h : s ⊆ toMeasurable μ' s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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
⊢ ∀ᵐ (x : G) ∂μ', LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₁ : ∀ (a : G),
  LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * a) ⁻¹' toMeasurable μ' s) : ℝ≥0∞) (∞ : ℝ≥0∞) →
    LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * a) ⁻¹' 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
have 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∞)
Tactic: refine ae_of_forall_measure_lt_top_ae_restrict' ν'.inv _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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∞)
⊢ ∀ᵐ (x : G) ∂μ'.restrict A,
    LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h3A₁ : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [ν'.inv_apply] at h3A
Cleared hypotheses: h3A
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
⊢ ∀ᵐ (x : G) ∂μ'.restrict A,
    LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x_1 : G) ↦ x_1 * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply : ∫⁻ (x : G) in A, (ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Tactic: apply ae_lt_top (measurable_measure_mul_right ν' sm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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∞)
⊢ ∫⁻ (x : G) in A, (ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
have 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∞) ∂μ'
Tactic: have h1 := measure_mul_lintegral_eq μ' ν' sm (A⁻¹.indicator 1) (measurable_one.indicator hA.inv)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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∞) ∂μ'
⊢ ∫⁻ (x : G) in A, (ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
have 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∞) ∂μ'
Tactic: rw [lintegral_indicator hA.inv] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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∞) ∂μ'
⊢ ∫⁻ (x : G) in A, (ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
have 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 ∂μ'
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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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 ∂μ'
⊢ ∫⁻ (x : G) in A, (ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) ≠ ∞
Tactic: rw [← lintegral_indicator hA, ← h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
have refine : ae μ' ≤ ae ν'
Tactic: refine (ae_measure_preimage_mul_right_lt_top ν' ν' h3s).filter_mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
⊢ ae μ' ≤ ae ν'
have refine : ν' ≠ 0
Tactic: refine (absolutelyContinuous_of_isMulLeftInvariant μ' ν' ?_).ae_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
⊢ ν' ≠ 0
have refine : ν' = 0 → Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine mt ?_ h2s
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
hν : ν' = 0
⊢ Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((0 : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hν, Measure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
hν : ν' = 0
rw : Eq (α := ℝ≥0∞) (((0 : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (0 s) 0
Tactic: rw [hν, Measure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (goal)
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∞)
hν : ν' = 0
rw : Eq (α := ℝ≥0∞) (((0 : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) (0 s) 0
⊢ Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [hν, Measure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Prod (hypothesis)
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
sm : MeasurableSet s
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : G → ℝ≥0∞
hf : Measurable f
g : (y : G) → ℝ≥0∞ :=
  fun (y : G) ↦ HDiv.hDiv (β := ℝ≥0∞) (f y⁻¹) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y⁻¹) ⁻¹' s) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (lintegral ν' g) = ∫⁻ (x : G), f x ∂μ'
have hg : Measurable g
Tactic: have hg : Measurable g :=
    (hf.comp measurable_inv).div ((measurable_measure_mul_right ν' sm).comp measurable_inv)