awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
have a : ∀ (j k : n),
  (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j k
Tactic: ext j k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j k : n
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j k
have a : (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j =
  diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j j
Tactic: obtain rfl | hjk := eq_or_ne j k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j k : n
a :
  (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j j
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j k
have a₁ : ∀ (hjk : j ≠ k),
  (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j k
Tactic: obtain rfl | hjk := eq_or_ne j k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j j
have a : (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j = Function.update (β := fun (a : n) ↦ α) v i x j
Tactic: rw [diagonal_apply_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j = Function.update (β := fun (a : n) ↦ α) v i x j
have a : (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) j x) j j = Function.update (β := fun (a : n) ↦ α) v j x j
Tactic: obtain rfl | hji := eq_or_ne j i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j : n
a : (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) j x) j j = Function.update (β := fun (a : n) ↦ α) v j x j
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j = Function.update (β := fun (a : n) ↦ α) v i x j
have a₁ : ∀ (hji : j ≠ i),
  (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j = Function.update (β := fun (a : n) ↦ α) v i x j
Tactic: obtain rfl | hji := eq_or_ne j i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
x : α
j : n
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) j x) j j = Function.update (β := fun (a : n) ↦ α) v j x j
have a : Pi.single (M := fun (a : n) ↦ α) j x j = Function.update (β := fun (a : n) ↦ α) v j x j
Tactic: rw [updateCol_self, Pi.single_eq_same, Function.update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
x : α
j : n
a : Pi.single (M := fun (a : n) ↦ α) j x j = Function.update (β := fun (a : n) ↦ α) v j x j
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) j x) j j = Function.update (β := fun (a : n) ↦ α) v j x j
have a₁ : x = Function.update (β := fun (a : n) ↦ α) v j x j
Tactic: rw [updateCol_self, Pi.single_eq_same, Function.update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
x : α
j : n
a : Pi.single (M := fun (a : n) ↦ α) j x j = Function.update (β := fun (a : n) ↦ α) v j x j
a₁ : x = Function.update (β := fun (a : n) ↦ α) v j x j
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) j x) j j = Function.update (β := fun (a : n) ↦ α) v j x j
have a₂ : x = x
Tactic: rw [updateCol_self, Pi.single_eq_same, Function.update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j = Function.update (β := fun (a : n) ↦ α) v i x j
have a : diagonal v j j = Function.update (β := fun (a : n) ↦ α) v i x j
Tactic: rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
a : diagonal v j j = Function.update (β := fun (a : n) ↦ α) v i x j
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j = Function.update (β := fun (a : n) ↦ α) v i x j
have a₁ : v j = Function.update (β := fun (a : n) ↦ α) v i x j
Tactic: rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
a : diagonal v j j = Function.update (β := fun (a : n) ↦ α) v i x j
a₁ : v j = Function.update (β := fun (a : n) ↦ α) v i x j
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j j = Function.update (β := fun (a : n) ↦ α) v i x j
have a₂ : v j = v j
Tactic: rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j k
have a : (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
Tactic: rw [diagonal_apply_ne _ hjk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
have a : (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) k x) j k = 0
Tactic: obtain rfl | hki := eq_or_ne k i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
a : (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) k x) j k = 0
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
have a₁ : ∀ (hki : k ≠ i), (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
Tactic: obtain rfl | hki := eq_or_ne k i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) k x) j k = 0
have a : Eq.{v + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) k x j : α) (0 : α)
Tactic: rw [updateCol_self, Pi.single_eq_of_ne hjk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
a : Eq.{v + 1} (α := α) (Pi.single (M := fun (a : n) ↦ α) k x j : α) (0 : α)
⊢ (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) k x) j k = 0
have a₁ : Eq.{v + 1} (α := α) 0 0
Tactic: rw [updateCol_self, Pi.single_eq_of_ne hjk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
have a : diagonal v j k = 0
Tactic: rw [updateCol_ne hki, diagonal_apply_ne _ hjk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
a : diagonal v j k = 0
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
have a₁ : Eq.{v + 1} (α := α) 0 0
Tactic: rw [updateCol_ne hki, diagonal_apply_ne _ hjk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
⊢ (diagonal v).updateRow i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
have rw : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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)
⊢ (diagonal v).updateRow i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
have rw₁ : ((diagonal v).updateCol 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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)
⊢ (diagonal v).updateRow i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
have rw₂ : (diagonal (Function.update (β := fun (a : n) ↦ α) v i x))ᵀ = diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
Tactic: rw [← diagonal_transpose, updateRow_transpose, diagonal_updateCol_single, diagonal_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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)
⊢ (diagonal v).updateRow i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
have rw₃ : diagonal (Function.update (β := fun (a : n) ↦ α) v i x) = diagonal (Function.update (β := fun (a : n) ↦ α) v i x)
Tactic: rw [← diagonal_transpose, updateRow_transpose, diagonal_updateCol_single, diagonal_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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
⊢ 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)
have 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
Tactic: ext i' j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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 → α
⊢ A.updateRow i c *ᵥ v = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v)
have h : ∀ (i' : l), (A.updateRow i c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v) i'
Tactic: ext i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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
⊢ (A.updateRow i c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v) i'
have h : (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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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'
⊢ (A.updateRow i c *ᵥ v) i' = Function.update (β := fun (a : l) ↦ α) (A *ᵥ v) i (c ⬝ᵥ v) i'
have h₁ : ∀ (hi : i' ≠ 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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 → α
⊢ v ᵥ* B.updateCol j r = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r)
have h : ∀ (j' : n), (v ᵥ* B.updateCol j r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r) j'
Tactic: ext j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r) j'
have h : (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
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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'
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (β := fun (a : n) ↦ α) (v ᵥ* B) j (v ⬝ᵥ r) j'
have h₁ : ∀ (hj : j' ≠ 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : Mul α
u : m → α
v : n → α
i : m
a : α
⊢ vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v = (vecMulVec u v).updateRow i (a • v)
have 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: ext i' j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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
⊢ vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j
have a₁ : 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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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
⊢ vecMulVec (Function.update (β := fun (a : m) ↦ α) u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j
have 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
Tactic: obtain rfl | hi := eq_or_ne i' i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Mul α
u : m → α
v : n → α
j : n
a : α
⊢ vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) = (vecMulVec u v).updateCol j (MulOpposite.op a • u)
have 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: ext i j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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
⊢ vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) i j' =
    (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'
have a₁ : 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
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.RowCol (goal)
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'
⊢ vecMulVec u (Function.update (β := fun (a : n) ↦ α) v j a) i j' =
    (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'
have 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'
Tactic: obtain rfl | hi := eq_or_ne j' j
-- 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 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
⊢ A.updateRow i r * B = (A * B).updateRow i (r ᵥ* B)
have a : ∀ (i' : l) (j' : n), (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
Tactic: ext i' j'
-- 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 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
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'
have a : (A.updateRow i' r * B) i' j' = (A * B).updateRow i' (r ᵥ* B) i' j'
Tactic: obtain rfl | hi := eq_or_ne i' i
Cleared hypotheses: i
-- 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 : 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.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
have a₁ : ∀ (hi : i' ≠ i), (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
Tactic: obtain rfl | hi := eq_or_ne i' i
-- 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 n
inst_1 : Fintype m
inst_2 : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
⊢ A * B.updateCol j c = (A * B).updateCol j (A *ᵥ c)
have a : ∀ (i' : l) (j' : n), (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'
Tactic: ext i' j'
-- 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 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 * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'
have a : (A * B.updateCol j' c) i' j' = (A * B).updateCol j' (A *ᵥ c) i' j'
Tactic: obtain rfl | hj := eq_or_ne j' j
Cleared hypotheses: j
-- 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 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 * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'
have a₁ : ∀ (hj : j' ≠ 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
-- 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 m
inst_1 : DecidableEq n
inst_2 : Fintype m
inst_3 : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : m
j : n
r : α
⊢ A * single i j r = updateCol 0 j (A.col i <• r)
have 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)
Tactic: rw [single_eq_updateCol_zero, mul_updateCol, Matrix.mul_zero, mulVec_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 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)
⊢ A * single i j r = updateCol 0 j (A.col i <• r)
have rw₁ : (A * 0).updateCol j (A *ᵥ Pi.single (M := fun (a : m) ↦ α) i r) = updateCol 0 j (A.col i <• r)
Tactic: rw [single_eq_updateCol_zero, mul_updateCol, Matrix.mul_zero, mulVec_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 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)
⊢ A * single i j r = updateCol 0 j (A.col i <• r)
have rw₂ : updateCol 0 j (A *ᵥ Pi.single (M := fun (a : m) ↦ α) i r) = updateCol 0 j (A.col i <• r)
Tactic: rw [single_eq_updateCol_zero, mul_updateCol, Matrix.mul_zero, mulVec_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 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)
⊢ A * single i j r = updateCol 0 j (A.col i <• r)
have rw₃ : updateCol 0 j (A.col i <• r) = updateCol 0 j (A.col i <• r)
Tactic: rw [single_eq_updateCol_zero, mul_updateCol, Matrix.mul_zero, mulVec_single]