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 ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
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 ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = 1
apply (e.det_to_matrix_orthonormalBasis_real f).resolve_right
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 ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
this : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
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 ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
have : 0 < e.toBasis.det f := by
  rw [e.toBasis.orientation_eq_iff_det_pos] at h
  simpa using h
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 ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
this : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
linarith
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 ι
h : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f)
⊢ 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
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 ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
rw [e.toBasis.orientation_eq_iff_det_pos] at h
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 ι
h : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f)
⊢ 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
simpa using h