awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
rw :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₁ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₂ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₃ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v i)
rw₄ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
rw₅ : vecMulVec u v = (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • v)
⊢ vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)
have rw₆ : vecMulVec u v = (((vecMulVec u v).updateRow j (u j • v)).updateRow i v).updateRow i (u i • v)
Tactic: rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
rw :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₁ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₂ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₃ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v i)
rw₄ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
rw₅ : vecMulVec u v = (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • v)
rw₆ : vecMulVec u v = (((vecMulVec u v).updateRow j (u j • v)).updateRow i v).updateRow i (u i • v)
⊢ vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)
have rw₇ : vecMulVec u v = ((vecMulVec u v).updateRow j (u j • v)).updateRow i (u i • v)
Tactic: rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
rw :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₁ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₂ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₃ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v i)
rw₄ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
rw₅ : vecMulVec u v = (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • v)
rw₆ : vecMulVec u v = (((vecMulVec u v).updateRow j (u j • v)).updateRow i v).updateRow i (u i • v)
rw₇ : vecMulVec u v = ((vecMulVec u v).updateRow j (u j • v)).updateRow i (u i • v)
⊢ vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)
have rw₈ : vecMulVec u v = (vecMulVec (update (β := fun (a : n) ↦ R) u j (u j)) v).updateRow i (u i • v)
Tactic: rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
rw :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₁ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₂ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₃ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v i)
rw₄ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
rw₅ : vecMulVec u v = (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • v)
rw₆ : vecMulVec u v = (((vecMulVec u v).updateRow j (u j • v)).updateRow i v).updateRow i (u i • v)
rw₇ : vecMulVec u v = ((vecMulVec u v).updateRow j (u j • v)).updateRow i (u i • v)
rw₈ : vecMulVec u v = (vecMulVec (update (β := fun (a : n) ↦ R) u j (u j)) v).updateRow i (u i • v)
⊢ vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)
have rw₉ : vecMulVec u v = (vecMulVec u v).updateRow i (u i • v)
Tactic: rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
rw :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₁ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₂ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₃ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v i)
rw₄ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
rw₅ : vecMulVec u v = (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • v)
rw₆ : vecMulVec u v = (((vecMulVec u v).updateRow j (u j • v)).updateRow i v).updateRow i (u i • v)
rw₇ : vecMulVec u v = ((vecMulVec u v).updateRow j (u j • v)).updateRow i (u i • v)
rw₈ : vecMulVec u v = (vecMulVec (update (β := fun (a : n) ↦ R) u j (u j)) v).updateRow i (u i • v)
rw₉ : vecMulVec u v = (vecMulVec u v).updateRow i (u i • v)
⊢ vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)
have rw₁₀ : vecMulVec u v = vecMulVec (update (β := fun (a : n) ↦ R) u i (u i)) v
Tactic: rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
rw :
  vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₁ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j
          (u j •
            (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
              (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)).updateRow
      i (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₂ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)
rw₃ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • ((vecMulVec u v).updateRow i v).updateRow j v j)).updateRow i
      (u i • (vecMulVec u v).updateRow i v i)
rw₄ :
  vecMulVec u v =
    (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
rw₅ : vecMulVec u v = (((vecMulVec u v).updateRow i v).updateRow j (u j • v)).updateRow i (u i • v)
rw₆ : vecMulVec u v = (((vecMulVec u v).updateRow j (u j • v)).updateRow i v).updateRow i (u i • v)
rw₇ : vecMulVec u v = ((vecMulVec u v).updateRow j (u j • v)).updateRow i (u i • v)
rw₈ : vecMulVec u v = (vecMulVec (update (β := fun (a : n) ↦ R) u j (u j)) v).updateRow i (u i • v)
rw₉ : vecMulVec u v = (vecMulVec u v).updateRow i (u i • v)
rw₁₀ : vecMulVec u v = vecMulVec (update (β := fun (a : n) ↦ R) u i (u i)) v
⊢ vecMulVec u v =
    ((((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i)).updateRow
      j
      (u j •
        (((vecMulVec u v).updateRow i v).updateRow j v).updateRow i
          (u i • ((vecMulVec u v).updateRow i v).updateRow j v i) j)
have rw₁₁ : vecMulVec u v = vecMulVec u v
Tactic: rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
⊢ (vecMulVec u v).det = 0
have this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
Tactic: have : vecMulVec u v =
      (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j) := by
    unfold uv'
    rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
⊢ (vecMulVec u v).det = 0
have rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
⊢ (vecMulVec u v).det = 0
have rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
⊢ (vecMulVec u v).det = 0
have rw₂ : u j * (uv'.updateRow i (u i • uv' i)).det = 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
rw₂ : u j * (uv'.updateRow i (u i • uv' i)).det = 0
⊢ (vecMulVec u v).det = 0
have rw₃ : u j * (u i * (uv'.updateRow i (uv' i)).det) = 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
rw₂ : u j * (uv'.updateRow i (u i • uv' i)).det = 0
rw₃ : u j * (u i * (uv'.updateRow i (uv' i)).det) = 0
⊢ (vecMulVec u v).det = 0
have rw₄ : u j * (u i * uv'.det) = 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
rw₂ : u j * (uv'.updateRow i (u i • uv' i)).det = 0
rw₃ : u j * (u i * (uv'.updateRow i (uv' i)).det) = 0
rw₄ : u j * (u i * uv'.det) = 0
⊢ (vecMulVec u v).det = 0
have rw₅ : u j * (u i * 0) = 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
rw₂ : u j * (uv'.updateRow i (u i • uv' i)).det = 0
rw₃ : u j * (u i * (uv'.updateRow i (uv' i)).det) = 0
rw₄ : u j * (u i * uv'.det) = 0
rw₅ : u j * (u i * 0) = 0
⊢ (vecMulVec u v).det = 0
have rw₆ : u j * 0 = 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
inst_3 : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
rw : ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
rw₁ : u j * ((uv'.updateRow i (u i • uv' i)).updateRow j (uv'.updateRow i (u i • uv' i) j)).det = 0
rw₂ : u j * (uv'.updateRow i (u i • uv' i)).det = 0
rw₃ : u j * (u i * (uv'.updateRow i (uv' i)).det) = 0
rw₄ : u j * (u i * uv'.det) = 0
rw₅ : u j * (u i * 0) = 0
rw₆ : u j * 0 = 0
⊢ (vecMulVec u v).det = 0
have rw₇ : Eq.{v + 1} (α := R) 0 0
Tactic: rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
⊢ A.det = B.det
have this : ∀ (i : n), c i = 0
Tactic: have : ∀ i, c i = 0 := by grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
⊢ A.det = B.det
have empty : A = B
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
⊢ A = B
have empty : ∀ (i j : n), A i j = B i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
i j : n
⊢ A i j = B i j
have empty : B i j + c i * B k j = B i j
Tactic: rw [A_eq, this, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
i j : n
empty : B i j + c i * B k j = B i j
⊢ A i j = B i j
have empty₁ : B i j + 0 * B k j = B i j
Tactic: rw [A_eq, this, zero_mul, add_zero]