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 ι
i : ι
⊢ ↑(if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
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 ι
i : ι
⊢ ↑(adjustToOrientation e x) i = ↑e i ∨ ↑(adjustToOrientation e x) i = -↑e i
rw [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 ι
i : ι
h : Basis.orientation e = x
⊢ ↑e i = ↑e i ∨ ↑e i = -↑e i

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 ι
i : ι
h : ¬Basis.orientation e = x
⊢ ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
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 ι
i : ι
⊢ ↑(if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
split_ifs with h
no goals
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 ι
i : ι
h : Basis.orientation e = x
⊢ ↑e i = ↑e i ∨ ↑e i = -↑e i
simp
no goals
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 ι
i : ι
h : ¬Basis.orientation e = x
⊢ ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = ↑e i ∨
    ↑(unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) i = -↑e i
by_cases hi : i = Classical.arbitrary ι <;> simp [unitsSMul_apply, hi]