awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.LIntegral
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : TopologicalSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : μ.IsMulLeftInvariant
inst_6 : μ.Regular
inst_7 : NeZero μ
f : G → ℝ≥0∞
hf : Continuous f
rw : f =ᶠ[ae μ] 0 ↔ f = 0
rw₁ rw₂ : f = 0 ↔ f = 0
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0

Tactic:
rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]

Premises used: MeasureTheory.lintegral_eq_zero_iff, Continuous.ae_eq_iff_eq, continuous_zero, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : μ.IsMulLeftInvariant
g : G
⊢ Measure.map (fun (x : G) ↦ g * x) μ = μ

Tactic:
IsMulLeftInvariant.map_mul_left_eq_self g

Premises used: MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : μ.IsMulRightInvariant
g : G
⊢ Measure.map (fun (x : G) ↦ x * g) μ = μ

Tactic:
IsMulRightInvariant.map_mul_right_eq_self g

Premises used: MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
c : ℝ≥0∞
g : G
rw : HSMul.hSMul (β := Measure G) c (Measure.map (fun (x : G) ↦ g * x) μ) = c • μ
rw₁ rw₂ : c • μ = c • μ
⊢ Measure.map (fun (x : G) ↦ g * x) (c • μ) = c • μ

Tactic:
rw [Measure.map_smul, map_mul_left_eq_self]

Premises used: MeasureTheory.map_mul_left_eq_self, MeasureTheory.Measure.map_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
c : ℝ≥0∞
g : G
rw : HSMul.hSMul (β := Measure G) c (Measure.map (fun (x : G) ↦ x * g) μ) = c • μ
rw₁ rw₂ : c • μ = c • μ
⊢ Measure.map (fun (x : G) ↦ x * g) (c • μ) = c • μ

Tactic:
rw [Measure.map_smul, map_mul_right_eq_self]

Premises used: MeasureTheory.Measure.map_smul, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
c : ℝ≥0
⊢ (c • μ).IsMulLeftInvariant

Tactic:
MeasureTheory.isMulLeftInvariant_smul (c : ℝ≥0∞)

Premises used: ENNReal.ofNNReal, MeasureTheory.isMulLeftInvariant_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Mul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
c : ℝ≥0
⊢ (c • μ).IsMulRightInvariant

Tactic:
MeasureTheory.isMulRightInvariant_smul (c : ℝ≥0∞)

Premises used: ENNReal.ofNNReal, MeasureTheory.isMulRightInvariant_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
g : G
⊢ MeasurePreserving (fun (x : G) ↦ g * x) μ μ

Tactic:
⟨measurable_const_mul g, map_mul_left_eq_self μ g⟩

Premises used: MeasureTheory.map_mul_left_eq_self, MeasureTheory.MeasurePreserving.mk, MeasurableMul.measurable_const_mul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
g : G
X : Type u_3
inst_4 : MeasurableSpace X
μ' : Measure X
f : X → G
hf : MeasurePreserving f μ' μ
⊢ MeasurePreserving (fun (x : X) ↦ g * f x) μ' μ

Tactic:
(measurePreserving_mul_left μ g).comp hf

Premises used: MeasureTheory.measurePreserving_mul_left, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
g : G
⊢ MeasurePreserving (fun (x : G) ↦ x * g) μ μ

Tactic:
⟨measurable_mul_const g, map_mul_right_eq_self μ g⟩

Premises used: MeasureTheory.MeasurePreserving.mk, MeasurableMul.measurable_mul_const, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
g : G
X : Type u_3
inst_4 : MeasurableSpace X
μ' : Measure X
f : X → G
hf : MeasurePreserving f μ' μ
⊢ MeasurePreserving (fun (x : X) ↦ f x * g) μ' μ

Tactic:
(measurePreserving_mul_right μ g).comp hf

