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
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∞)
hg : Measurable g
⊢ HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (lintegral ν' g) = ∫⁻ (x : G), f x ∂μ'
have simp_rw : ∫⁻ (x : G),
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞) (f x) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)) ∂μ' =
  ∫⁻ (x : G), f x ∂μ'
Tactic: simp_rw [measure_mul_lintegral_eq μ' ν' sm g hg, g, inv_inv]
-- 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
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∞)
hg : Measurable g
⊢ ∫⁻ (x : G),
      HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (HDiv.hDiv (β := ℝ≥0∞) (f x) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)) ∂μ' =
    ∫⁻ (x : G), f x ∂μ'
have refine : (fun (x : G) ↦
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞) (f x) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞))) =ᶠ[ae μ']
  f
Tactic: refine lintegral_congr_ae ?_
-- 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
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∞)
hg : Measurable g
⊢ (fun (x : G) ↦
      HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
        (HDiv.hDiv (β := ℝ≥0∞) (f x) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞))) =ᶠ[ae μ']
    f
have refine : ∀ (x : G) (hx : LT.lt (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (y : G) ↦ y * x) ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (fun (x : G) ↦
        HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)
          (HDiv.hDiv (β := ℝ≥0∞) (f x) ((ν' : (a : Set G) → ℝ≥0∞) ((fun (z : G) ↦ z * x) ⁻¹' s) : ℝ≥0∞)))
      x =
    f x
Tactic: refine (ae_measure_preimage_mul_right_lt_top_of_ne_zero μ' ν' h2s h3s).mono fun x 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s t : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have inr : ∀
  (this :
    ∀ (s : Set G) (h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
      (h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hs : MeasurableSet s),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
  (hs : ¬MeasurableSet s),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: wlog hs : 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s t : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inr :
  ∀
    (this :
      ∀ (s : Set G) (h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
        (h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hs : MeasurableSet s),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
    (hs : ¬MeasurableSet s),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have wlog : ∀ (s : Set G) (h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
  (h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hs : MeasurableSet s),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: wlog hs : MeasurableSet s generalizing s
Cleared hypotheses: s, h2s, h3s
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s t : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ (s : Set G) (h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hs : MeasurableSet s),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
hs : ¬MeasurableSet s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have inr : ∀ (s' : Set G) (hm : MeasurableSet s')
  (hμ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
  (hν : Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rcases exists_measurable_superset₂ μ' ν' s with ⟨s', -, hm, hμ, hν⟩
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s t : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ (s : Set G) (h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hs : MeasurableSet s),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← hμ, ← hν, this s' _ _ hm]
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s t : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ (s : Set G) (h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞))
    (h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hs : MeasurableSet s),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
rw : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s' : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← hμ, ← hν, this s' _ _ hm]
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
t s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have inr : ∀
  (this :
    ∀ (t : Set G) (ht : MeasurableSet t),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
  (ht : ¬MeasurableSet t),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: wlog ht : MeasurableSet t generalizing t
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
t s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
inr :
  ∀
    (this :
      ∀ (t : Set G) (ht : MeasurableSet t),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
    (ht : ¬MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have wlog : ∀ (t : Set G) (ht : MeasurableSet t),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: wlog ht : MeasurableSet t generalizing t
Cleared hypotheses: t
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
t s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
this :
  ∀ (t : Set G) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
ht : ¬MeasurableSet t
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have inr : ∀ (t' : Set G) (hm : MeasurableSet t')
  (hμ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
  (hν : Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rcases exists_measurable_superset₂ μ' ν' t with ⟨t', -, hm, hμ, hν⟩
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
t s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
this :
  ∀ (t : Set G) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have inr : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞)
Tactic: rw [← hμ, ← hν, this _ hm]
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
t s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
this :
  ∀ (t : Set G) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
inr :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have inr₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞)
Tactic: rw [← hμ, ← hν, this _ hm]
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
t s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
this :
  ∀ (t : Set G) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
ht : ¬MeasurableSet t
t' : Set G
hm : MeasurableSet t'
hμ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
hν : Eq (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
inr :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞)
inr₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have inr₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t' : ℝ≥0∞)
Tactic: rw [← hμ, ← hν, this _ hm]
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have h1 : HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∫⁻ (y : G),
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) (t.indicator (fun (x : G) ↦ 1) y⁻¹ : ℝ≥0∞)
        ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y⁻¹) ⁻¹' s) : ℝ≥0∞) ∂ν') =
  ∫⁻ (x : G), t.indicator (fun (x : G) ↦ 1) x ∂ν'
Tactic: have h1 := measure_lintegral_div_measure ν' ν' hs h2s h3s (t.indicator fun _ => 1)
    (measurable_const.indicator ht)
-- 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
inst_3 : MeasurableInv G
μ' ν' : Measure G
inst_4 : SigmaFinite μ'
inst_5 : SigmaFinite ν'
inst_6 : μ'.IsMulLeftInvariant
inst_7 : ν'.IsMulLeftInvariant
s : Set G
h2s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h3s : Ne (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 :
  HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (∫⁻ (y : G),
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) (t.indicator (fun (x : G) ↦ 1) y⁻¹ : ℝ≥0∞)
          ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y⁻¹) ⁻¹' s) : ℝ≥0∞) ∂ν') =
    ∫⁻ (x : G), t.indicator (fun (x : G) ↦ 1) x ∂ν'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
have h2 : HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (∫⁻ (y : G),
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) (t.indicator (fun (x : G) ↦ 1) y⁻¹ : ℝ≥0∞)
        ((ν' : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * y⁻¹) ⁻¹' s) : ℝ≥0∞) ∂ν') =
  ∫⁻ (x : G), t.indicator (fun (x : G) ↦ 1) x ∂μ'
Tactic: have h2 := measure_lintegral_div_measure μ' ν' hs h2s h3s (t.indicator fun _ => 1)
    (measurable_const.indicator ht)