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

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
⊢ Basis.orientation (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = x
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 ι
⊢ Basis.orientation
      (if Basis.orientation e = x then e else unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) =
    x
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 ι
h : Basis.orientation e = x
⊢ Basis.orientation e = x
exact h
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
⊢ Basis.orientation e ≠ x
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
⊢ Basis.orientation (unitsSMul e (Function.update 1 (Classical.arbitrary ι) (-1))) = x
rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]
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 ι
h : ¬Basis.orientation e = x
⊢ Basis.orientation e ≠ x
exact h