awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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 (comp (β := G) (⇑f : (a : G) → H) 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 (α := G) (⇑f : (a : G) → H) (Measure.map (fun (x : G) ↦ g * x) μ))

Tactic:
rw [map_map hf (measurable_const_mul _)]

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)
g : G
e_f :
  Eq (α := G → H) ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H))
    (comp (β := G) (⇑f : (a : G) → H) 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 (comp (β := G) (⇑f : (a : G) → H) fun (x : G) ↦ g * x) μ)

Tactic:
congr 2
-- 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
e_f :
  ∀ (y : G),
    Eq.{u_3 + 1} (α := H) (((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) y)
      (comp (β := G) (⇑f : (a : G) → H) (fun (x : G) ↦ g * x) y)
⊢ Eq (α := G → H) ((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H))
    (comp (β := G) (⇑f : (a : G) → H) fun (x : G) ↦ g * x)

Tactic:
ext y
-- 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 y : G
⊢ Eq.{u_3 + 1} (α := H) (((fun (x : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) g : H) x) ∘ (⇑f : (a : G) → H)) y)
    (comp (β := G) (⇑f : (a : G) → H) (fun (x : G) ↦ g * x) y)

Tactic:
simp only [comp_apply, map_mul]

Premises used: map_mul, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Semigroup G
inst_2 : MeasurableMul G
μ : Measure G
α : Type u_3
inst_3 : SMul α G
inst_4 : SMulCommClass α G G
inst_5 : MeasurableConstSMul α G
inst_6 : μ.IsMulLeftInvariant
a : α
⊢ IsMulLeftInvariant (G := G) (Measure.map (fun (x : G) ↦ a • x) μ)

Tactic:
(forall_measure_preimage_mul_iff _).1 fun x _ hs =>
    (smulInvariantMeasure_map_smul μ a).measure_preimage_smul x hs

Premises used: MeasureTheory.forall_measure_preimage_mul_iff, MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, Iff.mp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Semigroup G
inst_2 : MeasurableMul G
μ : Measure G
α : Type u_3
inst_3 : SMul α G
inst_4 : SMulCommClass α Gᵐᵒᵖ G
inst_5 : MeasurableConstSMul α G
inst_6 : μ.IsMulRightInvariant
a : α
⊢ IsMulRightInvariant (G := G) (Measure.map (fun (x : G) ↦ a • x) μ)

Tactic:
(forall_measure_preimage_mul_right_iff _).1 fun x _ hs =>
    (smulInvariantMeasure_map_smul μ a).measure_preimage_smul (MulOpposite.op x) hs

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, Iff.mp, MulOpposite.op, MeasureTheory.forall_measure_preimage_mul_right_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Semigroup G
inst_3 : MeasurableMul G
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
g : G
⊢ IsMulLeftInvariant (G := G) (Measure.map (fun (x : G) ↦ x * g) μ)

Tactic:
isMulLeftInvariant_map_smul (MulOpposite.op g)

Premises used: MeasureTheory.isMulLeftInvariant_map_smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Semigroup G
inst_3 : MeasurableMul G
μ : Measure G
inst_4 : μ.IsMulRightInvariant
g : G
⊢ IsMulRightInvariant (G := G) (Measure.map (fun (x : G) ↦ g * x) μ)

Tactic:
isMulRightInvariant_map_smul g

Premises used: MeasureTheory.isMulRightInvariant_map_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : DivInvMonoid G
μ : Measure G
inst_2 : μ.IsMulRightInvariant
g : G
simp_rw : Measure.map (fun (x : G) ↦ x * g⁻¹) μ = μ
⊢ Measure.map (fun (x : G) ↦ x / g) μ = μ

Tactic:
simp_rw [div_eq_mul_inv, map_mul_right_eq_self μ g⁻¹]

Premises used: div_eq_mul_inv, Inv.inv, MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
g : G
simp_rw : MeasurePreserving (fun (x : G) ↦ x * g⁻¹) μ μ
⊢ MeasurePreserving (fun (x : G) ↦ x / g) μ μ

