-- Mathlib/LinearAlgebra/Orientation.lean
theorem eq_or_eq_neg_of_isEmpty [IsEmpty ι] (o : Orientation R M ι) :
    o = positiveOrientation ∨ o = -positiveOrientation

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    ∑ i ∈ s, g i • ![f x, 1] i = 0 → ∀ i ∈ s, g i = 0
⊢ 0 ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ LinearIndependent R ![f x, 1]

Tactic:
convert h.map' f.toLinearMap f.ker

Result:
case h.e'_4
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ ![f x, 1] = ⇑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    ∑ i ∈ s, g i • ![f x, 1] i = 0 → ∀ i ∈ s, g i = 0
⊢ ∑ i : Fin (Nat.succ 0).succ, ![1, -f x] i • ![f x, 1] i = 0

Tactic:
simp [Fin.sum_univ_succ]

Result:
no goals

Proof state:
case h.e'_4
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ ![f x, 1] = ⇑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]

Tactic:
ext i

Result:
case h.e'_4.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
i : Fin (Nat.succ 0).succ
⊢ ![f x, 1] i = (⇑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) i

Proof state:
case h.e'_4.h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
i : Fin (Nat.succ 0).succ
⊢ ![f x, 1] i = (⇑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) i

Tactic:
fin_cases i <;> simp [f]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
o : Orientation R M ι
⊢ o = positiveOrientation ∨ o = -positiveOrientation

Tactic:
induction o using Module.Ray.ind with | h x hx =>
dsimp [positiveOrientation]
simp only [ray_eq_iff, sameRay_neg_swap]
rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]
intro h
set f : (M [⋀^ι]→ₗ[R] R) ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
have H : LinearIndependent R ![f x, 1] := by
  convert h.map' f.toLinearMap f.ker
  ext i
  fin_cases i <;> simp [f]
rw [linearIndependent_iff'] at H
simpa using H Finset.univ ![1, -f x] (by simp [Fin.sum_univ_succ]) 0 (by simp)

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ rayOfNeZero R x hx = rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1) ⋯ ∨
    rayOfNeZero R x hx = rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) ⋯

Tactic:
simp only [ray_eq_iff, sameRay_neg_swap]

Result:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    ∑ i ∈ s, g i • ![f x, 1] i = 0 → ∀ i ∈ s, g i = 0
⊢ False

Tactic:
simpa using H Finset.univ ![1, -f x] (by simp [Fin.sum_univ_succ]) 0 (by simp)

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ rayOfNeZero R x hx = positiveOrientation ∨ rayOfNeZero R x hx = -positiveOrientation

Tactic:
dsimp [positiveOrientation]

Result:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ rayOfNeZero R x hx = rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1) ⋯ ∨
    rayOfNeZero R x hx = rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) ⋯

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
⊢ False

Tactic:
set f : (M [⋀^ι]→ₗ[R] R) ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm

Result:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
⊢ False

Proof state:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H : LinearIndependent R ![f x, 1]
⊢ False

Tactic:
rw [linearIndependent_iff'] at H

Result:
case h
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    ∑ i ∈ s, g i • ![f x, 1] i = 0 → ∀ i ∈ s, g i = 0
⊢ False