theorem MeasureTheory.addEquivAddHaarChar_eq.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1]
  (μMeasureTheory.Measure G : MeasureTheory.MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 GType u_1)
  [μMeasureTheory.Measure G.IsAddHaarMeasureMeasureTheory.Measure.IsAddHaarMeasure.{u_3} {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  (μ : MeasureTheory.Measure G) : PropA measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition. ] [μMeasureTheory.Measure G.RegularMeasureTheory.Measure.Regular.{u_1} {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α]
  (μ : MeasureTheory.Measure α) : PropA measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. ]
  (φG ≃ₜ+ G : GType u_1 ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  GType u_1) :
  MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φG ≃ₜ+ G =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    μMeasureTheory.Measure G.addHaarScalarFactorMeasureTheory.Measure.addHaarScalarFactor.{u_1} {G : Type u_1} [TopologicalSpace G] [AddGroup G]
  [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure]
  [MeasureTheory.IsFiniteMeasureOnCompacts μ'] [μ'.IsAddLeftInvariant] : NNRealGiven two left-invariant measures which are finite on compacts,
`addHaarScalarFactor μ' μ` is a scalar such that `∫ f dμ' = (addHaarScalarFactor μ' μ) ∫ f dμ` for
any compactly supported continuous function `f`.

Note that there is a dissymmetry in the assumptions between `μ'` and `μ`: the measure `μ'` needs
only be finite on compact sets, while `μ` has to be finite on compact sets and positive on open
sets, i.e., an additive Haar measure, to exclude for instance the case where `μ = 0`, where the
definition doesn't make sense. 
      (MeasureTheory.Measure.mapMeasureTheory.Measure.map.{u_4, u_5} {α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] (f : α → β)
  (μ : MeasureTheory.Measure α) : MeasureTheory.Measure βThe pushforward of a measure. It is defined to be `0` if `f` is not an almost everywhere
measurable function.  (⇑φG ≃ₜ+ G) μMeasureTheory.Measure G)

theorem MeasureTheory.addEquivAddHaarChar_smul_map.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1]
  (μMeasureTheory.Measure G : MeasureTheory.MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 GType u_1)
  [μMeasureTheory.Measure G.IsAddHaarMeasureMeasureTheory.Measure.IsAddHaarMeasure.{u_3} {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  (μ : MeasureTheory.Measure G) : PropA measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition. ] [μMeasureTheory.Measure G.RegularMeasureTheory.Measure.Regular.{u_1} {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α]
  (μ : MeasureTheory.Measure α) : PropA measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. ]
  (φG ≃ₜ+ G : GType u_1 ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  GType u_1) :
  MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φG ≃ₜ+ G •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.
      MeasureTheory.Measure.mapMeasureTheory.Measure.map.{u_4, u_5} {α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] (f : α → β)
  (μ : MeasureTheory.Measure α) : MeasureTheory.Measure βThe pushforward of a measure. It is defined to be `0` if `f` is not an almost everywhere
measurable function.  (⇑φG ≃ₜ+ G) μMeasureTheory.Measure G =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    μMeasureTheory.Measure G

theorem MeasureTheory.addEquivAddHaarChar_smul_eq_comap.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1]
  (μMeasureTheory.Measure G : MeasureTheory.MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 GType u_1)
  [μMeasureTheory.Measure G.IsAddHaarMeasureMeasureTheory.Measure.IsAddHaarMeasure.{u_3} {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  (μ : MeasureTheory.Measure G) : PropA measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition. ] [μMeasureTheory.Measure G.RegularMeasureTheory.Measure.Regular.{u_1} {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α]
  (μ : MeasureTheory.Measure α) : PropA measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. ]
  (φG ≃ₜ+ G : GType u_1 ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  GType u_1) :
  MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φG ≃ₜ+ G •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.
      μMeasureTheory.Measure G =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    MeasureTheory.Measure.comapMeasureTheory.Measure.comap.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β)
  (μ : MeasureTheory.Measure β) : MeasureTheory.Measure αPullback of a `Measure`. If `f` sends each measurable set to a null-measurable set,
then for each measurable set `s` we have `comap f μ s = μ (f '' s)`.

Note that if `f` is not injective, this definition assigns `Set.univ` measure zero.  (⇑φG ≃ₜ+ G) μMeasureTheory.Measure G

