mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
⊢ ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A✝ : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
⊢ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Submodule ℝ E
hs : s ≠ ⊤
⊢ μ ↑s = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
⊢ μ ↑s = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
⊢ FiniteDimensional ℝ (ι → ℝ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
⊢ LinearMap.det g = LinearMap.det f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
⊢ f = ↑e.symm ∘ₗ g ∘ₗ ↑e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
⊢ span K ↑(span ℤ (Set.range ⇑b)) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SFinite μ
hf : AEMeasurable f (μ.restrict s)
hg : AEMeasurable g (μ.restrict s)
hs : MeasurableSet s
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst✝¹ : AddCommGroup F
inst✝ : Module K F
f : E ≃ₗ[K] F
⊢ Submodule.map (↑(LinearEquiv.restrictScalars ℤ f)) (span ℤ (Set.range ⇑b)) = span ℤ (Set.range ⇑(b.map f))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ AEMeasurable (fun p ↦ f p.1) (μ.prod volume)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ AEMeasurable (fun p ↦ g p.1) (μ.prod volume)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)} (μ.prod volume)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
⊢ c • span ℤ (Set.range ⇑b) = span ℤ (Set.range ⇑(b.isUnitSMul ⋯))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det g ≠ 0
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
fg : f = ↑e.symm ∘ₗ g ∘ₗ ↑e
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑e
Cg : Continuous ⇑g
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑e.symm
this : (map (⇑e) μ).IsAddHaarMeasure
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : LinearOrder K
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
f : E ≃ₗ[K] F
⊢ ⇑f '' fundamentalDomain b = fundamentalDomain (b.map f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝³ : NormedField K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
b : Basis ι K E
inst✝ : LinearOrder K
ι' : Type u_4
e : ι ≃ ι'
⊢ fundamentalDomain (b.reindex e) = fundamentalDomain b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
⊢ fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x ↦ Set.Ico 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (b.repr ↑(floor b m)) i = ↑⌊(b.repr m) i⌋

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (b.repr ↑(ceil b m)) i = ↑⌈(b.repr m) i⌉

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)} (μ.prod volume)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ↑(floor b m) = m

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)} (μ.prod volume)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ⇑b)
⊢ ↑(ceil b m) = m

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
s : Set E
⊢ (map (⇑f) μ) s = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ (b.repr (fract b m)) i = Int.fract ((b.repr m) i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
x✝ : ι
⊢ (b.repr (fract b (fract b m))) x✝ = (b.repr (fract b m)) x✝

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
⊢ μ (⇑f ⁻¹' s) = ENNReal.ofReal |LinearMap.det ↑f.symm| * μ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
⊢ fract b (v + m) = fract b m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
⊢ fract b (m + v) = fract b m

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)} (μ.prod volume)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ = ‖∑ i, (b.repr (fract b m)) i • b i‖

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖∑ i, (b.repr (fract b m)) i • b i‖ = ‖∑ i, Int.fract ((b.repr m) i) • b i‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
⊢ μ (⇑f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ∑ i, ‖Int.fract ((b.repr m) i) • b i‖ = ∑ i, ‖Int.fract ((b.repr m) i)‖ * ‖b i‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ QuasiMeasurePreserving (⇑f) μ μ

Tactic:
refine ⟨f.continuous_of_finiteDimensional.measurable, ?_⟩

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ map (⇑f) μ ≪ μ
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
i : ι
x✝ : i ∈ Finset.univ
this : ‖Int.fract ((b.repr m) i)‖ ≤ 1
⊢ ‖Int.fract ((b.repr m) i)‖ * ‖b i‖ ≤ ‖b i‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
⊢ QuasiMeasurePreserving (⇑f) μ μ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : HasSolidNorm K
m : E
⊢ ‖fract b m‖ ≤ ∑ i, ‖b i‖

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
f : E →ₗ[ℝ] E := r • 1
⊢ LinearMap.det f ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
K : Type u_3
inst✝⁵ : NormedField K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ι
⊢ ((Basis.singleton ι K).repr ↑(floor (Basis.singleton ι K) k)) x✝ = ((Basis.singleton ι K).repr ↑⌊k⌋) x✝

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ map (fun x ↦ r • x) μ = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| • μ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
K : Type u_3
inst✝⁵ : NormedField K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ι
⊢ ((Basis.singleton ι K).repr (fract (Basis.singleton ι K) k)) x✝ = ((Basis.singleton ι K).repr (Int.fract k)) x✝

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
⊢ QuasiMeasurePreserving (fun x ↦ r • x) μ μ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁷ : NormedField K
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace K E
b : Basis ι K E
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
⊢ IsBounded (fundamentalDomain b)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : r ≠ 0
s : Set E
⊢ (map (fun x ↦ r • x) μ) s = ENNReal.ofReal |(r ^ finrank ℝ E)⁻¹| * μ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
x : ℝ
hx : x ∈ s
h'x : x ∈ ⋃ i ∈ A, T i
⊢ ∃ p ∈ A, x ∈ T p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Finite ι
x : E
⊢ ∃! v, v +ᵥ x ∈ fundamentalDomain b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
⊢ s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
s : Set E
⊢ μ (r • s) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hr : 0 ≤ r
s : Set E
⊢ μ (r • s) = ENNReal.ofReal (r ^ finrank ℝ E) * μ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ≥0
s : Set E
⊢ μ (r • s) = ↑r ^ finrank ℝ E * μ s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: μ : Measure ℝ
inst✝ : NullSingletonClass μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Ioo a b), p x
T : ↑s × ↑s → Set ℝ := fun p ↦ Ioo ↑p.1 ↑p.2
u : Set ℝ := ⋃ i, T i
hfinite : (s \ u).Finite
A : Set (↑s × ↑s)
A_count : A.Countable
hA : ⋃ i ∈ A, T i = ⋃ i, T i
this : s ⊆ s \ u ∪ ⋃ p ∈ A, s ∩ T p
⊢ μ.restrict (s \ u) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁶ : NormedField K
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace K E
b : Basis ι K E
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Fintype ι
⊢ E ⧸ span ℤ (Set.range ⇑b) ≃ ↑(fundamentalDomain b)

Tactic:
by

Goal state after: