R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
⊢ x₁ = x₂ ∨ x₁ = -x₂
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
⊢ x₁ = x₂ ∨ x₁ = -x₂
have e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
⊢ x₁ = x₂ ∨ x₁ = -x₂
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
⊢ x₁ = x₂ ∨ x₁ = -x₂
letI := Classical.decEq ι
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
⊢ x₁ = x₂ ∨ x₁ = -x₂
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
⊢ x₁ = x₂ ∨ x₁ = -x₂
have orientation_neg_neg :
  ∀ f : Basis ι R M,  - -Basis.orientation f = Basis.orientation f := by simp
no goals
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
⊢ x₁ = x₂ ∨ x₁ = -x₂
rcases e.orientation_eq_or_eq_neg x₁ with (h₁ | h₁) <;>
  rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂) <;> simp [h₁, h₂, orientation_neg_neg]
no goals
R : Type u_1
inst✝³ : LinearOrderedField R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
_i : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ (f : Basis ι R M), - -Basis.orientation f = Basis.orientation f
simp