theorem MeasureTheory.addEquivAddHaarChar_refl.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1] :
  MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`. 
      (ContinuousAddEquiv.reflContinuousAddEquiv.refl.{u_1} (M : Type u_1) [TopologicalSpace M] [Add M] : M ≃ₜ+ MThe identity map is a continuous additive isomorphism.  GType u_1) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    1

theorem MeasureTheory.addEquivAddHaarChar_smul_preimage.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1]
  (μMeasureTheory.Measure G : MeasureTheory.MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 GType u_1)
  [μMeasureTheory.Measure G.IsAddHaarMeasureMeasureTheory.Measure.IsAddHaarMeasure.{u_3} {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  (μ : MeasureTheory.Measure G) : PropA measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition. ] [μMeasureTheory.Measure G.RegularMeasureTheory.Measure.Regular.{u_1} {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α]
  (μ : MeasureTheory.Measure α) : PropA measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. ]
  {XSet G : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 GType u_1} (φG ≃ₜ+ G : GType u_1 ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  GType u_1) :
  MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φG ≃ₜ+ G •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.
      μMeasureTheory.Measure G (Set.preimage.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set β) : Set αThe preimage of `s : Set β` by `f : α → β`, written `f ⁻¹' s`,
is the set of `x : α` such that `f x ∈ s`. ⇑φG ≃ₜ+ G ⁻¹'Set.preimage.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set β) : Set αThe preimage of `s : Set β` by `f : α → β`, written `f ⁻¹' s`,
is the set of `x : α` such that `f x ∈ s`.  XSet G)Set.preimage.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set β) : Set αThe preimage of `s : Set β` by `f : α → β`, written `f ⁻¹' s`,
is the set of `x : α` such that `f x ∈ s`.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    μMeasureTheory.Measure G XSet G

theorem MeasureTheory.addEquivAddHaarChar_smul_integral_map.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1]
  (μMeasureTheory.Measure G : MeasureTheory.MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 GType u_1)
  [μMeasureTheory.Measure G.IsAddHaarMeasureMeasureTheory.Measure.IsAddHaarMeasure.{u_3} {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  (μ : MeasureTheory.Measure G) : PropA measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition. ] [μMeasureTheory.Measure G.RegularMeasureTheory.Measure.Regular.{u_1} {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α]
  (μ : MeasureTheory.Measure α) : PropA measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. ]
  {fG → ℝ : GType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (φG ≃ₜ+ G : GType u_1 ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  GType u_1) :
  MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φG ≃ₜ+ G •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.
      ∫MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  (aG : GType u_1),MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral 
        fG → ℝ
          aG ∂MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral MeasureTheory.Measure.mapMeasureTheory.Measure.map.{u_4, u_5} {α : Type u_4} {β : Type u_5} [MeasurableSpace α] [MeasurableSpace β] (f : α → β)
  (μ : MeasureTheory.Measure α) : MeasureTheory.Measure βThe pushforward of a measure. It is defined to be `0` if `f` is not an almost everywhere
measurable function. 
          (⇑φG ≃ₜ+ G) μMeasureTheory.Measure G =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    ∫MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  (aG : GType u_1),MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  fG → ℝ aG ∂MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral μMeasureTheory.Measure G

theorem MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1]
  (μMeasureTheory.Measure G : MeasureTheory.MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 GType u_1)
  [μMeasureTheory.Measure G.IsAddHaarMeasureMeasureTheory.Measure.IsAddHaarMeasure.{u_3} {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  (μ : MeasureTheory.Measure G) : PropA measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition. ] [μMeasureTheory.Measure G.RegularMeasureTheory.Measure.Regular.{u_1} {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α]
  (μ : MeasureTheory.Measure α) : PropA measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. ]
  {fG → ℝ : GType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (φG ≃ₜ+ G : GType u_1 ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  GType u_1) :
  ∫MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  (aG : GType u_1),MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral 
      fG → ℝ
        aG ∂MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral MeasureTheory.Measure.comapMeasureTheory.Measure.comap.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β)
  (μ : MeasureTheory.Measure β) : MeasureTheory.Measure αPullback of a `Measure`. If `f` sends each measurable set to a null-measurable set,
then for each measurable set `s` we have `comap f μ s = μ (f '' s)`.

Note that if `f` is not injective, this definition assigns `Set.univ` measure zero. 
        (⇑φG ≃ₜ+ G) μMeasureTheory.Measure G =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φG ≃ₜ+ G •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.
      ∫MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  (aG : GType u_1),MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  fG → ℝ aG ∂MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral μMeasureTheory.Measure G

theorem MeasureTheory.addEquivAddHaarChar_trans.{u_1}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddGroupAddGroup.{u} (A : Type u) : Type uAn `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
 GType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  GType u_1] [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  GType u_1]
  [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  GType u_1] [IsTopologicalAddGroupIsTopologicalAddGroup.{u} (G : Type u) [TopologicalSpace G] [AddGroup G] : PropA topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.rightUniformSpace` and `isUniformAddGroup_of_addCommGroup`.  GType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  GType u_1]
  {φG ≃ₜ+ G ψG ≃ₜ+ G : GType u_1 ≃ₜ+ContinuousAddEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Add G] [Add H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between additive groups.
Note that both the map and its inverse have to be continuous.  GType u_1} :
  MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`. 
      (ψG ≃ₜ+ G.transContinuousAddEquiv.trans.{u_1, u_2, u_3} {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] [Add M]
  [Add N] {L : Type u_3} [Add L] [TopologicalSpace L] (cme1 : M ≃ₜ+ N) (cme2 : N ≃ₜ+ L) : M ≃ₜ+ LThe composition of two ContinuousAddEquiv.  φG ≃ₜ+ G) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  ψG ≃ₜ+ G *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.addEquivAddHaarCharMeasureTheory.addEquivAddHaarChar.{u_1} {G : Type u_1} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  [BorelSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] (φ : G ≃ₜ+ G) : NNRealIf `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
real factor by which `φ` scales Haar measures on `A`.  φG ≃ₜ+ G

theorem MeasureTheory.ringHaarChar_mul_integral.{u_1}
  {RType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_1]
  [TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  RType u_1]
  [IsTopologicalRingIsTopologicalRing.{u_1} (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] : PropA topological ring is a ring `R` where addition, multiplication and negation are continuous.

If `R` is a (unital) ring, then continuity of negation can be derived from continuity of
multiplication as it is multiplication with `-1`. (See
`IsTopologicalSemiring.continuousNeg_of_mul` and
`topological_semiring.to_topological_add_group`)  RType u_1]
  [LocallyCompactSpaceLocallyCompactSpace.{u_3} (X : Type u_3) [TopologicalSpace X] : PropThere are various definitions of "locally compact space" in the literature,
which agree for Hausdorff spaces but not in general.
This one is the precise condition on X needed
for the evaluation map `C(X, Y) × X → Y` to be continuous for all `Y`
when `C(X, Y)` is given the compact-open topology.

See also `WeaklyLocallyCompactSpace`, a typeclass that only assumes
that each point has a compact neighborhood.  RType u_1]
  [MeasurableSpaceMeasurableSpace.{u_7} (α : Type u_7) : Type u_7A measurable space is a space equipped with a σ-algebra.  RType u_1] [BorelSpaceBorelSpace.{u_6} (α : Type u_6) [TopologicalSpace α] [MeasurableSpace α] : PropA space with `MeasurableSpace` and `TopologicalSpace` structures such that
the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets.  RType u_1]
  (μMeasureTheory.Measure R : MeasureTheory.MeasureMeasureTheory.Measure.{u_6} (α : Type u_6) [MeasurableSpace α] : Type u_6A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.
 RType u_1)
  [μMeasureTheory.Measure R.IsAddHaarMeasureMeasureTheory.Measure.IsAddHaarMeasure.{u_3} {G : Type u_3} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G]
  (μ : MeasureTheory.Measure G) : PropA measure on an additive group is an additive Haar measure if it is left-invariant, and
gives finite mass to compact sets and positive mass to open sets.

Textbooks generally require an additional regularity assumption to ensure nice behavior on
arbitrary locally compact groups. Use `[IsAddHaarMeasure μ] [Regular μ]` or
`[IsAddHaarMeasure μ] [InnerRegular μ]` in these situations. Note that a Haar measure in our
sense is automatically regular and inner regular on second countable locally compact groups, as
checked just below this definition. ] [μMeasureTheory.Measure R.RegularMeasureTheory.Measure.Regular.{u_1} {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α]
  (μ : MeasureTheory.Measure α) : PropA measure `μ` is regular if
- it is finite on all compact sets;
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using compact sets:
  `μ(U) = sup {μ(K) | K ⊆ U compact}` for `U` open. ]
  {fR → ℝ : RType u_1 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (hfMeasurable f : MeasurableMeasurable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : PropA function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.  fR → ℝ)
  (uRˣ : RType u_1ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. ) :
  ↑(MeasureTheory.ringHaarCharMeasureTheory.ringHaarChar.{u_1} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
  [LocallyCompactSpace R] [MeasurableSpace R] [BorelSpace R] : Rˣ →ₜ* NNReal`ringHaarChar : Rˣ →ₜ* ℝ≥0` is the function sending a unit of
a locally compact topological ring `R` to the positive real factor
which left multiplication by the unit scales additive Haar measure by.
 uRˣ) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      ∫MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  (rR : RType u_1),MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  fR → ℝ (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.↑uRˣ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. rR)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ∂MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral μMeasureTheory.Measure R =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    ∫MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  (aR : RType u_1),MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral  fR → ℝ aR ∂MeasureTheory.integral.{u_6, u_7} {α : Type u_6} {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G]
  {x✝ : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → G) : GThe Bochner integral μMeasureTheory.Measure R