Premises used: MeasureTheory.measurePreserving_mul_right, MeasureTheory.MeasurePreserving.comp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G_1 : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G_1
inst_1 : MeasurableSpace H_1
inst_2 : Mul G_1
μ_1 : Measure G_1
inst_3 : MeasurableMul G_1
G : Type u_3
α : Type u_4
inst_4 : Group G
inst_5 : MulAction G α
inst_6 : MeasurableSpace α
μ : Measure α
inst_7 : SMulInvariantMeasure G α μ
H : Subgroup G
y : ↥H
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (↑y : G) • x) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
SMulInvariantMeasure.measure_preimage_smul (μ := μ) (y : G) hs

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, Subtype.val
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G_1 : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G_1
inst_1 : MeasurableSpace H_1
inst_2 : Mul G_1
μ_1 : Measure G_1
inst_3 : MeasurableMul G_1
G : Type u_3
α : Type u_4
inst_4 : Group G
inst_5 : MulAction G α
inst_6 : MeasurableSpace α
μ : Measure α
inst_7 : SMulInvariantMeasure G α μ
H : Subgroup G
y : ↥H
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ y • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
convert! SMulInvariantMeasure.measure_preimage_smul (μ := μ) (y : G) hs

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, Subtype.val
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
trans :
  (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ
trans₁ : (∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ) ↔ μ.IsMulLeftInvariant
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    μ.IsMulLeftInvariant

Tactic:
trans ∀ g, map (g * ·) μ = μ
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
simp_rw :
  (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ

Tactic:
simp_rw [Measure.ext_iff]

Premises used: MeasureTheory.Measure.ext_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_

Premises used: forall_congr'
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
refine :
  ∀ (g : G) (A : Set G) (hA : MeasurableSet A),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
      Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_

Premises used: forall_congr'
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ g * h) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ g * x) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [map_apply (measurable_const_mul g) hA]

Premises used: MeasureTheory.Measure.map_apply, MeasurableMul.measurable_const_mul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ) ↔ μ.IsMulLeftInvariant

Tactic:
⟨fun h => ⟨h⟩, fun h => h.1⟩

Premises used: MeasureTheory.Measure.IsMulLeftInvariant.mk, Iff.intro, MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun (x : G) ↦ g * x) μ = μ) ↔ μ.IsMulLeftInvariant

