R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ det (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = det e ∨
    det (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ det (adjustToOrientation e x) = det e ∨ det (adjustToOrientation e x) = -det e
dsimp [Basis.adjustToOrientation]
case inl
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : Basis.orientation e = x
⊢ det e = det e ∨ det e = -det e

case inr
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = det e ∨
    det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
⊢ det (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = det e ∨
    det (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
split_ifs
case inl.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : Basis.orientation e = x
⊢ det e = det e
case inl
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : Basis.orientation e = x
⊢ det e = det e ∨ det e = -det e
left
no goals
case inl.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : Basis.orientation e = x
⊢ det e = det e
rfl
case inr.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
case inr
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = det e ∨
    det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
right
case inr.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ -1 • det e = -det e
case inr.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ det (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = -det e
simp [e.det_unitsSMul, ← Units.coe_prod, Finset.prod_update_of_mem]
case inr.h.H
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
x✝ : ι → M
⊢ ↑(-1 • det e) x✝ = ↑(-det e) x✝
case inr.h
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
⊢ -1 • det e = -det e
ext
no goals
case inr.h.H
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h✝ : ¬Basis.orientation e = x
x✝ : ι → M
⊢ ↑(-1 • det e) x✝ = ↑(-det e) x✝
simp