Tactic:
simp_rw [div_eq_mul_inv, measurePreserving_mul_right μ g⁻¹]

Premises used: div_eq_mul_inv, Inv.inv, MeasureTheory.measurePreserving_mul_right
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
g : G
A : Set G
rw rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (h : G) ↦ g * h) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

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 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
g : G
A : Set G
rw rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (h : G) ↦ h * g) μ : Measure G) : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [map_mul_right_eq_self μ g]

Premises used: MeasureTheory.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
x : G
⊢ Filter.map (fun (h : G) ↦ x * h) (ae μ) = ae μ

Tactic:
((MeasurableEquiv.mulLeft x).map_ae μ).trans <| congr_arg ae <| map_mul_left_eq_self μ x

Premises used: MeasurableEquiv.mulLeft, MeasureTheory.ae, MeasureTheory.map_mul_left_eq_self, congr_arg, MeasurableEquiv.map_ae, Eq.trans
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
x : G
⊢ Filter.map (fun (h : G) ↦ h * x) (ae μ) = ae μ

Tactic:
((MeasurableEquiv.mulRight x).map_ae μ).trans <| congr_arg ae <| map_mul_right_eq_self μ x

Premises used: MeasureTheory.ae, MeasurableEquiv.mulRight, congr_arg, MeasurableEquiv.map_ae, MeasureTheory.map_mul_right_eq_self, Eq.trans
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
x : G
⊢ Filter.map (fun (t : G) ↦ t / x) (ae μ) = ae μ

Tactic:
((MeasurableEquiv.divRight x).map_ae μ).trans <| congr_arg ae <| map_div_right_eq_self μ x

Premises used: MeasureTheory.ae, MeasureTheory.map_div_right_eq_self, congr_arg, MeasurableEquiv.divRight, MeasurableEquiv.map_ae, Eq.trans
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
t : G
p : G → Prop
rw : Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ t * h) (ae μ)) {x : G | p x}
| ∀ᵐ (x : G) ∂μ, p x

Tactic:
rw [Filter.Eventually, ← map_mul_left_ae μ t]

Premises used: MeasureTheory.map_mul_left_ae, Filter.Eventually
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
t : G
p : G → Prop
conv_rhs :
  (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ t * h) (ae μ)) {x : G | p x}
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
conv_rhs => rw [Filter.Eventually, ← map_mul_left_ae μ t]

Premises used: MeasureTheory.map_mul_left_ae, Filter.Eventually
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (t * x)) ↔ Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ t * h) (ae μ)) {x : G | p x}

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
rw : Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ h * t) (ae μ)) {x : G | p x}
| ∀ᵐ (x : G) ∂μ, p x

Tactic:
rw [Filter.Eventually, ← map_mul_right_ae μ t]

Premises used: Filter.Eventually, MeasureTheory.map_mul_right_ae
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
conv_rhs :
  (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ h * t) (ae μ)) {x : G | p x}
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
conv_rhs => rw [Filter.Eventually, ← map_mul_right_ae μ t]

Premises used: Filter.Eventually, MeasureTheory.map_mul_right_ae
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ Membership.mem (γ := Filter G) (Filter.map (fun (h : G) ↦ h * t) (ae μ)) {x : G | p x}

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
rw : Membership.mem (γ := Filter G) (Filter.map (fun (t_1 : G) ↦ t_1 / t) (ae μ)) {x : G | p x}
| ∀ᵐ (x : G) ∂μ, p x

Tactic:
rw [Filter.Eventually, ← map_div_right_ae μ t]

Premises used: Filter.Eventually, MeasureTheory.map_div_right_ae
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
conv_rhs :
  (∀ᵐ (x : G) ∂μ, p (x / t)) ↔
    Membership.mem (γ := Filter G) (Filter.map (fun (t_1 : G) ↦ t_1 / t) (ae μ)) {x : G | p x}
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
conv_rhs => rw [Filter.Eventually, ← map_div_right_ae μ t]

