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 ι
⊢ Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x)) = Basis.det (OrthonormalBasis.toBasis e) ∨
    Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x)) = -Basis.det (OrthonormalBasis.toBasis e)
simpa using e.toBasis.det_adjustToOrientation x