Tactic:
exact ⟨fun h => ⟨h⟩, fun h => h.1⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
trans :
  (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ
trans₁ : (∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ) ↔ μ.IsMulRightInvariant
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    μ.IsMulRightInvariant

Tactic:
trans ∀ g, map (· * g) μ = μ
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
simp_rw :
  (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ

Tactic:
simp_rw [Measure.ext_iff]

Premises used: MeasureTheory.Measure.ext_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_

Premises used: forall_congr'
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
refine :
  ∀ (g : G) (A : Set G) (hA : MeasurableSet A),
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
      Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
        ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ (∀ (g : G) (A : Set G),
      MeasurableSet A →
        Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)) ↔
    ∀ (g : G) (s : Set G),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
          ((μ : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_

Premises used: forall_congr'
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((fun (h : G) ↦ h * g) ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((Measure.map (fun (x : G) ↦ x * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
      ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [map_apply (measurable_mul_const g) hA]

Premises used: MeasureTheory.Measure.map_apply, MeasurableMul.measurable_mul_const
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ) ↔ μ.IsMulRightInvariant

Tactic:
⟨fun h => ⟨h⟩, fun h => h.1⟩

Premises used: MeasureTheory.Measure.IsMulRightInvariant.mk, MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self, Iff.intro
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
inst_2 : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun (x : G) ↦ x * g) μ = μ) ↔ μ.IsMulRightInvariant

Tactic:
exact ⟨fun h => ⟨h⟩, fun h => h.1⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
map_mul_left_eq_self : ∀ (g : G × H), map (fun (x : G × H) ↦ g * x) (μ.prod ν) = μ.prod ν
⊢ (μ.prod ν).IsMulLeftInvariant

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_left_eq_self : map (Prod.map (fun (x : G) ↦ g * x) fun (x : H) ↦ h * x) (μ.prod ν) = μ.prod ν
⊢ map (fun (x : G × H) ↦ (g, h) * x) (μ.prod ν) = μ.prod ν

Tactic:
change map (Prod.map (g * ·) (h * ·)) (μ.prod ν) = μ.prod ν

Premises used: HMul.hMul, Prod.map, MeasureTheory.Measure.prod, MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulLeftInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulLeftInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_left_eq_self : Measure.prod (map (fun (x : G) ↦ g * x) μ) (map (fun (x : H) ↦ h * x) ν) = μ.prod ν
map_mul_left_eq_self₁ : μ.prod (map (fun (x : H) ↦ h * x) ν) = μ.prod ν
map_mul_left_eq_self₂ map_mul_left_eq_self₃ : μ.prod ν = μ.prod ν
⊢ map (Prod.map (fun (x : G) ↦ g * x) fun (x : H) ↦ h * x) (μ.prod ν) = μ.prod ν

Tactic:
rw [← map_prod_map _ _ (measurable_const_mul g) (measurable_const_mul h),
    map_mul_left_eq_self μ g, map_mul_left_eq_self ν h]

Premises used: MeasureTheory.map_mul_left_eq_self, MeasurableMul.measurable_const_mul, MeasureTheory.Measure.map_prod_map
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
map_mul_right_eq_self : ∀ (g : G × H), map (fun (x : G × H) ↦ x * g) (μ.prod ν) = μ.prod ν
⊢ (μ.prod ν).IsMulRightInvariant

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_right_eq_self : map (Prod.map (fun (x : G) ↦ x * g) fun (x : H) ↦ x * h) (μ.prod ν) = μ.prod ν
⊢ map (fun (x : G × H) ↦ x * (g, h)) (μ.prod ν) = μ.prod ν

Tactic:
change map (Prod.map (· * g) (· * h)) (μ.prod ν) = μ.prod ν

Premises used: HMul.hMul, Prod.map, MeasureTheory.Measure.prod, MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Mul G
μ : Measure G
inst_3 : MeasurableMul G
inst_4 : μ.IsMulRightInvariant
inst_5 : SFinite μ
H : Type u_3
inst_6 : Mul H
mH : MeasurableSpace H
ν : Measure H
inst_7 : MeasurableMul H
inst_8 : ν.IsMulRightInvariant
inst_9 : SFinite ν
g : G
h : H
map_mul_right_eq_self : Measure.prod (map (fun (x : G) ↦ x * g) μ) (map (fun (x : H) ↦ x * h) ν) = μ.prod ν
map_mul_right_eq_self₁ : μ.prod (map (fun (x : H) ↦ x * h) ν) = μ.prod ν
map_mul_right_eq_self₂ map_mul_right_eq_self₃ : μ.prod ν = μ.prod ν
⊢ map (Prod.map (fun (x : G) ↦ x * g) fun (x : H) ↦ x * h) (μ.prod ν) = μ.prod ν

Tactic:
rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h),
    map_mul_right_eq_self μ g, map_mul_right_eq_self ν h]

Premises used: MeasureTheory.Measure.map_prod_map, MeasurableMul.measurable_mul_const, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ IsMulLeftInvariant.{u_3} (G := H) (Measure.map (⇑f : (a : G) → H) μ)

Tactic:
⟨fun h => ?_⟩

Premises used: MeasureTheory.Measure.IsMulLeftInvariant.mk
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
refine :
  ∀ (h : H),
    Eq.{u_3 + 1} (α := Measure H) (Measure.map (fun (x : H) ↦ h * x) (Measure.map (⇑f : (a : G) → H) μ))
      (Measure.map (⇑f : (a : G) → H) μ)
⊢ IsMulLeftInvariant.{u_3} (G := H) (Measure.map (⇑f : (a : G) → H) μ)

Tactic:
refine ⟨fun h => ?_⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : H
rw :
  Eq.{u_3 + 1} (α := Measure H) (Measure.map ((fun (x : H) ↦ h * x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (⇑f : (a : G) → H) μ)
⊢ Eq.{u_3 + 1} (α := Measure H) (Measure.map (fun (x : H) ↦ h * x) (Measure.map (⇑f : (a : G) → H) μ))
    (Measure.map (⇑f : (a : G) → H) μ)

Tactic:
rw [map_map (measurable_const_mul _) hf]

Premises used: MeasurableMul.measurable_const_mul, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h : H
obtain :
  ∀ (g : G),
    Eq.{u_3 + 1} (α := Measure H)
      (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
      (Measure.map (⇑f : (a : G) → H) μ)
⊢ Eq.{u_3 + 1} (α := Measure H) (Measure.map ((fun (x : H) ↦ h * x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (⇑f : (a : G) → H) μ)

Tactic:
obtain ⟨g, rfl⟩ := h_surj h

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
rw : Measure.map (α := G) (⇑f : (a : G) → H) (Measure.map (fun (x : G) ↦ g * x) μ)
| Measure.map (⇑f : (a : G) → H) μ

Tactic:
rw [← map_mul_left_eq_self μ g]

Premises used: MeasureTheory.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Mul G
μ : Measure G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : MeasurableSpace H
inst_4 : Mul H
inst_5 : MeasurableMul H
inst_6 : μ.IsMulLeftInvariant
f : G →ₙ* H
hf : Measurable.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
h_surj : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
conv_rhs :
  Eq.{u_3 + 1} (α := Measure H)
    (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (α := G) (⇑f : (a : G) → H) (Measure.map (fun (x : G) ↦ g * x) μ))
⊢ Eq.{u_3 + 1} (α := Measure H)
    (Measure.map ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) μ)
    (Measure.map (⇑f : (a : G) → H) μ)

Tactic:
conv_rhs => rw [← map_mul_left_eq_self μ g]

Premises used: MeasureTheory.map_mul_left_eq_self