awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g_1 : G
this_1 : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) (g * g') : Gᵈᵐᵃ)
          addHaar).addHaarScalarFactor
      addHaar =
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
        addHaar *
      (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
        addHaar
have simp_rw : (HSMul.hSMul (β := Measure A)
        (HMul.hMul (α := Gᵈᵐᵃ) (β := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
          ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ))
        addHaar).addHaarScalarFactor
    addHaar =
  (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
      addHaar *
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
      addHaar
Tactic: simp_rw [DomMulAct.mk_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g_1 : G
this_1 : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (HSMul.hSMul (β := Measure A)
          (HMul.hMul (α := Gᵈᵐᵃ) (β := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
            ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ))
          addHaar).addHaarScalarFactor
      addHaar =
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
        addHaar *
      (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
        addHaar
have rw : (HSMul.hSMul (β := Measure A)
          (HMul.hMul (α := Gᵈᵐᵃ) (β := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
            ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ))
          addHaar).addHaarScalarFactor
      (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar) *
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
      addHaar =
  (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
      addHaar *
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
      addHaar
Tactic: rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g' • addHaar (G := A))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g_1 : G
this_1 : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (HSMul.hSMul (β := Measure A)
            (HMul.hMul (α := Gᵈᵐᵃ) (β := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
              ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ))
            addHaar).addHaarScalarFactor
        (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar) *
      (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
        addHaar =
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
        addHaar *
      (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
        addHaar
have e_a : (HSMul.hSMul (β := Measure A)
        (HMul.hMul (α := Gᵈᵐᵃ) (β := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
          ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ))
        addHaar).addHaarScalarFactor
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar) =
  (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
    addHaar
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g_1 : G
this_1 : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (HSMul.hSMul (β := Measure A)
          (HMul.hMul (α := Gᵈᵐᵃ) (β := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
            ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ))
          addHaar).addHaarScalarFactor
      (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar) =
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
      addHaar
have e_a : (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
        (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ)
          addHaar)).addHaarScalarFactor
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar) =
  (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
    addHaar
Tactic: simp_rw [mul_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
g_1 : G
this_1 : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ)
          (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ)
            addHaar)).addHaarScalarFactor
      (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g' : Gᵈᵐᵃ) addHaar) =
    (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
      addHaar
have e_a : (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
    addHaar =
  (HSMul.hSMul (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) addHaar).addHaarScalarFactor
    addHaar
Tactic: rw [addHaarScalarFactor_domSMul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
g : G
⊢ (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g
have borelize : ∀ [inst_10 : BorelSpace A] (μ : Measure A) [inst_11 : μ.IsAddHaarMeasure],
  (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g
Tactic: borelize A
Cleared hypotheses: inst_7, inst_8, μ, inst_9
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
g : G
⊢ μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g)⁻¹ : Gᵈᵐᵃ) μ) =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g
have rw : (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor
    (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ)
      (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g)⁻¹ : Gᵈᵐᵃ) μ)) =
  ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g
Tactic: rw [← addHaarScalarFactor_domSMul _ _ (DomMulAct.mk g)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
g : G
⊢ (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor
      (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ)
        (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g)⁻¹ : Gᵈᵐᵃ) μ)) =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g
have simp_rw : (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ =
  ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g
Tactic: simp_rw [← mul_smul, mul_inv_cancel, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
g : G
⊢ μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g)⁻¹
have rw : μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
  ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g⁻¹
Tactic: rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_distribHaarChar μ, DomMulAct.mk_inv, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
g : G
rw :
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g⁻¹
⊢ μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g)⁻¹
have rw₁ : μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g⁻¹)⁻¹ : Gᵈᵐᵃ) μ)
Tactic: rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_distribHaarChar μ, DomMulAct.mk_inv, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
g : G
rw :
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g⁻¹
rw₁ :
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g⁻¹)⁻¹ : Gᵈᵐᵃ) μ)
⊢ μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g)⁻¹
have rw₂ : μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g)⁻¹⁻¹ : Gᵈᵐᵃ) μ)
Tactic: rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_distribHaarChar μ, DomMulAct.mk_inv, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
g : G
rw :
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g⁻¹
rw₁ :
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g⁻¹)⁻¹ : Gᵈᵐᵃ) μ)
rw₂ :
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) (((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g)⁻¹⁻¹ : Gᵈᵐᵃ) μ)
⊢ μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
    (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g)⁻¹
have rw₃ : μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ) =
  μ.addHaarScalarFactor (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ)
Tactic: rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_distribHaarChar μ, DomMulAct.mk_inv, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (hypothesis)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
g : G
s : Set A
⊢ HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set A) → ℝ≥0∞) (g • s)
have this : Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
  ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞)
Tactic: have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [domSMul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
g : G
s : Set A
this :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set A) → ℝ≥0∞) (g • s)
have rw : (μ : (a : Set A) → ℝ≥0∞) (g • s) =
  HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
    ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
g : G
s : Set A
this :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞)
rw :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set A) → ℝ≥0∞) (g • s)
have rw₁ : (μ : (a : Set A) → ℝ≥0∞) (g • s) =
  HSMul.hSMul (α := ℝ≥0) (β := ℝ≥0∞) (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g : ℝ≥0)
    ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
g : G
s : Set A
this :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞)
rw :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HSMul.hSMul (α := ℝ≥0) (β := ℝ≥0∞) (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g : ℝ≥0)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set A) → ℝ≥0∞) (g • s)
have rw₂ : (μ : (a : Set A) → ℝ≥0∞) (g • s) =
  HSMul.hSMul (β := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ)
    ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
g : G
s : Set A
this :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞)
rw :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HSMul.hSMul (α := ℝ≥0) (β := ℝ≥0∞) (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g : ℝ≥0)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HSMul.hSMul (β := ℝ≥0∞)
      ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set A) → ℝ≥0∞) (g • s)
have rw₃ : (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s =
  HSMul.hSMul (β := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ)
    ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.DistribChar (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : TopologicalSpace A
inst_4 : IsTopologicalAddGroup A
inst_5 : LocallyCompactSpace A
inst_6 : ContinuousConstSMul G A
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
g : G
s : Set A
this :
  Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞)
rw :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HSMul.hSMul (α := ℝ≥0) (β := ℝ≥0∞) (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g : ℝ≥0)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  (μ : (a : Set A) → ℝ≥0∞) (g • s) =
    HSMul.hSMul (β := ℝ≥0∞)
      ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
rw₃ :
  (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞)
      ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞)
      ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) =
    (μ : (a : Set A) → ℝ≥0∞) (g • s)
have rw₄ : Eq (α := ℝ≥0∞) ((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
  (((HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ • μ :
        (a : Set A) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]