awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
hM : Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)
A :
  ∀ (x : F × E),
    Membership.mem (α := F) s ((M : (a : F × E) → F) x : F) ↔
      Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x
⊢ MeasurableSet (α := F × E) ((⇑M : (a : F × E) → F) ⁻¹' s)

Tactic:
exact M_cont.measurable hs

Premises used: Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
h : ∀ (y : F), ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s
⊢ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
(ae_ae_add_linearMap_mem_iff L μ ν hs).1 (Filter.Eventually.of_forall h)

Premises used: MeasureTheory.ae_ae_add_linearMap_mem_iff, Filter.Eventually.of_forall, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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 : G
this_1 : MeasurableSpace A := borel A
this : BorelSpace A
⊢ (HSMul.hSMul.{u_1, u_2, u_2} (α := Gᵈᵐᵃ) (β := Measure A) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) 1 : Gᵈᵐᵃ)
          addHaar).addHaarScalarFactor
      addHaar =
    1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
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
⊢ (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

Tactic:
simp_rw [DomMulAct.mk_mul]

Premises used: DomMulAct.mk_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
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
⊢ (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:
rw [addHaarScalarFactor_eq_mul _ (DomMulAct.mk g' • addHaar (G := A))]

Premises used: MeasureTheory.Measure.addHaarScalarFactor_eq_mul, DomMulAct.mk, HSMul.hSMul, MeasureTheory.Measure.addHaar, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
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
⊢ (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:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
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
⊢ (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:
simp_rw [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
e_a 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
⊢ (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:
rw [addHaarScalarFactor_domSMul]

Premises used: MeasureTheory.Measure.addHaarScalarFactor_domSMul
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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 : G
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) (((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g : ℝ≥0)

Tactic:
pos_iff_ne_zero.mpr ((Group.isUnit g).map (distribHaarChar A)).ne_zero

Premises used: Iff.mpr, MeasureTheory.distribHaarChar, Group.isUnit, IsUnit.ne_zero, IsUnit.map, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
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
⊢ (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g

Tactic:
borelize A
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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 : G
inst_7 : BorelSpace A
μ : Measure A
inst_8 : μ.IsAddHaarMeasure
this : MeasurableSpace A := borel A
⊢ (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g

Tactic:
addHaarScalarFactor_smul_congr' ..

Premises used: MeasureTheory.Measure.addHaarScalarFactor, MeasureTheory.Measure.addHaarScalarFactor_smul_congr', ite
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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 : G
inst_7 : BorelSpace A
μ : Measure A
inst_8 : μ.IsAddHaarMeasure
this : MeasurableSpace A := borel A
⊢ (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g

Tactic:
exact addHaarScalarFactor_smul_congr' ..

Premises used: MeasureTheory.Measure.addHaarScalarFactor_smul_congr'
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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 :
  (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
⊢ μ.addHaarScalarFactor (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)]

Premises used: DomMulAct.mk, MeasureTheory.Measure.addHaarScalarFactor_domSMul, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
simp_rw :
  (HSMul.hSMul (α := Gᵈᵐᵃ) ((DomMulAct.mk : (a : G) → Gᵈᵐᵃ) g : Gᵈᵐᵃ) μ).addHaarScalarFactor μ =
    ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) 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

Tactic:
simp_rw [← mul_smul, mul_inv_cancel, one_smul]

Premises used: one_smul, mul_inv_cancel, SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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

Tactic:
addHaarScalarFactor_smul_eq_distribHaarChar ..

Premises used: MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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

Tactic:
exact addHaarScalarFactor_smul_eq_distribHaarChar ..

Premises used: MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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ᵈᵐᵃ) μ)
rw₃ 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)⁻¹

Tactic:
rw [← map_inv, ← addHaarScalarFactor_smul_inv_eq_distribHaarChar μ, DomMulAct.mk_inv, inv_inv]

Premises used: MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar, map_inv, inv_inv, DomMulAct.mk_inv
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
⊢ 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:
simp [domSMul_apply]

Premises used: MeasureTheory.Measure.domSMul_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
⊢ 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]
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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∞)
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∞)
rw₅ 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ᵈᵐᵃ) μ : (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)

Tactic:
rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]

Premises used: MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar, eq_comm, MeasureTheory.Measure.nnreal_smul_coe_apply, MeasureTheory.Measure.isAddLeftInvariant_eq_smul_of_regular, MeasureTheory.Measure.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : G
hb₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (↑(((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) (g • s) : ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← distribHaarChar_mul, ENNReal.mul_div_cancel_right]

Premises used: ENNReal.mul_div_cancel_right, MeasureTheory.distribHaarChar_mul
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : G
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : G
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar
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 : G
inst_7 : MeasurableSpace A
inst_8 : BorelSpace A
μ : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : μ.Regular
s : Set A
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0
hμgs : (μ : (a : Set A) → ℝ≥0∞) (g • s) = HMul.hMul (β := ℝ≥0∞) (↑r : ℝ≥0∞) ((μ : (a : Set A) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((distribHaarChar A : G →* ℝ≥0) : (a : G) → ℝ≥0) g = r

Tactic:
ENNReal.coe_injective ?_

Premises used: ENNReal.coe_injective