awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingLeft
hc : M.det = 0
obtain : ∀ (v : n → A) (hvne : v ≠ 0) (hv : v ᵥ* M = 0), False
⊢ False

Tactic:
obtain ⟨v, hvne, hv⟩ := exists_vecMul_eq_zero_iff.mpr hc

Premises used: Iff.mpr, Matrix.exists_vecMul_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingLeft
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : v ᵥ* M = 0
⊢ False

Tactic:
hvne (separatingLeft_def.mp h v ?_)

Premises used: Matrix.separatingLeft_def, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingLeft
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : v ᵥ* M = 0
refine : ∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0
⊢ False

Tactic:
refine hvne (separatingLeft_def.mp h v ?_)

Premises used: Matrix.separatingLeft_def, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingLeft
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : v ᵥ* M = 0
⊢ ∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0

Tactic:
simp [dotProduct_mulVec, hv]

Premises used: Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.SeparatingRight ↔ M.det ≠ 0

Tactic:
⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).2⟩

Premises used: Matrix.Nondegenerate.separatingRight, Matrix.nondegenerate_of_det_ne_zero, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
refine : ∀ (h : M.SeparatingRight) (hc : M.det = 0), False
⊢ M.SeparatingRight ↔ M.det ≠ 0

Tactic:
refine ⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).2⟩
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingRight
hc : M.det = 0
obtain : ∀ (v : n → A) (hvne : v ≠ 0) (hv : M *ᵥ v = 0), False
⊢ False

Tactic:
obtain ⟨v, hvne, hv⟩ := exists_mulVec_eq_zero_iff.mpr hc

Premises used: Iff.mpr, Matrix.exists_mulVec_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingRight
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : M *ᵥ v = 0
⊢ False

Tactic:
hvne (separatingRight_def.mp h v ?_)

Premises used: Iff.mp, Matrix.separatingRight_def
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingRight
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : M *ᵥ v = 0
refine : ∀ (v_1 : n → A), v_1 ⬝ᵥ M *ᵥ v = 0
⊢ False

Tactic:
refine hvne (separatingRight_def.mp h v ?_)

Premises used: Iff.mp, Matrix.separatingRight_def
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingRight
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : M *ᵥ v = 0
⊢ ∀ (v_1 : n → A), v_1 ⬝ᵥ M *ᵥ v = 0

Tactic:
simp [hv]
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : N.Nondegenerate
simp : ∀ (h : N.det ≠ 0), M.det * N.det ≠ 0 ↔ M.det ≠ 0
⊢ (M * N).Nondegenerate ↔ M.Nondegenerate

Tactic:
simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢

Premises used: Matrix.det_mul, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : N.det ≠ 0
⊢ M.det * N.det ≠ 0 ↔ M.det ≠ 0

Tactic:
mul_ne_zero_iff_right h

Premises used: mul_ne_zero_iff_right
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : N.det ≠ 0
⊢ M.det * N.det ≠ 0 ↔ M.det ≠ 0

Tactic:
exact mul_ne_zero_iff_right h

Premises used: mul_ne_zero_iff_right
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : N.Nondegenerate
simp : ∀ (h : N.det ≠ 0), M.det * N.det ≠ 0 ↔ M.det ≠ 0
⊢ (M * N).Nondegenerate ↔ M.Nondegenerate

Tactic:
classical
  simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
  exact mul_ne_zero_iff_right h

Premises used: Matrix.det_mul, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : M.Nondegenerate
simp : ∀ (h : M.det ≠ 0), M.det * N.det ≠ 0 ↔ N.det ≠ 0
⊢ (M * N).Nondegenerate ↔ N.Nondegenerate

Tactic:
simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢

Premises used: Matrix.det_mul, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : M.det ≠ 0
⊢ M.det * N.det ≠ 0 ↔ N.det ≠ 0

Tactic:
mul_ne_zero_iff_left h

Premises used: mul_ne_zero_iff_left
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : M.det ≠ 0
⊢ M.det * N.det ≠ 0 ↔ N.det ≠ 0

Tactic:
exact mul_ne_zero_iff_left h

Premises used: mul_ne_zero_iff_left
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : M.Nondegenerate
simp : ∀ (h : M.det ≠ 0), M.det * N.det ≠ 0 ↔ N.det ≠ 0
⊢ (M * N).Nondegenerate ↔ N.Nondegenerate

Tactic:
classical
  simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
  exact mul_ne_zero_iff_left h

Premises used: Matrix.det_mul, Matrix.nondegenerate_iff_det_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Finite n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M : Matrix n n A
t : A
h : t ≠ 0
have : ∀ (this : (α : Type u_1) → [Finite α] → Fintype α), (t • M).Nondegenerate ↔ M.Nondegenerate
⊢ (t • M).Nondegenerate ↔ M.Nondegenerate

