awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
rw :
  (diagonal v)ᵀ.updateRow i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
rw₁ :
  ((diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x))ᵀ =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
rw₂ :
  (diagonal (Function.update (β := fun (a : n) ↦ α) v i x))ᵀ = diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
rw₃ rw₄ :
  diagonal (Function.update (β := fun (a : n) ↦ α) v i x) = diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
⊢ (diagonal v).updateRow i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)

Tactic:
rw [← diagonal_transpose, updateRow_transpose, diagonal_updateCol_single, diagonal_transpose]

Premises used: Matrix.updateRow_transpose, Matrix.diagonal_updateCol_single, Matrix.diagonal_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
A : Matrix m n α
i : m
x y : n → α
⊢ (A.updateRow i x).updateRow i y = A.updateRow i y

Tactic:
Function.update_idem _ _ _

Premises used: Function.update, Matrix, dite, Function.update_idem, Matrix.updateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
A : Matrix m n α
i i' : m
h : i ≠ i'
x y : n → α
⊢ (A.updateRow i x).updateRow i' y = (A.updateRow i' y).updateRow i x

Tactic:
Function.update_comm h _ _ _

Premises used: Function.update, Matrix, Function.update_comm, dite, Matrix.updateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
A : Matrix m n α
j : n
x y : m → α
⊢ (A.updateCol j x).updateCol j y = A.updateCol j y

Tactic:
simpa only [updateRow_transpose] using congr_arg transpose <| updateRow_idem Aᵀ j x y

Premises used: Matrix.updateRow_transpose, Matrix.updateRow_idem, congr_arg, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
A : Matrix m n α
j j' : n
h : j ≠ j'
x y : m → α
⊢ (A.updateCol j x).updateCol j' y = (A.updateCol j' y).updateCol j x

Tactic:
simpa only [updateRow_transpose] using congr_arg transpose <| updateRow_comm Aᵀ h x y

Premises used: Matrix.updateRow_transpose, Matrix.updateRow_comm, congr_arg, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq l
inst_1 : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
a :
  ∀ (i' : l) (j : o),
    updateRow (A.submatrix (⇑e : (a : l) → m) (⇑f : (a : o) → n)) i r i' j =
      (A.updateRow ((e : (a : l) → m) i) fun (j : n) ↦ r ((f.symm : (a : n) → o) j)).submatrix (⇑e : (a : l) → m)
        (⇑f : (a : o) → n) i' j
⊢ updateRow (A.submatrix (⇑e : (a : l) → m) (⇑f : (a : o) → n)) i r =
    (A.updateRow ((e : (a : l) → m) i) fun (j : n) ↦ r ((f.symm : (a : n) → o) j)).submatrix (⇑e : (a : l) → m)
      (⇑f : (a : o) → n)

Tactic:
ext i' j
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq l
inst_1 : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ updateRow (A.submatrix (⇑e : (a : l) → m) (⇑f : (a : o) → n)) i r i' j =
    (A.updateRow ((e : (a : l) → m) i) fun (j : n) ↦ r ((f.symm : (a : n) → o) j)).submatrix (⇑e : (a : l) → m)
      (⇑f : (a : o) → n) i' j

Tactic:
simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Matrix.submatrix_apply, Equiv.apply_eq_iff_eq, Matrix.updateRow_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq l
inst_1 : DecidableEq m
A : Matrix m n α
i : m
r : n → α
e : l ≃ m
f : o ≃ n
⊢ Eq (α := Matrix l o α) ((A.updateRow i r).submatrix (⇑e : (a : l) → m) (⇑f : (a : o) → n))
    ((A.updateRow ((e : (a : l) → m) ((e.symm : (a : m) → l) i : l)) fun (j : n) ↦
          r ((f : (a : o) → n) ((f.symm : (a : n) → o) j : o))).submatrix
      (⇑e : (a : l) → m) (⇑f : (a : o) → n))

Tactic:
simp_rw [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq o
inst_1 : DecidableEq n
A : Matrix m n α
j : o
c : l → α
e : l ≃ m
f : o ≃ n
⊢ updateCol (A.submatrix (⇑e : (a : l) → m) (⇑f : (a : o) → n)) j c =
    (A.updateCol ((f : (a : o) → n) j) fun (i : m) ↦ c ((e.symm : (a : m) → l) i)).submatrix (⇑e : (a : l) → m)
      (⇑f : (a : o) → n)

Tactic:
simpa only [← transpose_submatrix, updateRow_transpose] using
    congr_arg transpose (updateRow_submatrix_equiv Aᵀ j c f e)

Premises used: Matrix.transpose_submatrix, Matrix.updateRow_submatrix_equiv, Matrix.updateRow_transpose, congr_arg, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq o
inst_1 : DecidableEq n
A : Matrix m n α
j : n
c : m → α
e : l ≃ m
f : o ≃ n
⊢ Eq (α := Matrix l o α) ((A.updateCol j c).submatrix (⇑e : (a : l) → m) (⇑f : (a : o) → n))
    ((A.updateCol ((f : (a : o) → n) ((f.symm : (a : n) → o) j : o)) fun (i : m) ↦
          c ((e : (a : l) → m) ((e.symm : (a : m) → l) i : l))).submatrix
      (⇑e : (a : l) → m) (⇑f : (a : o) → n))

Tactic:
simp_rw [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq l
inst_1 : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : m ≃ l
f : n ≃ o
⊢ updateRow ((reindex e f : (a : Matrix m n α) → Matrix l o α) A) i r =
    (reindex e f : (a : Matrix m n α) → Matrix l o α)
      (A.updateRow ((e.symm : (a : l) → m) i) fun (j : n) ↦ r ((f : (a : n) → o) j))

Tactic:
updateRow_submatrix_equiv _ _ _ _ _

Premises used: Matrix.submatrix, Function.update, Matrix.updateRow_submatrix_equiv, dite, Matrix.updateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq l
inst_1 : DecidableEq m
A : Matrix m n α
i : m
r : n → α
e : m ≃ l
f : n ≃ o
⊢ Eq (α := Matrix l o α) ((reindex e f : (a : Matrix m n α) → Matrix l o α) (A.updateRow i r) : Matrix l o α)
    (updateRow ((reindex e f : (a : Matrix m n α) → Matrix l o α) A) ((e : (a : m) → l) i) fun (i : o) ↦
        r ((f.symm : (a : o) → n) i) :
      Matrix l o α)

Tactic:
submatrix_updateRow_equiv _ _ _ _ _

Premises used: Matrix.submatrix, Function.update, Matrix.submatrix_updateRow_equiv, dite, Matrix.updateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq o
inst_1 : DecidableEq n
A : Matrix m n α
j : o
c : l → α
e : m ≃ l
f : n ≃ o
⊢ updateCol ((reindex e f : (a : Matrix m n α) → Matrix l o α) A) j c =
    (reindex e f : (a : Matrix m n α) → Matrix l o α)
      (A.updateCol ((f.symm : (a : o) → n) j) fun (i : m) ↦ c ((e : (a : m) → l) i))

Tactic:
updateCol_submatrix_equiv _ _ _ _ _

Premises used: Matrix.submatrix, Function.update, dite, Matrix.updateCol_submatrix_equiv, Matrix.updateCol
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst : DecidableEq o
inst_1 : DecidableEq n
A : Matrix m n α
j : n
c : m → α
e : m ≃ l
f : n ≃ o
⊢ Eq (α := Matrix l o α) ((reindex e f : (a : Matrix m n α) → Matrix l o α) (A.updateCol j c) : Matrix l o α)
    (updateCol ((reindex e f : (a : Matrix m n α) → Matrix l o α) A) ((f : (a : n) → o) j) fun (i : l) ↦
        c ((e.symm : (a : l) → m) i) :
      Matrix l o α)

Tactic:
submatrix_updateCol_equiv _ _ _ _ _

Premises used: Matrix.submatrix, Function.update, Matrix.submatrix_updateCol_equiv, dite, Matrix.updateCol
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
r : α
⊢ single i j r = updateRow 0 i (Pi.single (M := fun (a : n) ↦ α) j r)

Tactic:
single_eq_of_single_single _ _ _

Premises used: Pi.single, Matrix.single_eq_of_single_single, Matrix.updateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero α
i : m
j : n
r : α
⊢ single i j r = updateCol 0 j (Pi.single (M := fun (a : m) ↦ α) i r)

Tactic:
simpa [← updateCol_transpose] using congr($(single_eq_updateRow_zero j i r)ᵀ)

Premises used: Matrix.single_eq_updateRow_zero, Matrix.updateCol_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
c v : m → α
h : ∀ (i' : l), (A.updateRow i c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v) i'
⊢ A.updateRow i c *ᵥ v = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v)

Tactic:
ext i'
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
c v : m → α
i' : l
h : (A.updateRow i' c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i' (c ⬝ᵥ v) i'
h₁ : ∀ (hi : i' ≠ i), (A.updateRow i c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v) i'
⊢ (A.updateRow i c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v) i'

Tactic:
obtain rfl | hi := eq_or_ne i' i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
c v : m → α
i' : l
⊢ (A.updateRow i' c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i' (c ⬝ᵥ v) i'

Tactic:
simp [mulVec]

Premises used: Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
c v : m → α
i' : l
hi : i' ≠ i
⊢ (A.updateRow i c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v) i'

Tactic:
simp [mulVec, hi]

Premises used: Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
h : ∀ (j' : n), (v ᵥ* B.updateCol j r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r) j'
⊢ v ᵥ* B.updateCol j r = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r)

Tactic:
ext j'
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
h : (v ᵥ* B.updateCol j' r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j' (v ⬝ᵥ r) j'
h₁ : ∀ (hj : j' ≠ j), (v ᵥ* B.updateCol j r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r) j'
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r) j'

Tactic:
obtain rfl | hj := eq_or_ne j' j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
r : m → α
j' : n
⊢ (v ᵥ* B.updateCol j' r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j' (v ⬝ᵥ r) j'

Tactic:
simp [vecMul]

Premises used: Matrix.vecMul
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
hj : j' ≠ j
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r) j'

Tactic:
simp [vecMul, hj]

Premises used: Matrix.vecMul
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : Mul α
u : m → α
v : n → α
i : m
a : α
a₁ :
  ∀ (i' : m) (j : n),
    vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j
⊢ vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v = (vecMulVec u v).updateRow i (a • v)

Tactic:
ext i' j
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : Mul α
u : m → α
v : n → α
i : m
a : α
i' : m
j : n
a₁ : vecMulVec (Function.update (β := fun (a : m) ↦ α) u i' a) v i' j = (vecMulVec u v).updateRow i' (a • v) i' j
a₂ :
  ∀ (hi : i' ≠ i),
    vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j
⊢ vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j

Tactic:
obtain rfl | hi := eq_or_ne i' i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : Mul α
u : m → α
v : n → α
a : α
i' : m
j : n
⊢ vecMulVec (Function.update (β := fun (a : m) ↦ α) u i' a) v i' j = (vecMulVec u v).updateRow i' (a • v) i' j

Tactic:
simp [vecMulVec_apply]

Premises used: Matrix.vecMulVec_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : Mul α
u : m → α
v : n → α
i : m
a : α
i' : m
j : n
hi : i' ≠ i
⊢ vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j

Tactic:
simp [vecMulVec_apply, hi]

Premises used: Matrix.vecMulVec_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Mul α
u : m → α
v : n → α
j : n
a : α
a₁ :
  ∀ (i : m) (j' : n),
    vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) i j' =
      (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'
⊢ vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) = (vecMulVec u v).updateCol j (MulOpposite.op a • u)

Tactic:
ext i j'
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Mul α
u : m → α
v : n → α
j : n
a : α
i : m
j' : n
a₁ :
  vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j' a) i j' =
    (vecMulVec u v).updateCol j' (MulOpposite.op a • u) i j'
a₂ :
  ∀ (hi : j' ≠ j),
    vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) i j' =
      (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'
⊢ vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) i j' =
    (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'

Tactic:
obtain rfl | hi := eq_or_ne j' j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Mul α
u : m → α
v : n → α
a : α
i : m
j' : n
⊢ vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j' a) i j' =
    (vecMulVec u v).updateCol j' (MulOpposite.op a • u) i j'

Tactic:
simp [vecMulVec_apply]

Premises used: Matrix.vecMulVec_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Mul α
u : m → α
v : n → α
j : n
a : α
i : m
j' : n
hi : j' ≠ j
⊢ vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) i j' =
    (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'

Tactic:
simp [vecMulVec_apply, hi]

Premises used: Matrix.vecMulVec_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
a : ∀ (i' : l) (j' : n), (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
⊢ A.updateRow i r * B = (A * B).updateRow i (r ᵥ* B)

Tactic:
ext i' j'
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
a : (A.updateRow i' r * B) i' j' = (A * B).updateRow i' (r ᵥ* B) i' j'
a₁ : ∀ (hi : i' ≠ i), (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'

Tactic:
obtain rfl | hi := eq_or_ne i' i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
r : m → α
B : Matrix m n α
i' : l
j' : n
⊢ (A.updateRow i' r * B) i' j' = (A * B).updateRow i' (r ᵥ* B) i' j'

Tactic:
simp [mul_apply, vecMul, dotProduct]

Premises used: dotProduct, Matrix.vecMul, Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq l
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
hi : i' ≠ i
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'

Tactic:
simp [mul_apply, hi]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
a : ∀ (i' : l) (j' : n), (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'
⊢ A * B.updateCol j c = (A * B).updateCol j (A *ᵥ c)

Tactic:
ext i' j'
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
i' : l
j' : n
a : (A * B.updateCol j' c) i' j' = (A * B).updateCol j' (A *ᵥ c) i' j'
a₁ : ∀ (hj : j' ≠ j), (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'
⊢ (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'

Tactic:
obtain rfl | hj := eq_or_ne j' j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
c : m → α
i' : l
j' : n
⊢ (A * B.updateCol j' c) i' j' = (A * B).updateCol j' (A *ᵥ c) i' j'

Tactic:
simp [mul_apply, mulVec, dotProduct]

Premises used: dotProduct, Matrix.mul_apply, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
i' : l
j' : n
hj : j' ≠ j
⊢ (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'

Tactic:
simp [mul_apply, hj]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : m
j : n
r : α
rw :
  HMul.hMul (β := Matrix m n α) A (updateCol 0 j (Pi.single (M := fun (a : m) ↦ α) i r)) = updateCol 0 j (A.col i <• r)
rw₁ : (A * 0).updateCol j (A *ᵥ Pi.single (M := fun (a : m) ↦ α) i r) = updateCol 0 j (A.col i <• r)
rw₂ : updateCol 0 j (A *ᵥ Pi.single (M := fun (a : m) ↦ α) i r) = updateCol 0 j (A.col i <• r)
rw₃ rw₄ : updateCol 0 j (A.col i <• r) = updateCol 0 j (A.col i <• r)
⊢ A * single i j r = updateCol 0 j (A.col i <• r)

Tactic:
rw [single_eq_updateCol_zero, mul_updateCol, Matrix.mul_zero, mulVec_single]

Premises used: Matrix.mul_updateCol, Matrix.mul_zero, Matrix.single_eq_updateCol_zero, Matrix.mulVec_single
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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)
rw₃ rw₄ : updateRow 0 i (r • B.row j) = updateRow 0 i (r • B.row j)
⊢ single i j r * B = updateRow 0 i (r • B.row j)

Tactic:
rw [single_eq_updateRow_zero, updateRow_mul, Matrix.zero_mul, single_vecMul]

Premises used: Matrix.single_eq_updateRow_zero, Matrix.single_vecMul, Matrix.updateRow_mul, Matrix.zero_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 α
C : Matrix l m α
D : Matrix l n α
inst_7 : Invertible A
⊢ fromBlocks A B C D =
    HMul.hMul (β := Matrix (m ⊕ n) (m ⊕ n) α)
      (HMul.hMul (α := Matrix (m ⊕ l) (m ⊕ l) α)
        (fromBlocks 1 0 (C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _) 1)
        (fromBlocks A 0 0 (D - C * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B)))
      (fromBlocks 1 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one A _ * B) 0 1)

Tactic:
simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add,
    Matrix.one_mul, Matrix.mul_one, invOf_mul_self, Matrix.mul_invOf_cancel_left,
    Matrix.mul_assoc, add_sub_cancel]

Premises used: Matrix.mul_assoc, invOf_mul_self, Matrix.mul_zero, zero_add, add_sub_cancel, Matrix.mul_invOf_cancel_left, Matrix.zero_mul, Matrix.mul_one, Matrix.fromBlocks_multiply, add_zero, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.SchurComplement
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 l m α
B : Matrix l n α
C : Matrix n m α
D : Matrix n n α
inst_7 : Invertible D
⊢ Eq (α := Matrix (n ⊕ l) (n ⊕ m) α)
    ((reindex (Equiv.sumComm l n) (Equiv.sumComm m n) : (a : Matrix (l ⊕ n) (m ⊕ n) α) → Matrix (n ⊕ l) (n ⊕ m) α)
        (fromBlocks A B C D) :
      Matrix (n ⊕ l) (n ⊕ m) α)
    ((reindex (Equiv.sumComm l n) (Equiv.sumComm m n) : (a : Matrix (l ⊕ n) (m ⊕ n) α) → Matrix (n ⊕ l) (n ⊕ m) α)
        (HMul.hMul (β := Matrix (m ⊕ n) (m ⊕ n) α)
          (HMul.hMul (α := Matrix (l ⊕ n) (l ⊕ n) α)
            (fromBlocks 1 (B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _) 0 1)
            (fromBlocks (A - B * @Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 0 0 D))
          (fromBlocks 1 0 (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one D _ * C) 1)) :
      Matrix (n ⊕ l) (n ⊕ m) α)

Tactic:
simpa [reindex_apply, Equiv.sumComm_symm, ← submatrix_mul_equiv _ _ _ (Equiv.sumComm n m), ←
      submatrix_mul_equiv _ _ _ (Equiv.sumComm n l), Equiv.sumComm_apply,
      fromBlocks_submatrix_sum_swap_sum_swap] using fromBlocks_eq_of_invertible₁₁ D C B A

Premises used: Equiv.sumComm_symm, Matrix.fromBlocks_eq_of_invertible₁₁, Matrix.fromBlocks_submatrix_sum_swap_sum_swap, Equiv.sumComm, Matrix.reindex_apply, Equiv.sumComm_apply, Matrix.submatrix_mul_equiv