awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
α : Type u_3
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
inst_7 : Group α
inst_8 : MulAction α G
inst_9 : SMulCommClass α G G
inst_10 : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := Homeomorph.toMeasurableEquiv (Homeomorph.smul a)
change : LT.lt (α := ℝ≥0∞) (((map (⇑F : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((map (fun (x : G) ↦ a • x) μ : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
change map F μ K < ∞

Premises used: MeasureTheory.Measure.map, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
α : Type u_3
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
inst_7 : Group α
inst_8 : MulAction α G
inst_9 : SMulCommClass α G G
inst_10 : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := Homeomorph.toMeasurableEquiv (Homeomorph.smul a)
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑F : (a : G) → G) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((map (⇑F : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [F.map_apply K]

Premises used: MeasurableEquiv.map_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
α : Type u_3
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
inst_7 : Group α
inst_8 : MulAction α G
inst_9 : SMulCommClass α G G
inst_10 : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := Homeomorph.toMeasurableEquiv (Homeomorph.smul a)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑F : (a : G) → G) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
IsCompact.measure_lt_top <| (Homeomorph.isCompact_preimage (Homeomorph.smul a)).2 hK

Premises used: Iff.mpr, Homeomorph.isCompact_preimage, Homeomorph.smul, IsCompact.measure_lt_top
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
α : Type u_3
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
inst_7 : Group α
inst_8 : MulAction α G
inst_9 : SMulCommClass α G G
inst_10 : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := Homeomorph.toMeasurableEquiv (Homeomorph.smul a)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) ((⇑F : (a : G) → G) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact IsCompact.measure_lt_top <| (Homeomorph.isCompact_preimage (Homeomorph.smul a)).2 hK

Premises used: Iff.mpr, Homeomorph.isCompact_preimage, Homeomorph.smul, IsCompact.measure_lt_top
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
g : G
⊢ IsHaarMeasure (G := G) (map (fun (x : G) ↦ x * g) μ)

Tactic:
isHaarMeasure_map_smul μ (MulOpposite.op g)

Premises used: MeasureTheory.Measure.isHaarMeasure_map_smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
μ : Measure G
inst_3 : μ.IsHaarMeasure
inst_4 : BorelSpace G
inst_5 : ContinuousMul G
H : Type u_3
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : MeasurableSpace H
inst_9 : BorelSpace H
inst_10 : IsTopologicalGroup H
e : G ≃* H
he : Continuous[inst_2, inst_7] (⇑e : (a : G) → H)
hesymm : Continuous[inst_7, inst_2] (⇑e.symm : (a : H) → G)
⊢ IsHaarMeasure.{u_3} (G := H) (map (⇑e : (a : G) → H) μ)

Tactic:
let f : G ≃ₜ H := .mk e he hesymm
  -- We need to write `e.toMonoidHom` instead of just `e`, to avoid unification issues.
  isHaarMeasure_map μ e.toMonoidHom he e.surjective f.isClosedEmbedding.tendsto_cocompact

Premises used: Homeomorph.mk, MulEquiv.surjective, Topology.IsClosedEmbedding.tendsto_cocompact, MulEquiv.toMonoidHom, MeasureTheory.Measure.isHaarMeasure_map, Homeomorph.isClosedEmbedding, EquivLike.toEquiv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H_1 : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H_1
inst_2 : Group G
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
inst_5 : BorelSpace G
inst_6 : IsTopologicalGroup G
H : Type u_3
inst_7 : Group H
inst_8 : TopologicalSpace H
inst_9 : MeasurableSpace H
inst_10 : BorelSpace H
inst_11 : IsTopologicalGroup H
e : G ≃ₜ* H
⊢ IsHaarMeasure.{u_3} (G := H) (map (⇑e : (a : G) → H) μ)

Tactic:
e.toMulEquiv.isHaarMeasure_map μ e.continuous e.symm.continuous

Premises used: Homeomorph.continuous, MulEquiv.isHaarMeasure_map, ContinuousMulEquiv.symm, ContinuousMulEquiv.toHomeomorph, ContinuousMulEquiv.toMulEquiv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
E : Type u_3
F : Type u_4
R : Type u_5
S : Type u_6
inst_5 : Semiring R
inst_6 : Semiring S
inst_7 : AddCommGroup E
inst_8 : Module R E
inst_9 : AddCommGroup F
inst_10 : Module S F
inst_11 : TopologicalSpace E
inst_12 : IsTopologicalAddGroup E
inst_13 : TopologicalSpace F
inst_14 : IsTopologicalAddGroup F
σ : R →+* S
σ' : S →+* R
inst_15 : RingHomInvPair σ σ'
inst_16 : RingHomInvPair σ' σ
inst_17 : MeasurableSpace E
inst_18 : BorelSpace E
inst_19 : MeasurableSpace F
inst_20 : BorelSpace F
L : E ≃SL[σ] F
μ : Measure E
inst_21 : μ.IsAddHaarMeasure
⊢ IsAddHaarMeasure.{u_4} (G := F) (map (⇑L : (a : E) → F) μ)

Tactic:
AddEquiv.isAddHaarMeasure_map _ (L : E ≃+ F) L.continuous L.symm.continuous

Premises used: ContinuousLinearEquiv.symm, AddEquiv.isAddHaarMeasure_map, AddEquivClass.toAddEquiv, ContinuousLinearEquiv.continuous
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ : Measure G
inst_4 : μ.IsHaarMeasure
inst_5 : SigmaCompactSpace G
⊢ SigmaFinite μ

Tactic:
⟨⟨{   set := compactCovering G
        set_mem := fun _ => mem_univ _
        finite := fun n => IsCompact.measure_lt_top <| isCompact_compactCovering G n
        spanning := iUnion_compactCovering G }⟩⟩

Premises used: compactCovering, iUnion_compactCovering, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, isCompact_compactCovering, Nonempty.intro, IsCompact.measure_lt_top, Set.mem_univ, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
inl : ∀ (x : G), Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NoAtoms μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (x : G), Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (K : Set G), IsCompact K ∧ Membership.mem (γ := Filter G) (𝓝 1) K

Tactic:
exists_compact_mem_nhds 1

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
inr : ∀ (K : Set G) (K_compact : IsCompact K) (K_nhds : Membership.mem (γ := Filter G) (𝓝 1) K), NoAtoms μ
⊢ NoAtoms μ

Tactic:
obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds, OfNat.ofNat, Set
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
K : Set G
K_compact : IsCompact K
K_nhds : Membership.mem (γ := Filter G) (𝓝 1) K
⊢ K.Infinite

Tactic:
have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
K : Set G
K_compact : IsCompact K
K_nhds : Membership.mem (γ := Filter G) (𝓝 1) K
K_inf : K.Infinite
⊢ NoAtoms μ

Tactic:
absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩)
      K_compact.measure_lt_top.ne

Premises used: MeasureTheory.Measure.haar_singleton, Eq.ge, Set.Infinite.meas_eq_top, absurd, IsCompact.measure_lt_top, And.intro, Exists.intro, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
h : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)
K : Set G
K_compact : IsCompact K
K_nhds : Membership.mem (γ := Filter G) (𝓝 1) K
K_inf : K.Infinite
⊢ NoAtoms μ

Tactic:
exact absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩)
      K_compact.measure_lt_top.ne

Premises used: MeasureTheory.Measure.haar_singleton, Eq.ge, Set.Infinite.meas_eq_top, absurd, IsCompact.measure_lt_top, And.intro, Exists.intro, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
inst_3 : TopologicalSpace G
μ_1 : Measure G
inst_4 : μ_1.IsHaarMeasure
inst_5 : IsTopologicalGroup G
inst_6 : BorelSpace G
inst_7 : T1Space G
inst_8 : WeaklyLocallyCompactSpace G
inst_9 : NeBot (α := G) (𝓝[≠] 1)
μ : Measure G
inst_10 : μ.IsHaarMeasure
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) 1 : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
cases eq_or_ne (μ 1) 0 with
  | inl h => constructor; simpa
  | inr h =>
    obtain ⟨K, K_compact, K_nhds⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ 𝓝 1 := exists_compact_mem_nhds 1
    have K_inf : Set.Infinite K := infinite_of_mem_nhds (1 : G) K_nhds
    exact absurd (K_inf.meas_eq_top ⟨_, h, fun x _ ↦ (haar_singleton _ _).ge⟩)
      K_compact.measure_lt_top.ne

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, nhds, eq_or_ne, OfNat.ofNat, DFunLike.coe, Set
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G_1 : Type u_1
H : Type u_2
inst : MeasurableSpace G_1
inst_1 : MeasurableSpace H
inst_2 : Group G_1
inst_3 : TopologicalSpace G_1
μ_1 : Measure G_1
inst_4 : μ_1.IsHaarMeasure
G : Type u_3
A : Type u_4
inst_5 : Group G
inst_6 : AddCommGroup A
inst_7 : DistribMulAction G A
inst_8 : MeasurableSpace A
inst_9 : TopologicalSpace A
inst_10 : BorelSpace A
inst_11 : IsTopologicalAddGroup A
inst_12 : ContinuousConstSMul G A
μ : Measure A
inst_13 : μ.IsAddHaarMeasure
g : Gᵈᵐᵃ
⊢ (g • μ).IsAddHaarMeasure

Tactic:
(DistribMulAction.toAddEquiv _ (DomMulAct.mk.symm g⁻¹)).isAddHaarMeasure_map _
    (continuous_const_smul _) (continuous_const_smul _)

Premises used: DistribMulAction.toAddEquiv, ContinuousConstSMul.continuous_const_smul, AddEquiv.isAddHaarMeasure_map, DomMulAct.mk, Inv.inv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.InnerRegular
g : G
rw : map (fun (x : G) ↦ x * g) μ = haarScalarFactor (map (fun (x : G) ↦ x * g) μ) μ • μ
⊢ map (fun (x : G) ↦ x * g) μ = modularCharacterFun g • μ

Tactic:
rw [modularCharacterFun_eq_haarScalarFactor μ _]

Premises used: MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.InnerRegular
g : G
⊢ map (fun (x : G) ↦ x * g) μ = haarScalarFactor (map (fun (x : G) ↦ x * g) μ) μ • μ

Tactic:
isMulLeftInvariant_eq_smul_of_innerRegular _ μ

Premises used: MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.InnerRegular
g : G
⊢ map (fun (x : G) ↦ x * g) μ = haarScalarFactor (map (fun (x : G) ↦ x * g) μ) μ • μ

Tactic:
exact isMulLeftInvariant_eq_smul_of_innerRegular _ μ

Premises used: MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_innerRegular
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g : G
⊢ let this := borel G;
  BorelSpace G

Tactic:
borelize G
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
rw : 0 < haarScalarFactor.{u_1} (G := G) (map (fun (x : G) ↦ x * g) haar) haar
⊢ 0 < modularCharacterFun g

Tactic:
rw [modularCharacterFun_eq_haarScalarFactor MeasureTheory.Measure.haar g]

Premises used: MeasureTheory.Measure.haar, MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ 0 < haarScalarFactor.{u_1} (G := G) (map (fun (x : G) ↦ x * g) haar) haar

Tactic:
haarScalarFactor_pos_of_isHaarMeasure _ _

Premises used: MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ 0 < haarScalarFactor.{u_1} (G := G) (map (fun (x : G) ↦ x * g) haar) haar

Tactic:
exact haarScalarFactor_pos_of_isHaarMeasure _ _

Premises used: MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
⊢ modularCharacterFun.{u_1} (G := G) 1 = 1

Tactic:
simp [modularCharacterFun, haarScalarFactor_self]

Premises used: MeasureTheory.Measure.modularCharacterFun, MeasureTheory.Measure.haarScalarFactor_self
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
⊢ let this := borel G;
  BorelSpace G

Tactic:
borelize G
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ Measurable (β := G) fun (x : G) ↦ x * g

Tactic:
have mul_g_meas : Measurable (· * g) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) g
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
⊢ Measurable (β := G) fun (x : G) ↦ x * h

Tactic:
have mul_h_meas : Measurable (· * h) := Measurable.mul_const (fun ⦃_⦄ a ↦ a) h
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
symm : modularCharacterFun g * modularCharacterFun h = modularCharacterFun (g * h)
⊢ modularCharacterFun (g * h) = modularCharacterFun g * modularCharacterFun h

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
⊢ modularCharacterFun g * modularCharacterFun h = modularCharacterFun h * modularCharacterFun g

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
rw rw₁ :
  haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      modularCharacterFun g =
    haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      modularCharacterFun g
⊢ modularCharacterFun h * modularCharacterFun g =
    haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      modularCharacterFun g

Tactic:
rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]

Premises used: HMul.hMul, MeasureTheory.Measure.map, MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactor
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
⊢ haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      modularCharacterFun g =
    haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      haarScalarFactor (map (fun (x : G) ↦ x * g) ν) ν

Tactic:
rfl

Premises used: MeasureTheory.Measure.modularCharacterFun, rfl
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
⊢ haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      haarScalarFactor (map (fun (x : G) ↦ x * g) ν) ν =
    haarScalarFactor (map (fun (x : G) ↦ x * (g * h)) ν) ν

Tactic:
simp only [map_map mul_h_meas mul_g_meas,
      comp_mul_right, ← haarScalarFactor_eq_mul]

Premises used: comp_mul_right, MeasureTheory.Measure.haarScalarFactor_eq_mul, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.ModularCharacter
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
g h : G
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
mul_g_meas : Measurable (β := G) fun (x : G) ↦ x * g
mul_h_meas : Measurable (β := G) fun (x : G) ↦ x * h
ν : Measure G := haar
modularCharacterFun :
  Measure.modularCharacterFun h * Measure.modularCharacterFun g =
    haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      Measure.modularCharacterFun g
modularCharacterFun₁ :
  haarScalarFactor (G := G) (map (fun (x : G) ↦ x * h) (map (fun (x : G) ↦ x * g) ν)) (map (fun (x : G) ↦ x * g) ν) *
      haarScalarFactor (map (fun (x : G) ↦ x * g) ν) ν =
    haarScalarFactor (map (fun (x : G) ↦ x * (g * h)) ν) ν
⊢ Measure.modularCharacterFun g * Measure.modularCharacterFun h = Measure.modularCharacterFun (g * h)

Tactic:
calc
    modularCharacterFun g * modularCharacterFun h =
      modularCharacterFun h * modularCharacterFun g := mul_comm _ _
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      modularCharacterFun g := by
      rw [modularCharacterFun_eq_haarScalarFactor (map (· * g) ν) _]
    _ = haarScalarFactor (map (· * h) (map (· * g) ν)) (map (· * g) ν) *
      haarScalarFactor (map (· * g) ν) ν := rfl
    _ = haarScalarFactor (map (· * (g * h)) ν) ν := by simp only [map_map mul_h_meas mul_g_meas,
      comp_mul_right, ← haarScalarFactor_eq_mul]

Premises used: MeasureTheory.Measure.modularCharacterFun, HMul.hMul, MeasureTheory.Measure.map, mul_comm, MeasureTheory.Measure.haarScalarFactor, rfl
-- Module: Mathlib.MeasureTheory.Group.Pointwise
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : MeasurableConstSMul G α
s : Set α
hs : MeasurableSet s
a : G
rw : MeasurableSet (α := α) ((fun (x : α) ↦ a⁻¹ • x) ⁻¹' s)
⊢ MeasurableSet (a • s)

Tactic:
rw [← preimage_smul_inv]

Premises used: Set.preimage_smul_inv