case mp
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 e) = Basis.det (OrthonormalBasis.toBasis f) →
    Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)

case mpr
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.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f) →
    Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis 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 ι
⊢ Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f) ↔
    Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
constructor
case mp
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.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
case mp
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 e) = Basis.det (OrthonormalBasis.toBasis f) →
    Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
intro h
case mp
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.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis e)) (_ : Basis.det (OrthonormalBasis.toBasis e) ≠ 0) =
    rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis f)) (_ : Basis.det (OrthonormalBasis.toBasis f) ≠ 0)
case mp
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.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
dsimp [Basis.orientation]
no goals
case mp
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.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis e)) (_ : Basis.det (OrthonormalBasis.toBasis e) ≠ 0) =
    rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis f)) (_ : Basis.det (OrthonormalBasis.toBasis f) ≠ 0)
congr
case mpr
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) = Basis.det (OrthonormalBasis.toBasis f)
case mpr
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.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f) →
    Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
intro h
case mpr
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)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    Basis.det (OrthonormalBasis.toBasis f)
case mpr
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) = Basis.det (OrthonormalBasis.toBasis f)
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
no goals
case mpr
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)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    Basis.det (OrthonormalBasis.toBasis f)
simp [e.det_to_matrix_orthonormalBasis_of_same_orientation f h]