Tactic:
have := Fintype.ofFinite
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Finite n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M : Matrix n n A
t : A
h : t ≠ 0
this : (α : Type u_1) → [Finite α] → Fintype α
rw :
  ((∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → w = 0) ↔
    (∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ M *ᵥ w = 0) → w = 0
⊢ (t • M).Nondegenerate ↔ M.Nondegenerate

Tactic:
rw [nondegenerate_def, nondegenerate_def]

Premises used: Matrix.nondegenerate_def
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Finite n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M : Matrix n n A
t : A
h : t ≠ 0
this : (α : Type u_1) → [Finite α] → Fintype α
⊢ ((∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → w = 0) ↔
    (∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ M *ᵥ w = 0) → w = 0

Tactic:
simp [smul_mulVec, mul_eq_zero_iff_left h]

Premises used: mul_eq_zero_iff_left, Matrix.smul_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, A i j)
inl : IsEmpty n → A.det ≠ 0
inr : Nonempty n → A.det ≠ 0
⊢ A.det ≠ 0

Tactic:
cases isEmpty_or_nonempty n

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, A i j)
h : IsEmpty n
⊢ A.det ≠ 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, A i j)
h : Nonempty n
inr : ∀ (h2 : A.det = 0), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
⊢ A.det ≠ 0

Tactic:
contrapose! h2
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h : Nonempty n
h2 : A.det = 0
inr : ∀ (v : n → S) (h_vnz : v ≠ 0) (h_vA : v ᵥ* A = 0), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0

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

Premises used: Iff.mpr, Matrix.exists_vecMul_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
inr :
  ∀
    (this :
      ∀ {n : Type u_1} [inst : Fintype n] [inst_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
        [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0)
    (h_sup : ¬0 < Finset.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
wlog :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0

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

Premises used: Finset.univ, Finset.univ_nonempty, Finset.sup'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
h_sup : ¬0 < Finset.sup' Finset.univ ⋯ v
⊢ HSMul.hSMul (α := ℤ) (-1) v ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
h_sup : ¬0 < Finset.sup' Finset.univ ⋯ v
inr : HSMul.hSMul (α := ℤ) (-1) v ᵥ* A = 0
inr₁ : 0 < Finset.sup' Finset.univ ⋯ (HSMul.hSMul (α := ℤ) (-1) v)
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0

Tactic:
refine this h1 inferInstance h2 (-1 • v) (by simp [*]) ?_ ?_

Premises used: inferInstance, HSMul.hSMul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
h_sup : ¬0 < Finset.sup' Finset.univ ⋯ v
inr : HSMul.hSMul (α := ℤ) (-1) (v ᵥ* A) = 0
inr₁ : HSMul.hSMul (α := ℤ) (β := n → S) (-1) 0 = 0
inr₂ inr₃ : Eq (α := n → S) 0 0
⊢ HSMul.hSMul (α := ℤ) (-1) v ᵥ* A = 0

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

Premises used: Matrix.smul_vecMul, smul_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
h_sup : ¬0 < Finset.sup' Finset.univ ⋯ v
inr : ∀ (i : n) (hi : v i ≠ 0 i), 0 < Finset.sup' Finset.univ ⋯ (HSMul.hSMul (α := ℤ) (-1) v)
⊢ 0 < Finset.sup' Finset.univ ⋯ (HSMul.hSMul (α := ℤ) (-1) v)

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
h_sup : ¬0 < Finset.sup' Finset.univ ⋯ v
i : n
hi : v i ≠ 0 i
inr : ∀ (h_sup : ¬∃ (b : n), 0 < v b), ∃ (b : n), 0 < HSMul.hSMul (α := ℤ) (-1) v b
⊢ 0 < Finset.sup' Finset.univ ⋯ (HSMul.hSMul (α := ℤ) (-1) v)

Tactic:
simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢

Premises used: Finset.mem_univ, Finset.lt_sup'_iff, true_and
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ (b : n), 0 < v b
⊢ ∀ (x : n), v x ≤ 0

Tactic:
simp_rw [not_exists, not_lt] at h_sup

Premises used: not_exists, not_lt
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ ∃ (b : n), 0 < HSMul.hSMul (α := ℤ) (-1) v b

Tactic:
⟨i, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
inr : 0 < HSMul.hSMul (α := ℤ) (-1) v i
⊢ ∃ (b : n), 0 < HSMul.hSMul (α := ℤ) (-1) v b

Tactic:
refine ⟨i, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
inr : v i < 0
⊢ 0 < HSMul.hSMul (α := ℤ) (-1) v i

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

Premises used: neg_smul, one_smul, Left.neg_pos_iff, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ v i < 0

Tactic:
Ne.lt_of_le hi (h_sup i)

Premises used: Ne.lt_of_le
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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_5 : DecidableEq n] {S : Type u_2} [inst_6 : CommRing S]
    [inst_7 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S} (h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ v i < 0

Tactic:
exact Ne.lt_of_le hi (h_sup i)

Premises used: Ne.lt_of_le
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v
obtain : ∀ (j₀ : n) (h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0

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

Premises used: Finset.univ_nonempty, Finset.exists_mem_eq_sup'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0

Tactic:
⟨j₀, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
refine : LE.le.{u_2} (α := S) (∑ i : n, A i j₀) 0
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0

Tactic:
refine ⟨j₀, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ 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.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
rw : LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) 0
⊢ LE.le.{u_2} (α := S) (∑ i : n, A i j₀) 0

Tactic:
rw [← mul_le_mul_iff_right₀ (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]

Premises used: Finset.mul_sum, MulZeroClass.mul_zero, mul_le_mul_iff_right₀