E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ ↑↑(Basis.addHaar b) (parallelepiped v) = ENNReal.ofReal (abs (↑(Basis.det b) v))
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
⊢ ↑↑(Basis.addHaar b) (parallelepiped v) = ENNReal.ofReal (abs (↑(Basis.det b) v))
have : FiniteDimensional ℝ G := FiniteDimensional.of_fintype_basis b
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ↑↑(Basis.addHaar b) (parallelepiped v) = ENNReal.ofReal (abs (↑(Basis.det b) v))
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ ↑↑(Basis.addHaar b) (parallelepiped v) = ENNReal.ofReal (abs (↑(Basis.det b) v))
have A : parallelepiped v = b.constr ℕ v '' parallelepiped b := by
  rw [image_parallelepiped]
  refine congr_arg _ <| funext fun i ↦ ?_
  exact (b.constr_basis ℕ v i).symm
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ENNReal.ofReal (abs (↑LinearMap.det (↑(Basis.constr b ℕ) v))) * ↑↑(Basis.addHaar b) (parallelepiped ↑b) =
    ENNReal.ofReal (abs (↑(Basis.det b) v))
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ↑↑(Basis.addHaar b) (parallelepiped v) = ENNReal.ofReal (abs (↑(Basis.det b) v))
rw [A, add_haar_image_linearMap]
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ENNReal.ofReal (abs (↑LinearMap.det (↑(Basis.constr b ℕ) v))) * 1 = ENNReal.ofReal (abs (↑(Basis.det b) v))
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ENNReal.ofReal (abs (↑LinearMap.det (↑(Basis.constr b ℕ) v))) * ↑↑(Basis.addHaar b) (parallelepiped ↑b) =
    ENNReal.ofReal (abs (↑(Basis.det b) v))
erw [b.addHaar_self]
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ENNReal.ofReal (abs (Matrix.det (Basis.toMatrix b v))) = ENNReal.ofReal (abs (↑(Basis.det b) v))
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ENNReal.ofReal (abs (↑LinearMap.det (↑(Basis.constr b ℕ) v))) * 1 = ENNReal.ofReal (abs (↑(Basis.det b) v))
rw [mul_one, ← LinearMap.det_toMatrix b, ← Basis.toMatrix_eq_toMatrix_constr]
no goals
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
⊢ ENNReal.ofReal (abs (Matrix.det (Basis.toMatrix b v))) = ENNReal.ofReal (abs (↑(Basis.det b) v))
rfl
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = parallelepiped (↑(↑(Basis.constr b ℕ) v) ∘ ↑b)
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = ↑(↑(Basis.constr b ℕ) v) '' parallelepiped ↑b
rw [image_parallelepiped]
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
i : ι
⊢ v i = (↑(↑(Basis.constr b ℕ) v) ∘ ↑b) i
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = parallelepiped (↑(↑(Basis.constr b ℕ) v) ∘ ↑b)
refine congr_arg _ <| funext fun i ↦ ?_
no goals
E : Type ?u.2040807
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : MeasurableSpace E
inst✝¹¹ : BorelSpace E
inst✝¹⁰ : FiniteDimensional ℝ E
μ : Measure E
inst✝⁹ : IsAddHaarMeasure μ
F : Type ?u.2041476
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace F
s : Set E
ι : Type u_1
G : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
i : ι
⊢ v i = (↑(↑(Basis.constr b ℕ) v) ∘ ↑b) i
exact (b.constr_basis ℕ v i).symm