mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
A : (interior (Icc 0 1)).Nonempty
⊢ (⇑b.equivFunL.symm.toHomeomorph '' interior (Icc 0 1)).Nonempty

Tactic:
image_nonempty

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
A : (interior (Icc 0 1)).Nonempty
⊢ (interior (Icc 0 1)).Nonempty
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
A : (interior (Icc 0 1)).Nonempty
⊢ (interior (Icc 0 1)).Nonempty

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
A : (interior (Icc 0 1)).Nonempty
⊢ (interior (Icc 0 1)).Nonempty
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖b‖₊ = ‖b‖₊

pp: case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ∀ (x : ι), x ≠ i → ‖(single (↑p) i b).ofLp x‖₊ ^ ↑p = 0

Tactic:
]

Goal state after:
case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ∀ (x : ι), x ≠ i → ‖(single (↑p) i b).ofLp x‖₊ ^ ↑p = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
⊢ Measure.map (⇑(toLin' (Matrix.diagonal D))) volume =
    ofReal (|(Matrix.diagonal D).det⁻¹| * |(Matrix.diagonal D).det|) •
      Measure.map (⇑(toLin' (Matrix.diagonal D))) volume

Tactic:
← abs_mul,

Goal state after:
case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
⊢ Measure.map (⇑(toLin' (Matrix.diagonal D))) volume =
    ofReal |(Matrix.diagonal D).det⁻¹ * (Matrix.diagonal D).det| • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case coe
ι : Type u_2
β : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
j : ι
hij : j ≠ i
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
⊢ Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = Measure.map (⇑(toLin' (Matrix.diagonal D))) volume

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ ‖b₁ - b₂‖₊ = ‖b₁ - b₂‖₊

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped).IsAddHaarMeasure

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped).IsAddHaarMeasure
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ SigmaFinite (addHaarMeasure b.parallelepiped)

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ SigmaFinite (addHaarMeasure b.parallelepiped)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
b : Basis ι ℝ E
μ : Measure E
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsAddLeftInvariant
⊢ addHaarMeasure b.parallelepiped = μ ↔ μ ↑b.parallelepiped = 1

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
b : Basis ι ℝ E
μ : Measure E
inst✝¹ : SigmaFinite μ
inst✝ : μ.IsAddLeftInvariant
⊢ addHaarMeasure b.parallelepiped = μ ↔ μ ↑b.parallelepiped = 1
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
⊢ b.addHaar = b.addHaar

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped) (_root_.parallelepiped ⇑b) = 1

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_3
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped) (_root_.parallelepiped ⇑b) = 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = ((Pi.basisFun ℝ ι).map b.equivFun.symm).parallelepiped

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ b.parallelepiped = ((Pi.basisFun ℝ ι).map b.equivFun.symm).parallelepiped
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ ofReal (|B.det⁻¹| * |A.det⁻¹|) • volume = ofReal |(A.det * B.det)⁻¹| • volume

pp: case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

pp: case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)

Tactic:
← abs_mul,

Goal state after:
case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ ofReal |B.det⁻¹ * A.det⁻¹| • volume = ofReal |(A.det * B.det)⁻¹| • volume

case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖

Tactic:
]

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

Goal state before:
pp: case hmul
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ ofReal |A.det⁻¹ * B.det⁻¹| • volume = ofReal |A.det⁻¹ * B.det⁻¹| • volume

pp: case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

pp: case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)

Tactic:
]

Goal state after:
case hmul.hg
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' A)

case hmul.hf
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
A B : Matrix ι ι ℝ
a✝¹ : A.det ≠ 0
a✝ : B.det ≠ 0
IHA : Measure.map (⇑(toLin' A)) volume = ofReal |A.det⁻¹| • volume
IHB : Measure.map (⇑(toLin' B)) volume = ofReal |B.det⁻¹| • volume
⊢ Measurable ⇑(toLin' B)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ b.addHaar (⇑f ⁻¹' _root_.parallelepiped (⇑↑f ∘ ⇑b)) =
    b.addHaar (⇑(↑f).toEquiv ⁻¹' ⇑(↑f).toEquiv '' _root_.parallelepiped ⇑b)

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ b.addHaar (⇑f ⁻¹' _root_.parallelepiped (⇑↑f ∘ ⇑b)) =
    b.addHaar (⇑(↑f).toEquiv ⁻¹' ⇑(↑f).toEquiv '' _root_.parallelepiped ⇑b)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist (toLp p x) (toLp p y) = 0
⊢ x = y

Tactic:
]

Goal state after:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist (toLp p x) (toLp p y) = 0
⊢ x = y
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖

Tactic:
]

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 : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ μ (range u + s) = μ (range u + s)

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ Measure.map (⇑(toLin' M)) volume = ofReal |M.det⁻¹| • volume

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ Measure.map (⇑(toLin' M)) volume = ofReal |M.det⁻¹| • volume
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 : Set E
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
⊢ μ s ≤ 0

Tactic:
]

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
s : Set E
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
⊢ μ s ≤ 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
hf : M.det ≠ 0
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ M.det ≠ 0

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
hf : M.det ≠ 0
A : LinearMap.det f = M.det
B : f = toLin' M
⊢ M.det ≠ 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

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

pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ∫⁻ (x : α), volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
x : α
⊢ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)} = if x ∈ s then ofReal (g x - f x) else 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

pp: case hs
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ MeasurableSet s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ ∫⁻ (a : α) in s, ofReal (g a - f a) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

case hs
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
h : (fun x ↦ volume {a | x ∈ s ∧ a ∈ Ioo (f x) (g x)}) = s.indicator fun x ↦ ofReal (g x - f x)
⊢ MeasurableSet s
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 = x

Tactic:
]

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
h₁ : (fun y ↦ ofReal ((g - f) y)) =ᵐ[μ.restrict s] fun y ↦ ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) =
    (μ.prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)

Tactic:
]

Goal state after:
α : 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)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) =
    (μ.prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

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

Tactic:
]

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

Goal state before:
pp: case inr
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.direction = ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0

Tactic:
]

Goal state after:
case inr
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.direction = ⊤
hne : (↑s).Nonempty
⊢ μ ↑s = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
this : μ = μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ ↑(piIcc01 ι) • volume =
    ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ ↑(piIcc01 ι) • volume

Tactic:
]

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

Goal state before:
pp: case e'_2
α : 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)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ((μ.prod volume).restrict (s ×ˢ univ)) (regionBetween f g s)

Tactic:
]

Goal state after:
case e'_2
α : 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)
h₂ :
  ((μ.restrict s).prod volume) (regionBetween f g s) =
    ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
⊢ (μ.prod volume) (regionBetween f g s) = ((μ.prod volume).restrict (s ×ˢ univ)) (regionBetween f g s)
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 (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
]

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
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f