case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx = positiveOrientation ∨ rayOfNeZero R x hx = -positiveOrientation
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
o : Orientation R M ι
⊢ o = positiveOrientation ∨ o = -positiveOrientation
induction' o using Module.Ray.ind with x hx
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx =
      rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1)
        (_ :
          ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) ∨
    rayOfNeZero R x hx =
      rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) (_ : ¬-AlternatingMap.constOfIsEmpty R M ι 1 = 0)
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx = positiveOrientation ∨ rayOfNeZero R x hx = -positiveOrientation
dsimp [positiveOrientation]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ rayOfNeZero R x hx =
      rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1)
        (_ :
          ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) ∨
    rayOfNeZero R x hx =
      rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) (_ : ¬-AlternatingMap.constOfIsEmpty R M ι 1 = 0)
simp only [ray_eq_iff, sameRay_neg_swap]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ ¬LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)
rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
⊢ False
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
⊢ ¬LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
intro h
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ False
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
⊢ False
set f : AlternatingMap R M R ι ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H : LinearIndependent R ![↑f x, 1]
⊢ False
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ False
have H : LinearIndependent R ![f x, 1] := by
  convert h.map' f.toLinearMap f.ker
  ext i
  fin_cases i <;> simp
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ (Nat.succ 0)))) (g : Fin (Nat.succ (Nat.succ 0)) → R),
    ∑ i in s, g i • Matrix.vecCons (↑f x) ![1] i = 0 → ∀ (i : Fin (Nat.succ (Nat.succ 0))), i ∈ s → g i = 0
⊢ False
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H : LinearIndependent R ![↑f x, 1]
⊢ False
rw [linearIndependent_iff'] at H
no goals
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ (Nat.succ 0)))) (g : Fin (Nat.succ (Nat.succ 0)) → R),
    ∑ i in s, g i • Matrix.vecCons (↑f x) ![1] i = 0 → ∀ (i : Fin (Nat.succ (Nat.succ 0))), i ∈ s → g i = 0
⊢ False
simpa using H Finset.univ ![1, -f x] (by simp [Fin.sum_univ_succ]) 0 (by simp)
case h.e'_4
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ ![↑f x, 1] = ↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ LinearIndependent R ![↑f x, 1]
convert h.map' f.toLinearMap f.ker
case h.e'_4.h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
i : Fin (Nat.succ (Nat.succ 0))
⊢ Matrix.vecCons (↑f x) ![1] i = (↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) i
case h.e'_4
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ ![↑f x, 1] = ↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]
ext i
no goals
case h.e'_4.h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
i : Fin (Nat.succ (Nat.succ 0))
⊢ Matrix.vecCons (↑f x) ![1] i = (↑↑f ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) i
fin_cases i <;> simp
no goals
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ (Nat.succ 0)))) (g : Fin (Nat.succ (Nat.succ 0)) → R),
    ∑ i in s, g i • Matrix.vecCons (↑f x) ![1] i = 0 → ∀ (i : Fin (Nat.succ (Nat.succ 0))), i ∈ s → g i = 0
⊢ ∑ i : Fin (Nat.succ (Nat.succ 0)), Matrix.vecCons 1 ![-↑f x] i • Matrix.vecCons (↑f x) ![1] i = 0
simp [Fin.sum_univ_succ]
no goals
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_2
inst✝¹ : Nontrivial R
inst✝ : IsEmpty ι
x : AlternatingMap R M R ι
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : AlternatingMap R M R ι ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ (Nat.succ 0)))) (g : Fin (Nat.succ (Nat.succ 0)) → R),
    ∑ i in s, g i • Matrix.vecCons (↑f x) ![1] i = 0 → ∀ (i : Fin (Nat.succ (Nat.succ 0))), i ∈ s → g i = 0
⊢ 0 ∈ Finset.univ
simp