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
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∞)
inr₂ 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∞)

Tactic:
rw [← hμ, ← hν, this _ hm]
-- Module: Mathlib.MeasureTheory.Group.Prod
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∞) ((ν' : (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)
-- Module: Mathlib.MeasureTheory.Group.Prod
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∞) ((μ' : (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)
-- Module: Mathlib.MeasureTheory.Group.Prod
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∞) ((ν' : (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

Premises used: MeasureTheory.setLIntegral_one, MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Group.Prod
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∞) ((μ' : (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

Premises used: MeasureTheory.setLIntegral_one, MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Group.Prod
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∞)
rw₂ 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∞)
⊢ 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]

Premises used: mul_left_comm
-- 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∞)
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∞)
⊢ μ' = HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((ν' : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) • ν'

Tactic:
ext1 t -
-- 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∞)
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∞)
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∞))
h₇ h₈ : Eq (α := ℝ≥0∞) ((μ' : (a : Set G) → ℝ≥0∞) t : ℝ≥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∞)

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]

Premises used: MeasureTheory.measure_mul_measure_eq, mul_div_assoc, ENNReal.mul_div_cancel, MeasureTheory.Measure.smul_apply, mul_comm, smul_eq_mul
-- 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 : ν.IsMulRightInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1, z.2 * z.1)) (μ.prod ν) (μ.prod ν)

Tactic:
MeasurePreserving.skew_product (g := fun x y => y * x) (MeasurePreserving.id μ)
    (measurable_snd.mul measurable_fst) <| Filter.Eventually.of_forall <| map_mul_right_eq_self ν

Premises used: Measurable.mul, Filter.Eventually.of_forall, measurable_snd, MeasureTheory.MeasurePreserving.skew_product, MeasureTheory.MeasurePreserving.id, measurable_fst, MeasureTheory.map_mul_right_eq_self
-- 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 : μ.IsMulRightInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.2, z.1 * z.2)) (μ.prod ν) (ν.prod μ)

Tactic:
(measurePreserving_prod_mul_right ν μ).comp measurePreserving_swap

Premises used: MeasureTheory.MeasurePreserving.comp, MeasureTheory.Measure.measurePreserving_swap, MeasureTheory.measurePreserving_prod_mul_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 μ
inst_5 : μ.IsMulRightInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1 * z.2, z.2)) (μ.prod ν) (μ.prod ν)

Tactic:
measurePreserving_swap.comp (measurePreserving_prod_mul_swap_right μ ν)

Premises used: MeasureTheory.measurePreserving_prod_mul_swap_right, Prod.swap, MeasureTheory.MeasurePreserving.comp, MeasureTheory.Measure.measurePreserving_swap
-- 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 : ν.IsMulRightInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1, z.2 / z.1)) (μ.prod ν) (μ.prod ν)

Tactic:
(measurePreserving_prod_mul_right μ ν).symm (MeasurableEquiv.shearDivRight G).symm

Premises used: MeasureTheory.MeasurePreserving.symm, MeasurableEquiv.symm, MeasurableEquiv.shearDivRight, MeasureTheory.measurePreserving_prod_mul_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 μ
inst_5 : MeasurableInv G
inst_6 : μ.IsMulRightInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.2, z.1 / z.2)) (μ.prod ν) (ν.prod μ)

Tactic:
(measurePreserving_prod_div ν μ).comp measurePreserving_swap

Premises used: MeasureTheory.measurePreserving_prod_div, MeasureTheory.MeasurePreserving.comp, MeasureTheory.Measure.measurePreserving_swap
-- 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 : μ.IsMulRightInvariant
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1 / z.2, z.2)) (μ.prod ν) (μ.prod ν)

Tactic:
measurePreserving_swap.comp (measurePreserving_prod_div_swap μ ν)

Premises used: MeasureTheory.measurePreserving_prod_div_swap, Prod.swap, MeasureTheory.MeasurePreserving.comp, MeasureTheory.Measure.measurePreserving_swap
-- 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 : μ.IsMulRightInvariant
inst_7 : ν.IsMulRightInvariant
⊢ MeasurePreserving ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (μ.prod ν) (μ.prod ν)

Tactic:
(measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν)

Premises used: MeasureTheory.measurePreserving_prod_mul_swap_right, MeasureTheory.measurePreserving_prod_div_swap, MeasureTheory.MeasurePreserving.comp
-- 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 : μ.IsMulRightInvariant
inst_7 : ν.IsMulRightInvariant
h :
  Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.1 * z.2, z.1⁻¹))
    ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2))
