E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
haveI := Fin.pos_iff_nonempty.1 hn
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
haveI := finiteDimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E)
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <|
  finCongr h).orientation_adjustToOrientation x