no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : OrthonormalBasis (Fin n) ℝ E
⊢ abs (↑(volumeForm o) ↑v) = 1
simpa [o.volumeForm_robust' v v] using congr_arg abs v.toBasis.det_self