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
M : Matrix n n R
j : n
s : R
u : n → R
⊢ (M.updateCol j (s • u)).det = s * (M.updateCol j u).det
have rw : s * (Mᵀ.updateRow j u).det = s * (M.updateCol j u).det
Tactic: rw [← det_transpose, ← updateRow_transpose, det_updateRow_smul]
-- 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
M : Matrix n n R
j : n
s : R
u : n → R
⊢ ((s • M).updateCol j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
have rw : s ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det
Tactic: rw [← det_transpose, ← updateRow_transpose, transpose_smul, det_updateRow_smul_left]
-- 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
M : Matrix n n R
j : n
c : n → R
a : R
hj : j ∉ ∅
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
have empty : (M.updateRow j (a • M j + 0)).det = a • M.det
Tactic: rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_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
M : Matrix n n R
j : n
c : n → R
a : R
hj : j ∉ ∅
empty : (M.updateRow j (a • M j + 0)).det = a • M.det
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
have empty₁ : (M.updateRow j (a • M j)).det = a • M.det
Tactic: rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_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
M : Matrix n n R
j : n
c : n → R
a : R
hj : j ∉ ∅
empty : (M.updateRow j (a • M j + 0)).det = a • M.det
empty₁ : (M.updateRow j (a • M j)).det = a • M.det
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
have empty₂ : (M.updateRow j (a • M j)).det = a * M.det
Tactic: rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_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
M : Matrix n n R
j : n
c : n → R
a : R
hj : j ∉ ∅
empty : (M.updateRow j (a • M j + 0)).det = a • M.det
empty₁ : (M.updateRow j (a • M j)).det = a • M.det
empty₂ : (M.updateRow j (a • M j)).det = a * M.det
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
have empty₃ : a * (M.updateRow j (M j)).det = a * M.det
Tactic: rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_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
M : Matrix n n R
j : n
c : n → R
a : R
hj : j ∉ ∅
empty : (M.updateRow j (a • M j + 0)).det = a • M.det
empty₁ : (M.updateRow j (a • M j)).det = a • M.det
empty₂ : (M.updateRow j (a • M j)).det = a * M.det
empty₃ : a * (M.updateRow j (M j)).det = a * M.det
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
have empty₄ : a * M.det = a * M.det
Tactic: rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_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
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s : Finset n
hk : k ∉ s
h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
hj : j ∉ insert k s
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s, c k • M k)).det = a • M.det
have h : k ≠ j
Tactic: have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_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
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s : Finset n
hk : k ∉ s
h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
hj : j ∉ insert k s
h : k ≠ j
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s, c k • M k)).det = a • M.det
have insert : j ∉ s
Tactic: rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
        det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]
-- 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
M : Matrix n n R
j : n
s : Finset n
hj : j ∉ s
c : n → R
a : R
⊢ (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
have empty : ∀ (hj : j ∉ ∅), (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
Tactic: induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]
  | insert k _ hk h_ind =>
      have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)
      rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
        det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]
      exact fun h ↦ hj (Finset.mem_insert_of_mem h)
Cleared hypotheses: s, hj
-- 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
M : Matrix n n R
j : n
s : Finset n
hj : j ∉ s
c : n → R
a : R
empty : ∀ (hj : j ∉ ∅), (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det
⊢ (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det
have insert : ∀ (k : n) (s : Finset n) (hk : k ∉ s)
  (h_ind : ∀ (hj : j ∉ s), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det) (hj : j ∉ insert k s),
  (M.updateRow j (a • M j + ∑ k ∈ insert k s, c k • M k)).det = a • M.det
Tactic: induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]
  | insert k _ hk h_ind =>
      have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)
      rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
        det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]
      exact fun h ↦ hj (Finset.mem_insert_of_mem h)
