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 ι
i : ι
⊢ ↑(adjustToOrientation e x) i = ↑e i ∨ ↑(adjustToOrientation e x) i = -↑e i
simpa [← e.toBasis_adjustToOrientation] using
  e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x i