-- Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
/-- A matrix whose nondiagonal entries are negative with the sum of the entries of each
column positive has nonzero determinant. -/
lemma det_ne_zero_of_sum_col_pos [DecidableEq n] {S : Type*} [LinearOrderedCommRing S]
    {A : Matrix n n S} (h1 : Pairwise fun i j => A i j < 0) (h2 : ∀ j, 0 < ∑ i, A i j) :
    A.det ≠ 0

Proof state:
case inr.intro.intro.inr.refine_3.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ 0 < (-1 • v) i

Tactic:
rw [Pi.smul_apply, neg_smul, one_smul, Left.neg_pos_iff]

Result:
case inr.intro.intro.inr.refine_3.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ v i < 0

Proof state:
case intro.intro
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
by_cases h : i = j₀

Result:
case pos
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
h : i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

case neg
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
j₀ : n
h_j₀ : Finset.univ.sup' ⋯ v = v j₀
i : n
hi : i ∈ Finset.univ
h : ¬i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Proof state:
case inr.intro.intro.inr.refine_2
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ (-1 • v) ᵥ* A = 0

Tactic:
rw [Matrix.vecMul_smul, h_vA, smul_zero]

Result:
no goals

Proof state:
case inr.intro.intro.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ ∃ j, ∑ i : n, A i j ≤ 0

Tactic:
refine this h1 inferInstance h2 (-1 • v) ?_ ?_ ?_

Result:
case inr.intro.intro.inr.refine_1
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ -1 • v ≠ 0

case inr.intro.intro.inr.refine_2
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ (-1 • v) ᵥ* A = 0

case inr.intro.intro.inr.refine_3
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ 0 < Finset.univ.sup' ⋯ (-1 • v)

Proof state:
case inr.intro.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
⊢ ∃ j, ∑ i : n, A i j ≤ 0

Tactic:
wlog h_sup : 0 < Finset.sup' Finset.univ Finset.univ_nonempty v

Result:
case inr.intro.intro.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (Pairwise fun i j => A i j < 0) →
      ∀ (h : Nonempty n),
        A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.univ.sup' ⋯ v
⊢ ∃ j, ∑ i : n, A i j ≤ 0

n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : Pairwise fun i j => A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.univ.sup' ⋯ v
⊢ ∃ j, ∑ i : n, A i j ≤ 0