awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
conv :
  (haarScalarFactor haar μ • μ).haarScalarFactor (map (⇑φ : (a : G) → G) (haarScalarFactor haar μ • μ)) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
⊢ (haarScalarFactor haar μ • μ).haarScalarFactor (map (α := G) (⇑φ : (a : G) → G) haar) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
conv =>
    enter [1, 2, 2]
    rw [smul]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
simp_rw :
  (haarScalarFactor haar μ • μ).haarScalarFactor
      (HSMul.hSMul (β := Measure G) (haarScalarFactor haar μ) (map (⇑φ : (a : G) → G) μ)) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
⊢ (haarScalarFactor haar μ • μ).haarScalarFactor (map (⇑φ : (a : G) → G) (haarScalarFactor haar μ • μ)) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
simp_rw [MeasureTheory.Measure.map_smul]

Premises used: MeasureTheory.Measure.map_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
⊢ (haarScalarFactor haar μ • μ).haarScalarFactor
      (HSMul.hSMul (β := Measure G) (haarScalarFactor haar μ) (map (⇑φ : (a : G) → G) μ)) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
haarScalarFactor_smul_smul _ _ (haarScalarFactor_pos_of_isHaarMeasure haar μ).ne'

Premises used: MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure, LT.lt.ne', MeasureTheory.Measure.haar, MeasureTheory.Measure.haarScalarFactor_smul_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
⊢ (haarScalarFactor haar μ • μ).haarScalarFactor
      (HSMul.hSMul (β := Measure G) (haarScalarFactor haar μ) (map (⇑φ : (a : G) → G) μ)) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
exact haarScalarFactor_smul_smul _ _ (haarScalarFactor_pos_of_isHaarMeasure haar μ).ne'

Premises used: MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure, LT.lt.ne', MeasureTheory.Measure.haar, MeasureTheory.Measure.haarScalarFactor_smul_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
rw : HSMul.hSMul (β := Measure G) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) (map (⇑φ : (a : G) → G) μ) = μ
⊢ HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ) (map (⇑φ : (a : G) → G) μ) = μ

Tactic:
rw [mulEquivHaarChar_eq μ φ]

Premises used: MeasureTheory.mulEquivHaarChar_eq
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
⊢ Regular (α := G) (map (⇑φ : (a : G) → G) μ)

Tactic:
have : Regular (map φ μ) := Regular.map φ.toHomeomorph
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
this : Regular (α := G) (map (⇑φ : (a : G) → G) μ)
⊢ HSMul.hSMul (β := Measure G) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) (map (⇑φ : (a : G) → G) μ) = μ

Tactic:
(isMulLeftInvariant_eq_smul_of_regular μ (map φ μ)).symm

Premises used: MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular, MeasureTheory.Measure.map, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
this : Regular (α := G) (map (⇑φ : (a : G) → G) μ)
⊢ HSMul.hSMul (β := Measure G) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) (map (⇑φ : (a : G) → G) μ) = μ

Tactic:
exact (isMulLeftInvariant_eq_smul_of_regular μ (map φ μ)).symm

Premises used: MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular, MeasureTheory.Measure.map, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
rw : mulEquivHaarChar φ • μ = map (⇑φ.symm : (a : G) → G) μ
⊢ mulEquivHaarChar φ • μ = comap (⇑φ : (a : G) → G) μ

Tactic:
rw [show ⇑φ = ⇑e from rfl, ← e.map_symm, show ⇑e.symm = ⇑φ.symm from rfl]

Premises used: rfl, MeasurableEquiv.map_symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ Regular (α := G) (map (⇑φ.symm : (a : G) → G) μ)

Tactic:
have : (map (φ.symm) μ).Regular := Regular.map φ.symm.toHomeomorph
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : Regular (α := G) (map (⇑φ.symm : (a : G) → G) μ)
rw :
  mulEquivHaarChar φ • μ =
    HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ)
      (map (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑φ.symm : (a : G) → G)) μ)