⊢ MeasurePreserving (fun (z : G × G) ↦ (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Tactic:
convert!
    (measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν) using 1

Premises used: MeasureTheory.measurePreserving_prod_mul_swap_right, MeasureTheory.measurePreserving_prod_div_swap, MeasureTheory.MeasurePreserving.comp
-- 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 : μ.IsMulRightInvariant
inst_7 : ν.IsMulRightInvariant
h :
  ∀ (x y : G),
    ((x, y).1 * (x, y).2, (x, y).1⁻¹) =
      ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
⊢ Eq.{u_1 + 1} (α := G × G → G × G) (fun (z : G × G) ↦ (z.1 * z.2, z.1⁻¹))
    ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2))

Tactic:
ext1 ⟨x, y⟩
-- 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 : μ.IsMulRightInvariant
inst_7 : ν.IsMulRightInvariant
x y : G
h h₁ : (x * y, x⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)
h₂ : (x * y, x⁻¹) = (x * y, y / (x * y))
h₃ : (x * y, x⁻¹) = (x * y, y / y / x)
h₄ : (x * y, x⁻¹) = (x * y, 1 / x)
⊢ ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun (z : G × G) ↦ (z.2, z.1 / z.2)) ∘ fun (z : G × G) ↦ (z.2, z.1 * z.2)) (x, y)

Tactic:
simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]

Premises used: div_mul_eq_div_div_swap, div_self', one_div, Function.comp_apply
-- 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 : ν.IsMulLeftInvariant
⊢ QuasiMeasurePreserving (fun (p : G × G) ↦ p.1 * p.2) (μ.prod ν) ν

Tactic:
quasiMeasurePreserving_snd.comp (measurePreserving_prod_mul _ _).quasiMeasurePreserving

Premises used: MeasureTheory.Measure.quasiMeasurePreserving_snd, MeasureTheory.Measure.QuasiMeasurePreserving.comp, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.measurePreserving_prod_mul
-- 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 : μ.IsMulLeftInvariant
⊢ QuasiMeasurePreserving (fun (p : G × G) ↦ p.2 * p.1) (μ.prod ν) μ

Tactic:
quasiMeasurePreserving_snd.comp (measurePreserving_prod_mul_swap _ _).quasiMeasurePreserving

Premises used: MeasureTheory.measurePreserving_prod_mul_swap, MeasureTheory.Measure.quasiMeasurePreserving_snd, MeasureTheory.Measure.QuasiMeasurePreserving.comp, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- 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
⊢ QuasiMeasurePreserving (fun (p : G × G) ↦ p.1⁻¹ * p.2) (μ.prod ν) ν

Tactic:
quasiMeasurePreserving_snd.comp (measurePreserving_prod_inv_mul _ _).quasiMeasurePreserving

Premises used: MeasureTheory.Measure.quasiMeasurePreserving_snd, MeasureTheory.Measure.QuasiMeasurePreserving.comp, MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.measurePreserving_prod_inv_mul
-- 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
⊢ QuasiMeasurePreserving (fun (p : G × G) ↦ p.2⁻¹ * p.1) (μ.prod ν) μ

Tactic:
quasiMeasurePreserving_snd.comp (measurePreserving_prod_inv_mul_swap _ _).quasiMeasurePreserving

Premises used: MeasureTheory.measurePreserving_prod_inv_mul_swap, MeasureTheory.Measure.quasiMeasurePreserving_snd, MeasureTheory.Measure.QuasiMeasurePreserving.comp, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- 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 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
rw : QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv
⊢ QuasiMeasurePreserving Inv.inv μ μ

Tactic:
rw [← μ.inv_inv]

Premises used: MeasureTheory.Measure.inv_inv
-- 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 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv

Tactic:
(quasiMeasurePreserving_inv μ.inv).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)

Premises used: MeasureTheory.inv_absolutelyContinuous, MeasureTheory.absolutelyContinuous_inv, MeasureTheory.quasiMeasurePreserving_inv, MeasureTheory.Measure.inv, MeasureTheory.Measure.QuasiMeasurePreserving.mono
-- 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 : MeasurableInv G
inst_5 : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving Inv.inv μ.inv.inv μ.inv.inv

Tactic:
exact
    (quasiMeasurePreserving_inv μ.inv).mono (inv_absolutelyContinuous μ.inv)
      (absolutelyContinuous_inv μ.inv)

Premises used: MeasureTheory.inv_absolutelyContinuous, MeasureTheory.absolutelyContinuous_inv, MeasureTheory.quasiMeasurePreserving_inv, MeasureTheory.Measure.inv, MeasureTheory.Measure.QuasiMeasurePreserving.mono
-- 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 : MeasurableInv G
inst_5 : μ.IsMulLeftInvariant
g : G
simp_rw : QuasiMeasurePreserving (fun (h : G) ↦ g * h⁻¹) μ μ
⊢ QuasiMeasurePreserving (fun (h : G) ↦ g / h) μ μ

Tactic:
simp_rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv