awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 m
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
i : l
j : m
r : α
B : Matrix m n α
⊢ single i j r * B = updateRow 0 i (r • B.row j)
have rw : HMul.hMul (α := Matrix l m α) (updateRow 0 i (Pi.single (M := fun (a : m) ↦ α) j r)) B = updateRow 0 i (r • B.row j)
Tactic: rw [single_eq_updateRow_zero, updateRow_mul, Matrix.zero_mul, single_vecMul]
-- 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 m
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
i : l
j : m
r : α
B : Matrix m n α
rw :
  HMul.hMul (α := Matrix l m α) (updateRow 0 i (Pi.single (M := fun (a : m) ↦ α) j r)) B = updateRow 0 i (r • B.row j)
⊢ single i j r * B = updateRow 0 i (r • B.row j)
have rw₁ : (0 * B).updateRow i (Pi.single (M := fun (a : m) ↦ α) j r ᵥ* B) = updateRow 0 i (r • B.row j)
Tactic: rw [single_eq_updateRow_zero, updateRow_mul, Matrix.zero_mul, single_vecMul]
-- 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 m
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
i : l
j : m
r : α
B : Matrix m n α
rw :
  HMul.hMul (α := Matrix l m α) (updateRow 0 i (Pi.single (M := fun (a : m) ↦ α) j r)) B = updateRow 0 i (r • B.row j)
rw₁ : (0 * B).updateRow i (Pi.single (M := fun (a : m) ↦ α) j r ᵥ* B) = updateRow 0 i (r • B.row j)
⊢ single i j r * B = updateRow 0 i (r • B.row j)
have rw₂ : updateRow 0 i (Pi.single (M := fun (a : m) ↦ α) j r ᵥ* B) = updateRow 0 i (r • B.row j)
Tactic: rw [single_eq_updateRow_zero, updateRow_mul, Matrix.zero_mul, single_vecMul]
-- 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 m
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
i : l
j : m
r : α
B : Matrix m n α
rw :
  HMul.hMul (α := Matrix l m α) (updateRow 0 i (Pi.single (M := fun (a : m) ↦ α) j r)) B = updateRow 0 i (r • B.row j)
rw₁ : (0 * B).updateRow i (Pi.single (M := fun (a : m) ↦ α) j r ᵥ* B) = updateRow 0 i (r • B.row j)
rw₂ : updateRow 0 i (Pi.single (M := fun (a : m) ↦ α) j r ᵥ* B) = updateRow 0 i (r • B.row j)
⊢ single i j r * B = updateRow 0 i (r • B.row j)
have rw₃ : updateRow 0 i (r • B.row j) = updateRow 0 i (r • B.row j)
Tactic: rw [single_eq_updateRow_zero, updateRow_mul, Matrix.zero_mul, single_vecMul]
-- 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 → α
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have rw : (0 * updateCol 0 j c).updateRow i (r ᵥ* updateCol 0 j c) = single i j (r ⬝ᵥ c)
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]
-- 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)
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have rw₁ : (0 * updateCol 0 j c).updateRow i (Function.update (β := fun (a : n) ↦ α) (r ᵥ* 0) j (r ⬝ᵥ c)) = single i j (r ⬝ᵥ c)
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]
-- 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)
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have 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)
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]
-- 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)
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have 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)))
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]
-- 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)))
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have 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)))
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]
-- 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)))
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have 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)))
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]
-- 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)))
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have 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))))
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]
-- 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))))
⊢ updateRow 0 i r * updateCol 0 j c = single i j (r ⬝ᵥ c)
have 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))))
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]
-- 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))))
⊢ 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 α)
      (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 α)
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]
-- 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 α)
⊢ 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 (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 α)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst_7 : Invertible A
inst_8 : Invertible D
⊢ fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
        (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
        0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
      fromBlocks A B 0 D =
    1
have simp_rw : fromBlocks
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A +
      -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
        0)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
      -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
        D)
    (0 * A + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * 0)
    (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
  1
Tactic: simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, add_neg_cancel,
      fromBlocks_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SchurComplement (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst : Fintype l
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst_7 : Invertible A
inst_8 : Invertible D
simp_rw :
  fromBlocks
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          0)
      (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
        -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
              @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
          D)
      (0 * A + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * 0)
      (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
    1
⊢ fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _)
        (-(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _))
        0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
      fromBlocks A B 0 D =
    1
have simp_rw₁ : fromBlocks (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * A + 0)
    (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B +
      -(@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B *
            @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) *
        D)
    (0 * A + 0) (0 * B + @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * D) =
  1
Tactic: simp_rw [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, zero_add, add_zero,
      Matrix.neg_mul, invOf_mul_self, Matrix.invOf_mul_cancel_right, add_neg_cancel,
      fromBlocks_one]