Premises used: Filter.Eventually, MeasureTheory.map_div_right_ae
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
μ : Measure G
inst_3 : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x / t)) ↔
    Membership.mem (γ := Filter G) (Filter.map (fun (t_1 : G) ↦ t_1 / t) (ae μ)) {x : G | p x}

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
obtain :
  ∀ (s : Set G) (hs : Subgroup.IsComplement s (↑H : Set G)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
      (μ : (a : Set G) → ℝ≥0∞) univ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ

Tactic:
obtain ⟨s, hs, -⟩ := H.exists_isComplement_left 1

Premises used: Subgroup.exists_isComplement_left, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have hs' : Finite s := hs.finite_left_iff.mpr inferInstance
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    ∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G))

Tactic:
simp [measure_smul, hs.encard_left]

Premises used: Subgroup.IsComplement.encard_left, MeasureTheory.measure_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (⋃ (i : (↑s : Type u_1)), (↑i : G) • (↑H : Set G)) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ :
  Pairwise.{u_1} (α := (↑s : Type u_1))
    (onFun (β := Set G) Disjoint fun (x : (↑s : Type u_1)) ↦ (↑x : G) • (↑H : Set G))
⊢ Eq (α := ℝ≥0∞) (∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G)) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]

Premises used: MeasureTheory.measure_iUnion, MeasurableSet.const_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (⋃ (i : (↑s : Type u_1)), (↑i : G) • (↑H : Set G)) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp [hs.mul_eq]

Premises used: Subgroup.IsComplement.mul_eq
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Pairwise.{u_1} (α := (↑s : Type u_1))
    (onFun (β := Set G) Disjoint fun (x : (↑s : Type u_1)) ↦ (↑x : G) • (↑H : Set G))

Tactic:
fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)

Premises used: Subtype.val_injective, Function.Injective.ne, Subgroup.IsComplement.pairwiseDisjoint_smul, Pairwise, Subtype.property
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Pairwise.{u_1} (α := (↑s : Type u_1))
    (onFun (β := Set G) Disjoint fun (x : (↑s : Type u_1)) ↦ (↑x : G) • (↑H : Set G))

Tactic:
exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)

Premises used: Subtype.val_injective, Function.Injective.ne, Subgroup.IsComplement.pairwiseDisjoint_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Subgroup G
inst_3 : H.FiniteIndex
hH : MeasurableSet (↑H : Set G)
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
s : Set G
hs : Subgroup.IsComplement s (↑H : Set G)
hs' : Finite.{u_1 + 1} (↑s : Type u_1)
μ₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    ∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G))
μ₂ :
  Eq (α := ℝ≥0∞) (∑' (a : (↑s : Type u_1)), (μ : (a : Set G) → ℝ≥0∞) ((↑a : G) • (↑H : Set G)) : ℝ≥0∞)
    ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑H.index : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑H : Set G) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ

Tactic:
calc
    H.index * μ H = ∑' a : s, μ (a.val • H) := by simp [measure_smul, hs.encard_left]
    _ = μ univ := by
      rw [← measure_iUnion _ fun _ ↦ hH.const_smul _]
      · simp [hs.mul_eq]
      · exact fun a b hab ↦ hs.pairwiseDisjoint_smul a.2 b.2 (Subtype.val_injective.ne hab)

Premises used: Set.univ, SetLike.coe, Subgroup.index, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Inv G
μ : Measure G
⊢ μ.inv = map inv μ

Tactic:
rfl

Premises used: MeasureTheory.Measure.inv, rfl
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Inv G
μ : Measure G
inst_2 : μ.IsInvInvariant
⊢ μ.inv = μ

Tactic:
IsInvInvariant.inv_eq_self

Premises used: MeasureTheory.Measure.IsInvInvariant.inv_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Inv G
μ : Measure G
inst_2 : μ.IsInvInvariant
⊢ map inv μ = μ

Tactic:
IsInvInvariant.inv_eq_self

Premises used: MeasureTheory.Measure.IsInvInvariant.inv_eq_self, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Inv G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsInvInvariant
⊢ MeasurePreserving inv μ μ

Tactic:
⟨measurable_inv, map_inv_eq_self μ⟩

Premises used: MeasureTheory.MeasurePreserving.mk, MeasurableInv.measurable_inv, MeasureTheory.Measure.map_inv_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 : Inv G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
⊢ SFinite (m0 := inst) (map inv μ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : InvolutiveInv G
inst_2 : MeasurableInv G
μ : Measure G
s : Set G
⊢ Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) s⁻¹ : ℝ≥0∞)

Tactic:
(MeasurableEquiv.inv G).map_apply s

Premises used: MeasurableEquiv.map_apply, MeasurableEquiv.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : InvolutiveInv G
inst_2 : MeasurableInv G
μ : Measure G
⊢ μ.inv.inv = μ

Tactic:
(MeasurableEquiv.inv G).map_symm_map

Premises used: MeasurableEquiv.inv, MeasurableEquiv.map_symm_map, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : InvolutiveInv G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsInvInvariant
A : Set G
rw : Eq (α := ℝ≥0∞) ((μ.inv : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A⁻¹ : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [← inv_apply, inv_eq_self]

Premises used: MeasureTheory.Measure.inv_eq_self, MeasureTheory.Measure.inv_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : InvolutiveInv G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsInvInvariant
A : Set G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (inv ⁻¹' A) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
μ.measure_inv A

Premises used: MeasureTheory.Measure.measure_inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : InvolutiveInv G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SigmaFinite μ
⊢ SigmaFinite μ.inv

Tactic:
(MeasurableEquiv.inv G).sigmaFinite_map

Premises used: MeasurableEquiv.inv, MeasurableEquiv.sigmaFinite_map, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
map_mul_right_eq_self : ∀ (g : G), map (fun (x : G) ↦ x * g) μ.inv = μ.inv
⊢ μ.inv.IsMulRightInvariant

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
rw : Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ)
| μ.inv

Tactic:
rw [← map_mul_left_eq_self μ g⁻¹]

Premises used: MeasureTheory.map_mul_left_eq_self, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
map_mul_right_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
⊢ map (fun (x : G) ↦ x * g) μ.inv = μ.inv

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

Premises used: MeasureTheory.map_mul_left_eq_self, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : DivisionMonoid G
inst_3 : MeasurableMul G
inst_4 : MeasurableInv G
μ : Measure G
inst_5 : μ.IsMulLeftInvariant
g : G
map_mul_right_eq_self :
  Eq (α := Measure G) (map (fun (x : G) ↦ x * g) (map inv μ)) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
map_mul_right_eq_self₁ :
  Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map inv (map (fun (x : G) ↦ g⁻¹ * x) μ))
map_mul_right_eq_self₂ : Eq (α := Measure G) (map ((fun (x : G) ↦ x * g) ∘ inv) μ) (map (inv ∘ fun (x : G) ↦ g⁻¹ * x) μ)
map_mul_right_eq_self₃ : Eq (α := Measure G) (map (fun (x : G) ↦ x⁻¹ * g) μ) (map (fun (x : G) ↦ (g⁻¹ * x)⁻¹) μ)
map_mul_right_eq_self₄ : Eq (α := Measure G) (map (fun (x : G) ↦ x⁻¹ * g) μ) (map (fun (x : G) ↦ x⁻¹ * g⁻¹⁻¹) μ)
⊢ Eq (α := Measure G) (map (fun (x : G) ↦ x * g) μ.inv) (Measure.inv (map (fun (x : G) ↦ g⁻¹ * x) μ))

Tactic:
simp_rw [Measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), Function.comp_def, mul_inv_rev, inv_inv]

Premises used: MeasurableMul.measurable_const_mul, MeasurableInv.measurable_inv, Function.comp_def, Inv.inv, inv_inv, MeasurableMul.measurable_mul_const, mul_inv_rev, MeasureTheory.Measure.inv, MeasureTheory.Measure.map_map