theorem
Matrix.vertex_integral_of_det_pm_one
{m n : ℕ}
(A : Matrix (Fin m) (Fin n) ℤ)
(b : Fin m → ℤ)
(rows : Fin n → Fin m)
(hrows : Function.Injective rows)
(y : Fin n → ℝ)
(hy_feasible : ∀ (i : Fin m), ∑ j : Fin n, ↑(A i j) * y j ≤ ↑(b i))
(hy_tight : ∀ (k : Fin n), ∑ j : Fin n, ↑(A (rows k) j) * y j = ↑(b (rows k)))
(hdet : (A.submatrix rows id).det = 1 ∨ (A.submatrix rows id).det = -1)
(j : Fin n)
: