-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq l
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
i : l
r : m → α
j : n
c : m → α
rw : (0 * updateCol 0 j c).updateRow i (r ᵥ* updateCol 0 j c) = single i j (r ⬝ᵥ c)
rw₁ :
  (0 * updateCol 0 j c).updateRow i (Function.update (β := fun (a : n) ↦ α) (r ᵥ* 0) j (r ⬝ᵥ c)) = single i j (r ⬝ᵥ c)
rw₂ :
  ((HMul.hMul (α := Matrix l m α) 0 0).updateCol j (0 *ᵥ c)).updateRow i
      (Function.update (β := fun (a : n) ↦ α) (r ᵥ* 0) j (r ⬝ᵥ c)) =
    single i j (r ⬝ᵥ c)
rw₃ :
  ((HMul.hMul (α := Matrix l m α) 0 0).updateCol j (0 *ᵥ c)).updateRow i
      (Function.update (β := fun (a : n) ↦ α) (r ᵥ* 0) j (r ⬝ᵥ c)) =
    (of : (a : l → n → α) → Matrix l n α)
      (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c)))
rw₄ :
  updateRow (updateCol 0 j (0 *ᵥ c)) i (Function.update (β := fun (a : n) ↦ α) (r ᵥ* 0) j (r ⬝ᵥ c)) =
    (of : (a : l → n → α) → Matrix l n α)
      (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c)))
rw₅ :
  updateRow (updateCol 0 j (0 *ᵥ c)) i (Function.update (β := fun (a : n) ↦ α) 0 j (r ⬝ᵥ c)) =
    (of : (a : l → n → α) → Matrix l n α)
      (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c)))
rw₆ :
  Eq (α := Matrix l n α) (updateRow (updateCol 0 j 0) i (Function.update (β := fun (a : n) ↦ α) 0 j (r ⬝ᵥ c)))
    ((of : (a : l → n → α) → Matrix l n α)
      (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c))))
rw₇ :
  Eq (α := Matrix l n α) (updateRow 0 i (Function.update (β := fun (a : n) ↦ α) 0 j (r ⬝ᵥ c)))
    ((of : (a : l → n → α) → Matrix l n α)
      (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c))))
rw₈ :
  Eq (α := Matrix l n α)
    ((of : (a : l → n → α) → Matrix l n α)
        (Function.update (β := fun (a : l) ↦ n → α) 0 i (Function.update (β := fun (a : n) ↦ α) 0 j (r ⬝ᵥ c))) :
      Matrix l n α)
    ((of : (a : l → n → α) → Matrix l n α)
        (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c))) :
      Matrix l n α)
rw₉ :
  Eq (α := Matrix l n α)
    ((of : (a : l → n → α) → Matrix l n α)
        (Pi.single (M := fun (a : l) ↦ n → α) i (Function.update (β := fun (a : n) ↦ α) 0 j (r ⬝ᵥ c))) :
      Matrix l n α)
    ((of : (a : l → n → α) → Matrix l n α)
        (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c))) :
      Matrix l n α)
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have rw₁₀ : Eq (α := Matrix l n α)
  ((of : (a : l → n → α) → Matrix l n α)
      (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c))) :
    Matrix l n α)
  ((of : (a : l → n → α) → Matrix l n α)
      (Pi.single (M := fun (a : l) ↦ n → α) i (Pi.single (M := fun (a : n) ↦ α) j (r ⬝ᵥ c))) :
    Matrix l n α)
Tactic: rw [updateRow_mul, vecMul_updateCol, mul_updateCol, single_eq_of_single_single, Matrix.zero_mul,
    vecMul_zero, zero_mulVec, updateCol_zero_zero, updateRow, ← Pi.single, ← Pi.single]