ι : Type ?u.6740
F : Type u_1
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A :
  ↑↑(AlternatingMap.measure (volumeForm o))
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) =
    1
⊢ AlternatingMap.measure (volumeForm o) = volume
ι : Type ?u.6740
F : Type u_1
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
⊢ AlternatingMap.measure (volumeForm o) = volume
have A : o.volumeForm.measure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1 :=
  Orientation.measure_orthonormalBasis o (stdOrthonormalBasis ℝ F)
ι : Type ?u.6740
F : Type u_1
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A :
  ↑↑(AlternatingMap.measure (volumeForm o))
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) =
    1
⊢ addHaarMeasure (Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) = volume
ι : Type ?u.6740
F : Type u_1
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A :
  ↑↑(AlternatingMap.measure (volumeForm o))
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) =
    1
⊢ AlternatingMap.measure (volumeForm o) = volume
rw [addHaarMeasure_unique o.volumeForm.measure
  (stdOrthonormalBasis ℝ F).toBasis.parallelepiped, A, one_smul]
no goals
ι : Type ?u.6740
F : Type u_1
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A :
  ↑↑(AlternatingMap.measure (volumeForm o))
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) =
    1
⊢ addHaarMeasure (Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) = volume
simp only [volume, Basis.addHaar]