awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∂ν'
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 ∂μ'
⊢ 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∞) ∂ν') =
  (ν' : (a : Set G) → ℝ≥0∞) t
Tactic: rw [lintegral_indicator ht, setLIntegral_one] at h1 h2
Cleared hypotheses: h1, h2
-- 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 ∂ν'
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 ∂μ'
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∞) ∂ν') =
    (ν' : (a : Set G) → ℝ≥0∞) 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 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∞) ∂ν') =
  (μ' : (a : Set G) → ℝ≥0∞) t
Tactic: rw [lintegral_indicator ht, setLIntegral_one] at h1 h2
Cleared hypotheses: h1, h2
-- 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 : 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∞) ∂ν') =
    (ν' : (a : Set G) → ℝ≥0∞) t
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∞) ∂ν') =
    (μ' : (a : Set G) → ℝ≥0∞) 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 rw : HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (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∞) ∂ν')) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [← h1, mul_left_comm, h2]
-- 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 : 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∞) ∂ν') =
    (ν' : (a : Set G) → ℝ≥0∞) t
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∞) ∂ν') =
    (μ' : (a : Set G) → ℝ≥0∞) t
rw :
  HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (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∞) ∂ν')) =
    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 rw₁ : HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (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∞) ∂ν')) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [← h1, mul_left_comm, h2]
-- 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 : 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∞) ∂ν') =
    (ν' : (a : Set G) → ℝ≥0∞) t
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∞) ∂ν') =
    (μ' : (a : Set G) → ℝ≥0∞) t
rw :
  HMul.hMul (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (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∞) ∂ν')) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (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∞) ∂ν')) =
    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 rw₂ : 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 [← h1, mul_left_comm, h2]
-- 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∞)
⊢ μ' = HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν'
have h : ∀ (t : Set G),
  Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
Tactic: ext1 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
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∞)
t : Set G
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h : (μ' : (a : Set G) → ℝ≥0∞) t =
  HSMul.hSMul (β := ℝ≥0∞)
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel 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
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∞)
t : Set G
h :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HSMul.hSMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h₁ : (μ' : (a : Set G) → ℝ≥0∞) t =
  HMul.hMul (β := ℝ≥0∞)
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel 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
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∞)
t : Set G
h :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HSMul.hSMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h₂ : (μ' : (a : Set G) → ℝ≥0∞) t =
  HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel 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
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∞)
t : Set G
h :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HSMul.hSMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₂ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h₃ : (μ' : (a : Set G) → ℝ≥0∞) t =
  HDiv.hDiv (β := ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
    ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel 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
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∞)
t : Set G
h :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HSMul.hSMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₂ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
h₃ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h₄ : (μ' : (a : Set G) → ℝ≥0∞) t =
  HDiv.hDiv (β := ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
    ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel 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
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∞)
t : Set G
h :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HSMul.hSMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₂ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
h₃ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
h₄ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h₅ : (μ' : (a : Set G) → ℝ≥0∞) t =
  HDiv.hDiv (β := ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
    ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel 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
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∞)
t : Set G
h :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HSMul.hSMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (β := ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
h₂ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
h₃ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
h₄ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
h₅ :
  (μ' : (a : Set G) → ℝ≥0∞) t =
    HDiv.hDiv (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞))
      ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞)
    ((HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν' :
          (a : Set G) → ℝ≥0∞)
        t :
      ℝ≥0∞)
have h₆ : (μ' : (a : Set G) → ℝ≥0∞) t =
  HMul.hMul (α := ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞))
Tactic: rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel h2s h3s]