Cleared hypotheses: s, hj
-- 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 : Matrix n n R
j : n
c : n → R
⊢ (A.updateRow j (∑ k : n, c k • A k)).det = c j • A.det
have h : ∑ k : n, c k • A k = c j • A j + ∑ k ∈ erase univ j, c k • A k
Tactic: convert! det_updateRow_sum_aux A (Finset.univ.erase j) (Finset.univ.notMem_erase j) c (c 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 : Matrix n n R
j : n
c : n → R
⊢ ∑ k : n, c k • A k = c j • A j + ∑ k ∈ erase univ j, c k • A k
have h : c j • A j + ∑ x ∈ erase univ j, c x • A x = c j • A j + ∑ k ∈ erase univ j, c k • A k
Tactic: rw [← Finset.univ.add_sum_erase _ (Finset.mem_univ 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 : Matrix n n R
j : n
c : n → R
⊢ (A.updateCol j fun (k : n) ↦ ∑ i : n, c i • A k i).det = c j • A.det
have rw : (Aᵀ.updateRow j fun (k : n) ↦ ∑ i : n, c i • A k i).det = c j • Aᵀ.det
Tactic: rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]
-- 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 : Matrix n n R
j : n
c : n → R
⊢ (Aᵀ.updateRow j fun (k : n) ↦ ∑ i : n, c i • A k i).det = c j • Aᵀ.det
have h : ∀ (x : n), Eq.{v + 1} (α := R) (∑ i : n, c i • A x i) ((∑ k : n, c k • Aᵀ k) x)
Tactic: convert! det_updateRow_sum A.transpose j c
-- 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 C : Matrix n n R
hC : C.det = 1
hA : A = B * C
⊢ B.det * C.det = B.det
have rw : B.det * 1 = B.det
Tactic: rw [hC, mul_one]
-- 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 C : Matrix n n R
hC : C.det = 1
hA : A = B * C
rw : B.det * 1 = B.det
⊢ B.det * C.det = B.det
have rw₁ : B.det = B.det
Tactic: rw [hC, mul_one]
-- 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 C : Matrix n n R
hC : C.det = 1
hA : A = C * B
⊢ C.det * B.det = B.det
have rw : 1 * B.det = B.det
Tactic: rw [hC, one_mul]
-- 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 C : Matrix n n R
hC : C.det = 1
hA : A = C * B
rw : 1 * B.det = B.det
⊢ C.det * B.det = B.det
have rw₁ : B.det = B.det
Tactic: rw [hC, one_mul]
-- 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 : Matrix n n R
i j : n
hij : i ≠ j
⊢ (A.updateCol i fun (k : n) ↦ A k i + A k j).det = A.det
have rw : (Aᵀ.updateRow i fun (k : n) ↦ A k i + A k j).det = Aᵀ.det
Tactic: rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]
-- 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 : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (A.updateCol i fun (k : n) ↦ A k i + c • A k j).det = A.det
have rw : (Aᵀ.updateRow i fun (k : n) ↦ A k i + c • A k j).det = Aᵀ.det
Tactic: rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
inst_3 : IsDomain R
A : Matrix m m R
hA : A.det ≠ 0
⊢ LinearIndependent R (M := m → R) fun (i : m) ↦ A i
have contrapose : ∀ (hA : ¬LinearIndependent R (M := m → R) fun (i : m) ↦ A i), A.det = 0
Tactic: contrapose hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
inst_3 : IsDomain R
A : Matrix m m R
hA : ¬LinearIndependent R (M := m → R) fun (i : m) ↦ Aᵀ i
⊢ A.det = 0
have contrapose! : ∀ (hA : A.det ≠ 0), LinearIndependent R (M := m → R) fun (i : m) ↦ Aᵀ i
Tactic: contrapose! hA
Cleared hypotheses: hA
-- 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
⊢ (vecMulVec u v).det = 0
have obtain : ∀ (i j : n) (hij : i ≠ j), (vecMulVec u v).det = 0
Tactic: obtain ⟨i, j, hij⟩ := exists_pair_ne n
-- 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
⊢ uv'.det = 0
have refine : uv' i = uv' j
Tactic: refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij
-- 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
⊢ (vecMulVec u v).det = 0
have huv' : uv'.det = 0
Tactic: have huv' : uv'.det = 0 := by
    refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij
    simp [uv', hij]
-- 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
⊢ 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 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)
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)
⊢ 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 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)
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)
⊢ 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 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)
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)
⊢ 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 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)
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)
⊢ 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 v).updateRow j (u j • v)).updateRow i (u i • (vecMulVec u v).updateRow i v i)
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)
⊢ 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 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]