awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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)) μ)
⊢ mulEquivHaarChar φ • μ = map (⇑φ.symm : (a : G) → G) μ
have hg : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
Tactic: rw [← mulEquivHaarChar_smul_map (map φ.symm μ) φ, map_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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)
⊢ mulEquivHaarChar φ • μ = map (⇑φ.symm : (a : G) → G) μ
have hf : Measurable (α := G) (β := G) (⇑φ.symm : (a : G) → G)
Tactic: rw [← mulEquivHaarChar_smul_map (map φ.symm μ) φ, map_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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) μ)
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
have funProp : inst_2 ≤ inst_2
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
have funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (φ : (a : G) → G) a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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) μ)
⊢ Measurable (α := G) (β := G) (⇑φ.symm : (a : G) → G)
have funProp : inst_2 ≤ inst_2
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ Measurable (α := G) (β := G) (⇑φ.symm : (a : G) → G)
have funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (φ.symm : (a : G) → G) a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 ∂μ
have 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) μ)
Tactic: nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ (@integral _ _ _ _ inst_2 (comap (⇑φ : (a : G) → G) μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
have change : (@integral _ _ _ _ inst_2 (comap (⇑e : (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 ∂μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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
⊢ (@integral _ _ _ _ inst_2 (comap (⇑e : (a : G) → G) μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
have this : IsHaarMeasure (G := G) (map (⇑e.symm : (a : G) → G) μ)
Tactic: have : (map (e.symm) μ).IsHaarMeasure := φ.symm.isHaarMeasure_map μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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) μ)
⊢ (@integral _ _ _ _ inst_2 (comap (⇑e : (a : G) → G) μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
have this₁ : Regular (α := G) (map (⇑e.symm : (a : G) → G) μ)
Tactic: have : (map (e.symm) μ).Regular := Regular.map φ.symm.toHomeomorph
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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) μ)
⊢ (@integral _ _ _ _ inst_2 (comap (⇑e : (a : G) → G) μ) fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
have 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 ∂μ)
Tactic: rw [← e.map_symm, ← mulEquivHaarChar_smul_integral_map (map e.symm μ) φ,
    map_map (by exact φ.toHomeomorph.toMeasurableEquiv.measurable) e.symm.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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) μ)
⊢ Eq (α := G → G) (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G)) id
have h : ∀ (x : G), Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G) x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑e.symm : (a : G) → G)) μ)
        fun (a : G) ↦ f a) =
    HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
have rw : HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (@integral _ _ _ _ inst_2 (map id μ) fun (a : G) ↦ f a) =
  HSMul.hSMul (β := ℝ) (mulEquivHaarChar φ) (∫ (a : G), f a ∂μ)
Tactic: rw [show ⇑φ ∘ ⇑e.symm = id by ext; simp [e]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ HSMul.hSMul (β := ℝ≥0∞) (mulEquivHaarChar φ) ((μ : (a : Set G) → ℝ≥0∞) ((⇑φ : (a : G) → G) ⁻¹' X) : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) X
have 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
Tactic: nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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)
have funProp : inst_2 ≤ inst_2
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
have funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (φ : (a : G) → G) a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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
⊢ haarScalarFactor (G := G) haar (map (α := G) (⇑(ψ.trans φ) : (a : G) → G) haar) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
have hφ : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
Tactic: have hφ : Measurable φ := by fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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)
have funProp : inst_2 ≤ inst_2
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ Measurable (α := G) (β := G) (⇑ψ : (a : G) → G)
have funProp₁ : MeasurableEmbedding (β := G) fun (a : G) ↦ (ψ : (a : G) → G) a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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)
⊢ haarScalarFactor (G := G) haar (map (α := G) (⇑(ψ.trans φ) : (a : G) → G) haar) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
have hψ : Measurable (α := G) (β := G) (⇑ψ : (a : G) → G)
Tactic: have hψ : Measurable ψ := by fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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)
⊢ haarScalarFactor (G := G) haar (map (α := G) (⇑(ψ.trans φ) : (a : G) → G) haar) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
have 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 φ
Tactic: simp_rw [ContinuousMulEquiv.coe_trans, ← map_map hφ hψ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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)
⊢ 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 φ
have h_reg : Regular (α := G) (map (α := G) (⇑ψ : (a : G) → G) haar)
Tactic: have h_reg : (haar.map ψ).Regular := Regular.map ψ.toHomeomorph
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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)
h_reg : Regular (α := G) (map (α := G) (⇑ψ : (a : G) → G) haar)
⊢ 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 φ
have rw : haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) *
    haarScalarFactor (G := G) (map (α := G) (⇑ψ : (a : 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 φ
Tactic: rw [MeasureTheory.Measure.haarScalarFactor_eq_mul haar (haar.map ψ),
    ← mulEquivHaarChar_eq (haar.map ψ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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)
h_reg : Regular (α := G) (map (α := G) (⇑ψ : (a : G) → G) haar)
rw :
  haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) *
      haarScalarFactor (G := G) (map (α := G) (⇑ψ : (a : 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) (⇑φ : (a : G) → G) (map (α := G) (⇑ψ : (a : G) → G) haar)) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
have rw₁ : haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ =
  haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
Tactic: rw [MeasureTheory.Measure.haarScalarFactor_eq_mul haar (haar.map ψ),
    ← mulEquivHaarChar_eq (haar.map ψ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ mulEquivHaarChar φ.symm = (mulEquivHaarChar φ)⁻¹
have symm : (mulEquivHaarChar φ)⁻¹ = mulEquivHaarChar φ.symm
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ (mulEquivHaarChar φ)⁻¹ = mulEquivHaarChar φ.symm
have a : mulEquivHaarChar φ * mulEquivHaarChar φ.symm = 1
Tactic: apply inv_eq_of_mul_eq_one_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
⊢ mulEquivHaarChar φ = 1
have hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: have hμ : μ univ = 1 := haarMeasure_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ mulEquivHaarChar φ = 1
have rw : μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ) = 1
Tactic: rw [mulEquivHaarChar_eq μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ) = 1
have suffices : (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = 1
Tactic: suffices (μ.haarScalarFactor (map φ μ) : ℝ≥0∞) = 1 by exact_mod_cast this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1
have rw : (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) 1
Tactic: rw [ENNReal.smul_def, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) 1
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1
have rw₁ : (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) * 1
Tactic: rw [ENNReal.smul_def, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) 1
rw₁ :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) * 1
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1
have rw₂ : (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞)
Tactic: rw [ENNReal.smul_def, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
    ((μ : (a : Set G) → ℝ≥0∞) (preimage (β := G) (⇑φ : (a : G) → G) univ) : ℝ≥0∞)
Tactic: rw [map_apply (map_continuous φ).measurable .univ, Set.preimage_univ, hμ]