awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
have 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 sorry v), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0)
  (h_sup : ¬0 < Finset.sup' Finset.univ sorry v), ∃ (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
have 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 sorry v), ∃ (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
Cleared hypotheses: inst_1, S, inst_2, inst_3, inst_4, A, h1, h, h2, v, h_vnz, h_vA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
have inr : HSMul.hSMul (α := ℤ) (-1) v ᵥ* A = 0
Tactic: refine this h1 inferInstance h2 (-1 • v) (by simp [*]) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
have inr₁ : 0 < Finset.sup' Finset.univ sorry (HSMul.hSMul (α := ℤ) (-1) v)
Tactic: refine this h1 inferInstance h2 (-1 • v) (by simp [*]) ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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 ᵥ* A = 0
have inr : HSMul.hSMul (α := ℤ) (-1) (v ᵥ* A) = 0
Tactic: rw [Matrix.smul_vecMul, h_vA, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ HSMul.hSMul (α := ℤ) (-1) v ᵥ* A = 0
have inr₁ : HSMul.hSMul (α := ℤ) (β := n → S) (-1) 0 = 0
Tactic: rw [Matrix.smul_vecMul, h_vA, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ HSMul.hSMul (α := ℤ) (-1) v ᵥ* A = 0
have inr₂ : Eq (α := n → S) 0 0
Tactic: rw [Matrix.smul_vecMul, h_vA, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ 0 < Finset.sup' Finset.univ ⋯ (HSMul.hSMul (α := ℤ) (-1) v)
have inr : ∀ (i : n) (hi : v i ≠ 0 i), 0 < Finset.sup' Finset.univ sorry (HSMul.hSMul (α := ℤ) (-1) v)
Tactic: obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ 0 < Finset.sup' Finset.univ ⋯ (HSMul.hSMul (α := ℤ) (-1) v)
have inr : ∀ (h_sup : ¬∃ (b : n), 0 < v b), ∃ (b : n), 0 < HSMul.hSMul (α := ℤ) (-1) v b
Tactic: simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢
Cleared hypotheses: h_sup
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (hypothesis)
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
⊢ ∃ (b : n), 0 < HSMul.hSMul (α := ℤ) (-1) v b
have h_sup₁ : ∀ (x : n), v x ≤ 0
Tactic: simp_rw [not_exists, not_lt] at h_sup
Cleared hypotheses: h_sup
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
have inr : 0 < HSMul.hSMul (α := ℤ) (-1) v i
Tactic: refine ⟨i, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ 0 < HSMul.hSMul (α := ℤ) (-1) v i
have inr : v i < 0
Tactic: rw [Pi.smul_apply, neg_smul, one_smul, Left.neg_pos_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
have obtain : ∀ (j₀ : n) (h_j₀ : Finset.sup' Finset.univ sorry v = v j₀), ∃ (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
have refine : LE.le.{u_2} (α := S) (∑ i : n, A i j₀) 0
Tactic: refine ⟨j₀, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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₀
⊢ LE.le.{u_2} (α := S) (∑ i : n, A i j₀) 0
have rw : LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) 0
Tactic: rw [← mul_le_mul_iff_right₀ (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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₀
⊢ LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) 0
have rw : LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) (∑ i : n, v i * A i j₀)
Tactic: rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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₀
⊢ LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) (∑ i : n, v i * A i j₀)
have refine : ∀ (i : n) (hi : Membership.mem (γ := Finset n) Finset.univ i), v j₀ * A i j₀ ≤ v i * A i j₀
Tactic: refine Finset.sum_le_sum (fun i hi => ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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₀
i : n
hi : Membership.mem (γ := Finset n) Finset.univ i
⊢ v j₀ * A i j₀ ≤ v i * A i j₀
have pos : ∀ (h : i = j₀), v j₀ * A i j₀ ≤ v i * A i j₀
Tactic: by_cases h : i = j₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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₀
i : n
hi : Membership.mem (γ := Finset n) Finset.univ i
pos : ∀ (h : i = j₀), v j₀ * A i j₀ ≤ v i * A i j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀
have neg : ∀ (h : ¬i = j₀), v j₀ * A i j₀ ≤ v i * A i j₀
Tactic: by_cases h : i = j₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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_1 : 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₀
i : n
hi : Membership.mem (γ := Finset n) Finset.univ i
h : i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀
have pos : v j₀ * A j₀ j₀ ≤ v j₀ * A j₀ j₀
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ A.det ≠ 0
have rw : Aᵀ.det ≠ 0
Tactic: rw [← Matrix.det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ Aᵀ.det ≠ 0
have refine_1 : Pairwise fun (i j : n) ↦ Aᵀ i j < 0
Tactic: refine det_ne_zero_of_sum_col_pos ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
refine_1 : Pairwise fun (i j : n) ↦ Aᵀ i j < 0
⊢ Aᵀ.det ≠ 0
have refine_2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, Aᵀ i j)
Tactic: refine det_ne_zero_of_sum_col_pos ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ Pairwise fun (i j : n) ↦ Aᵀ i j < 0
have refine_1 : Pairwise fun (i j : n) ↦ A j i < 0
Tactic: simp_rw [Matrix.transpose_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : AddCommMonoidWithOne R
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) 1) (↑(Fintype.card n) : R)
have simp_rw : Eq.{u_6 + 1} (α := R) (∑ i : n, diag 1 i) (↑(Fintype.card n) : R)
Tactic: simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : AddCommMonoidWithOne R
simp_rw : Eq.{u_6 + 1} (α := R) (∑ i : n, diag 1 i) (↑(Fintype.card n) : R)
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) 1) (↑(Fintype.card n) : R)
have simp_rw₁ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1 x) (↑(Fintype.card n) : R)
Tactic: simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : AddCommMonoidWithOne R
simp_rw : Eq.{u_6 + 1} (α := R) (∑ i : n, diag 1 i) (↑(Fintype.card n) : R)
simp_rw₁ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1 x) (↑(Fintype.card n) : R)
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) 1) (↑(Fintype.card n) : R)
have simp_rw₂ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1) (↑(Fintype.card n) : R)
Tactic: simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : AddCommMonoidWithOne R
simp_rw : Eq.{u_6 + 1} (α := R) (∑ i : n, diag 1 i) (↑(Fintype.card n) : R)
simp_rw₁ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1 x) (↑(Fintype.card n) : R)
simp_rw₂ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1) (↑(Fintype.card n) : R)
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) 1) (↑(Fintype.card n) : R)
have simp_rw₃ : HSMul.hSMul (β := R) (Finset.card.{u_3} (α := n) Finset.univ) 1 = (↑(Fintype.card n) : R)
Tactic: simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : AddCommMonoidWithOne R
simp_rw : Eq.{u_6 + 1} (α := R) (∑ i : n, diag 1 i) (↑(Fintype.card n) : R)
simp_rw₁ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1 x) (↑(Fintype.card n) : R)
simp_rw₂ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1) (↑(Fintype.card n) : R)
simp_rw₃ : HSMul.hSMul (β := R) (Finset.card.{u_3} (α := n) Finset.univ) 1 = (↑(Fintype.card n) : R)
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) 1) (↑(Fintype.card n) : R)
have simp_rw₄ : Eq.{u_6 + 1} (α := R) (↑(Finset.card.{u_3} (α := n) Finset.univ) : R) (↑(Fintype.card n) : R)
Tactic: simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid R
inst_3 : CommMagma R
A : Matrix m n R
B : Matrix n m R
⊢ (A * B).trace = (B * A).trace
have rw : (A * B)ᵀ.trace = (B * A).trace
Tactic: rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid R
inst_3 : CommMagma R
A : Matrix m n R
B : Matrix n m R
rw : (A * B)ᵀ.trace = (B * A).trace
⊢ (A * B).trace = (B * A).trace
have rw₁ : (A * B)ᵀ.trace = (Bᵀ * Aᵀ).trace
Tactic: rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid R
inst_3 : CommMagma R
A : Matrix m n R
B : Matrix n m R
rw : (A * B)ᵀ.trace = (B * A).trace
rw₁ : (A * B)ᵀ.trace = (Bᵀ * Aᵀ).trace
⊢ (A * B).trace = (B * A).trace
have rw₂ : (Bᵀ * Aᵀ).trace = (Bᵀ * Aᵀ).trace
Tactic: rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Trace (goal)
Goal:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Fintype p
inst_3 : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * B * C).trace = (C * A * B).trace
have rw : (C * (A * B)).trace = (C * A * B).trace
Tactic: rw [trace_mul_comm, Matrix.mul_assoc]