-- 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 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, v j₀ * A i j₀ ≤ 0

Tactic:
rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]

Result:
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, v j₀ * A i j₀ ≤ ∑ i : n, v i * A i j₀

Proof state:
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₀

Tactic:
exact (mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

Result:
no goals

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
⊢ ∃ b, 0 < (-1 • v) b

Tactic:
refine ⟨i, ?_⟩

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
⊢ 0 < (-1 • v) i

Proof state:
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

Tactic:
obtain ⟨j₀, -, h_j₀⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty v

Result:
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₀
⊢ ∃ j, ∑ i : n, A i j ≤ 0

Proof state:
case 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
⊢ ∃ j, ∑ i : n, A i j ≤ 0

Tactic:
obtain ⟨v, ⟨h_vnz, h_vA⟩⟩ := Matrix.exists_vecMul_eq_zero_iff.mpr h2

Result:
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

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 : ¬∃ b, 0 < v b
⊢ ∃ b, 0 < (-1 • v) b

Tactic:
simp_rw [not_exists, not_lt] at h_sup

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
⊢ ∃ b, 0 < (-1 • v) b

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, v j₀ * A i j₀ ≤ ∑ i : n, v i * A i j₀

Tactic:
refine Finset.sum_le_sum (fun i hi => ?_)

Result:
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₀

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₀
⊢ ∃ j, ∑ i : n, A i j ≤ 0

Tactic:
refine ⟨j₀, ?_⟩

Result:
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, A i j₀ ≤ 0