hg : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
hf : Measurable (α := G) (β := G) (⇑φ.symm : (a : G) → G)
⊢ mulEquivHaarChar φ • μ = map (⇑φ.symm : (a : G) → G) μ

Tactic:
rw [← mulEquivHaarChar_smul_map (map φ.symm μ) φ, map_map]

Premises used: MeasureTheory.mulEquivHaarChar_smul_map, MeasureTheory.Measure.map, ContinuousMulEquiv.symm, MeasureTheory.Measure.map_map, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : Regular (α := G) (map (⇑φ.symm : (a : G) → G) μ)
⊢ mulEquivHaarChar φ • μ =
    HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ)
      (map (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑φ.symm : (a : G) → G)) μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : Regular (α := G) (map (⇑φ.symm : (a : G) → G) μ)
funProp : inst_2 ≤ inst_2
funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (φ : (a : G) → G) a
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : Regular (α := G) (map (⇑φ.symm : (a : G) → G) μ)
funProp : inst_2 ≤ inst_2
funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (φ.symm : (a : G) → G) a
⊢ Measurable (α := G) (β := G) (⇑φ.symm : (a : G) → G)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
nth_rw :
  HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (@integral _ _ _ _ inst_2 (map (⇑φ : (a : G) → G) μ) fun (a : G) ↦ f a) =
    ∫ (a : G), f a ∂HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ) (map (⇑φ : (a : G) → G) μ)
⊢ HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (@integral _ _ _ _ inst_2 (map (⇑φ : (a : G) → G) μ) fun (a : G) ↦ f a) =
    ∫ (a : G), f a ∂μ

Tactic:
nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]

Premises used: MeasureTheory.mulEquivHaarChar_smul_map
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
⊢ HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (@integral _ _ _ _ inst_2 (map (⇑φ : (a : G) → G) μ) fun (a : G) ↦ f a) =
    ∫ (a : G), f a ∂HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ) (map (⇑φ : (a : G) → G) μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
change :
  (@integral _ _ _ _ inst_2 (comap (⇑e : (a : G) → G) μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
⊢ (@integral _ _ _ _ inst_2 (comap (⇑φ : (a : G) → G) μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)

Tactic:
change ∫ a, f a ∂(comap e μ) = mulEquivHaarChar φ • ∫ a, f a ∂μ

Premises used: MeasureTheory.Measure.comap, DFunLike.coe, MeasureTheory.mulEquivHaarChar
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)

Tactic:
have : (map (e.symm) μ).IsHaarMeasure := φ.symm.isHaarMeasure_map μ
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
⊢ Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)

Tactic:
have : (map (e.symm) μ).Regular := Regular.map φ.symm.toHomeomorph
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this_1 : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
this : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)

Tactic:
φ.toHomeomorph.toMeasurableEquiv.measurable

Premises used: Homeomorph.toMeasurableEquiv, ContinuousMulEquiv.toHomeomorph, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this_1 : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
this : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)

Tactic:
exact φ.toHomeomorph.toMeasurableEquiv.measurable

Premises used: Homeomorph.toMeasurableEquiv, ContinuousMulEquiv.toHomeomorph, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this_1 : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
this : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
rw :
  HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ)
      (@integral _ _ _ _ inst_2 (map (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G)) μ)
        fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
⊢ (@integral _ _ _ _ inst_2 (comap (⇑e : (a : G) → G) μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)

Tactic:
rw [← e.map_symm, ← mulEquivHaarChar_smul_integral_map (map e.symm μ) φ,
    map_map (by exact φ.toHomeomorph.toMeasurableEquiv.measurable) e.symm.measurable]

Premises used: MeasureTheory.mulEquivHaarChar_smul_integral_map, MeasurableEquiv.symm, MeasureTheory.Measure.map, MeasurableEquiv.measurable, MeasureTheory.Measure.map_map, DFunLike.coe, MeasurableEquiv.map_symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this_1 : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
this : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
h : ∀ (x : G), Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G) x = id x
⊢ Eq (α := G → G) (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G)) id

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this_1 : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
this : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
x : G
⊢ Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G) x = id x

