refactor: use SignType to define IsTotallyUnimodular (#19345)

This is a little easier than working with a three-element disjunction.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Matrix.2EfromRows.20TU.20.28help.20wanted.29/near/483771954)

Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

@@ -5,6 +5,7 @@ Authors: Martin Dvorak, Vladimir Kolmogorov, Ivan Sergeev
 -/
 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
 import Mathlib.Data.Matrix.ColumnRowPartitioned
+import Mathlib.Data.Sign
 
 /-!
 # Totally unimodular matrices
@@ -29,24 +30,20 @@ namespace Matrix
 variable {m n R : Type*} [CommRing R]
 
 /-- `A.IsTotallyUnimodular` means that every square submatrix of `A` (not necessarily contiguous)
-has determinant `0` or `1` or `-1`. -/
+has determinant `0` or `1` or `-1`; that is, the determinant is in the range of `SignType.cast`. -/
 def IsTotallyUnimodular (A : Matrix m n R) : Prop :=
   ∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n, f.Injective → g.Injective →
-    (A.submatrix f g).det = 0 ∨
-    (A.submatrix f g).det = 1 ∨
-    (A.submatrix f g).det = -1
+    (A.submatrix f g).det ∈ Set.range SignType.cast
 
 lemma isTotallyUnimodular_iff (A : Matrix m n R) : A.IsTotallyUnimodular ↔
     ∀ k : ℕ, ∀ f : Fin k → m, ∀ g : Fin k → n,
-      (A.submatrix f g).det = 0 ∨
-      (A.submatrix f g).det = 1 ∨
-      (A.submatrix f g).det = -1 := by
+      (A.submatrix f g).det ∈ Set.range SignType.cast := by
   constructor <;> intro hA
   · intro k f g
-    if h : f.Injective ∧ g.Injective then
-      exact hA k f g h.1 h.2
-    else
-      left
+    by_cases h : f.Injective ∧ g.Injective
+    · exact hA k f g h.1 h.2
+    · refine ⟨0, ?_⟩
+      rw [SignType.coe_zero, eq_comm]
       simp_rw [not_and_or, Function.not_injective_iff] at h
       obtain ⟨i, j, hfij, hij⟩ | ⟨i, j, hgij, hij⟩ := h
       · rw [← det_transpose, transpose_submatrix]
@@ -59,10 +56,10 @@ lemma isTotallyUnimodular_iff (A : Matrix m n R) : A.IsTotallyUnimodular ↔
 
 lemma IsTotallyUnimodular.apply {A : Matrix m n R} (hA : A.IsTotallyUnimodular)
     (i : m) (j : n) :
-    A i j = 0 ∨ A i j = 1 ∨ A i j = -1 := by
+    A i j ∈ Set.range SignType.cast := by
   let f : Fin 1 → m := (fun _ => i)
   let g : Fin 1 → n := (fun _ => j)
-  convert hA 1 f g (Function.injective_of_subsingleton f) (Function.injective_of_subsingleton g) <;>
+  convert hA 1 f g (Function.injective_of_subsingleton f) (Function.injective_of_subsingleton g)
   exact (det_fin_one (A.submatrix f g)).symm
 
 lemma IsTotallyUnimodular.submatrix {A : Matrix m n R} (hA : A.IsTotallyUnimodular) {k : ℕ}
@@ -96,7 +93,8 @@ lemma fromRows_row0_isTotallyUnimodular_iff (A : Matrix m n R) {m' : Type*} :
   · exact hA k (Sum.inl ∘ f) g
   · if zerow : ∃ i, ∃ x', f i = Sum.inr x' then
       obtain ⟨i, _, _⟩ := zerow
-      left
+      use 0
+      rw [eq_comm]
       apply det_eq_zero_of_row_eq_zero i
       intro
       simp_all