no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
v : ι → E
⊢ abs (↑(Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x))) v) =
    abs (↑(Basis.det (OrthonormalBasis.toBasis e)) v)
simp [toBasis_adjustToOrientation]