Tactic:
simp [e]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this_1 : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
this : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
rw :
  HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (@integral _ _ _ _ inst_2 (map id μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
⊢ HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ)
      (@integral _ _ _ _ inst_2 (map (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G)) μ)
        fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)

Tactic:
rw [show ⇑φ ∘ ⇑e.symm = id by ext; simp [e]]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this_1 : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
this : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
⊢ HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (@integral _ _ _ _ inst_2 (map id μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
X : Set G
φ : G ≃ₜ* G
nth_rw :
  HSMul.hSMul (β := ℝ≥0∞) (mulEquivHaarChar φ) ((μ : (a : Set G) → ℝ≥0∞) ((⇑φ : (a : G) → G) ⁻¹' X) : ℝ≥0∞) =
    (HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ) (map (⇑φ : (a : G) → G) μ) : (a : Set G) → ℝ≥0∞) X
⊢ HSMul.hSMul (β := ℝ≥0∞) (mulEquivHaarChar φ) ((μ : (a : Set G) → ℝ≥0∞) ((⇑φ : (a : G) → G) ⁻¹' X) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) X

Tactic:
nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]

Premises used: MeasureTheory.mulEquivHaarChar_smul_map
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
X : Set G
φ : G ≃ₜ* G
⊢ HMul.hMul (β := ℝ≥0∞) (↑(mulEquivHaarChar φ) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑φ : (a : G) → G) ⁻¹' X) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(mulEquivHaarChar φ) : ℝ≥0∞)
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) X : ℝ≥0∞)

Tactic:
congr_arg _ <| (MeasurableEquiv.map_apply φ.toMeasurableEquiv X).symm

Premises used: MeasurableEquiv.map_apply, Homeomorph.toMeasurableEquiv, congr_arg, ContinuousMulEquiv.toHomeomorph, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
X : Set G
φ : G ≃ₜ* G
⊢ HMul.hMul (β := ℝ≥0∞) (↑(mulEquivHaarChar φ) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑φ : (a : G) → G) ⁻¹' X) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑(mulEquivHaarChar φ) : ℝ≥0∞)
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) X : ℝ≥0∞)

Tactic:
exact congr_arg _ <| (MeasurableEquiv.map_apply φ.toMeasurableEquiv X).symm

Premises used: MeasurableEquiv.map_apply, Homeomorph.toMeasurableEquiv, congr_arg, ContinuousMulEquiv.toHomeomorph, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
⊢ mulEquivHaarChar (ContinuousMulEquiv.refl G) = 1

Tactic:
simp [mulEquivHaarChar, Function.id_def]

Premises used: Function.id_def, MeasureTheory.mulEquivHaarChar
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
funProp : inst_2 ≤ inst_2
funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (φ : (a : G) → G) a
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)

Tactic:
have hφ : Measurable φ := by fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
hφ : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
funProp : inst_2 ≤ inst_2
funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (ψ : (a : G) → G) a
⊢ Measurable (α := G) (β := G) (⇑ψ : (a : G) → G)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
hφ : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
⊢ Measurable (α := G) (β := G) (⇑ψ : (a : G) → G)

Tactic:
have hψ : Measurable ψ := by fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
hφ : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
hψ : Measurable (α := G) (β := G) (⇑ψ : (a : G) → G)
simp_rw :
  haarScalarFactor (G := G) haar (map (α := G) (⇑φ : (a : G) → G) (map (α := G) (⇑ψ : (a : G) → G) haar)) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
⊢ haarScalarFactor (G := G) haar (map (α := G) (⇑(ψ.trans φ) : (a : G) → G) haar) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ

Tactic:
simp_rw [ContinuousMulEquiv.coe_trans, ← map_map hφ hψ]

Premises used: ContinuousMulEquiv.coe_trans, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
hφ : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
hψ : Measurable (α := G) (β := G) (⇑ψ : (a : G) → G)
⊢ Regular (α := G) (map (α := G) (⇑ψ : (a : G) → G) haar)

Tactic:
have h_reg : (haar.map ψ).Regular := Regular.map ψ.toHomeomorph