awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Star α
v : m → α
a : ∀ (i : ι) (j : m), (replicateCol ι v)ᴴ i j = replicateRow ι (star v) i j
⊢ (replicateCol ι v)ᴴ = replicateRow ι (star v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Star α
v : m → α
i : ι
j : m
⊢ (replicateCol ι v)ᴴ i j = replicateRow ι (star v) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Star α
v : m → α
a : ∀ (i : m) (j : ι), (replicateRow ι v)ᴴ i j = replicateCol ι (star v) i j
⊢ (replicateRow ι v)ᴴ = replicateCol ι (star v)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Star α
v : m → α
i : m
j : ι
⊢ (replicateRow ι v)ᴴ i j = replicateCol ι (star v) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
a : ∀ (i : ι) (j : n), replicateRow ι (v ᵥ* M) i j = (replicateRow ι v * M) i j
⊢ replicateRow ι (v ᵥ* M) = replicateRow ι v * M

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i : ι
j : n
⊢ replicateRow ι (v ᵥ* M) i j = (replicateRow ι v * M) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
a : ∀ (i : n) (j : ι), replicateCol ι (v ᵥ* M) i j = (replicateRow ι v * M)ᵀ i j
⊢ replicateCol ι (v ᵥ* M) = (replicateRow ι v * M)ᵀ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i : n
j : ι
⊢ replicateCol ι (v ᵥ* M) i j = (replicateRow ι v * M)ᵀ i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
a : ∀ (i : m) (j : ι), replicateCol ι (M *ᵥ v) i j = (M * replicateCol ι v) i j
⊢ replicateCol ι (M *ᵥ v) = M * replicateCol ι v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i : m
j : ι
⊢ replicateCol ι (M *ᵥ v) i j = (M * replicateCol ι v) i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
a : ∀ (i : ι) (j : m), replicateRow ι (M *ᵥ v) i j = (M * replicateCol ι v)ᵀ i j
⊢ replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i : ι
j : m
⊢ replicateRow ι (M *ᵥ v) i j = (M * replicateCol ι v)ᵀ i j

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
v w : m → α
⊢ replicateRow ι v *ᵥ w = Function.const ι (v ⬝ᵥ w)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.replicateRow, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : NonUnitalNonAssocSemiring α
v w : m → α
⊢ v ᵥ* replicateCol ι w = Function.const ι (v ⬝ᵥ w)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.vecMul, Matrix.replicateCol, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : Mul α
inst_2 : AddCommMonoid α
v w : m → α
⊢ replicateRow ι v * replicateCol ι w = (of : (a : ι → ι → α) → Matrix ι ι α) fun (x x_1 : ι) ↦ v ⬝ᵥ w

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.replicateCol, Matrix.replicateRow, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
α : Type v
ι : Type u_6
inst : Fintype m
inst_1 : Mul α
inst_2 : AddCommMonoid α
v w : m → α
i j : ι
⊢ (replicateRow ι v * replicateCol ι w) i j = v ⬝ᵥ w

Tactic:
rfl

Premises used: Matrix.replicateCol, Matrix.replicateRow, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Mul α
inst_1 : AddCommMonoid α
inst_2 : Unique ι
a b : n → α
h : ∀ (x : n), (replicateCol ι a * replicateRow ι b).diag x = (a * b) x
⊢ (replicateCol ι a * replicateRow ι b).diag = a * b

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
ι : Type u_6
inst : Mul α
inst_1 : AddCommMonoid α
inst_2 : Unique ι
a b : n → α
x : n
⊢ (replicateCol ι a * replicateRow ι b).diag x = (a * b) x

Tactic:
simp [Matrix.mul_apply, replicateCol, replicateRow]

Premises used: Matrix.replicateCol, Matrix.mul_apply, Matrix.replicateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Mul α
inst_1 : AddCommMonoid α
inst_2 : Unique ι
w : m → α
v : n → α
a : ∀ (i : m) (j : n), vecMulVec w v i j = (replicateCol ι w * replicateRow ι v) i j
⊢ vecMulVec w v = replicateCol ι w * replicateRow ι v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst : Mul α
inst_1 : AddCommMonoid α
inst_2 : Unique ι
w : m → α
v : n → α
i : m
j : n
⊢ vecMulVec w v i j = (replicateCol ι w * replicateRow ι v) i j

Tactic:
simp [vecMulVec, mul_apply]

Premises used: Matrix.mul_apply, Matrix.vecMulVec
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
⊢ M.updateRow i b i = b

Tactic:
Function.update_self (β := fun _ => (n → α)) i b M

Premises used: Function.update, dite, Function.update_self, Matrix.updateRow
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
⊢ M.updateCol j c i j = c i

Tactic:
Function.update_self (β := fun _ => α) j (c i) (M i)

Premises used: Function.update, dite, Function.update_self, Matrix.updateCol
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
i' : m
i_ne : i' ≠ i
⊢ M.updateRow i b i' = M i'

Tactic:
Function.update_of_ne (β := fun _ => (n → α)) i_ne b M

Premises used: Function.update, dite, Matrix.updateRow, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
j_ne : j' ≠ j
⊢ M.updateCol j c i j' = M i j'

Tactic:
Function.update_of_ne (β := fun _ => α) j_ne (c i) (M i)

Premises used: Function.update, dite, Matrix.updateCol, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
pos : ∀ (h : i' = i), M.updateRow i b i' j = if i' = i then b j else M i' j
neg : ∀ (h : ¬i' = i), M.updateRow i b i' j = if i' = i then b j else M i' j
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
by_cases h : i' = i
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
h : i' = i
pos : M.updateRow i b i j = if i = i then b j else M i j
pos₁ : b j = if i = i then b j else M i j
pos₂ pos₃ : b j = b j
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
rw [h, updateRow_self, if_pos rfl]

Premises used: if_pos, Matrix.updateRow_self, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst : DecidableEq m
i' : m
h : ¬i' = i
neg : M i' j = if i' = i then b j else M i' j
neg₁ neg₂ : M i' j = M i' j
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
rw [updateRow_ne h, if_neg h]

Premises used: Matrix.updateRow_ne, if_neg
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
pos : ∀ (h : j' = j), M.updateCol j c i j' = if j' = j then c i else M i j'
neg : ∀ (h : ¬j' = j), M.updateCol j c i j' = if j' = j then c i else M i j'
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
by_cases h : j' = j
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
h : j' = j
pos : M.updateCol j c i j = if j = j then c i else M i j
pos₁ : c i = if j = j then c i else M i j
pos₂ pos₃ : c i = c i
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
rw [h, updateCol_self, if_pos rfl]

Premises used: Matrix.updateCol_self, if_pos, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst : DecidableEq n
j' : n
h : ¬j' = j
neg : M i j' = if j' = j then c i else M i j'
neg₁ neg₂ : M i j' = M i j'
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
rw [updateCol_ne h, if_neg h]

Premises used: Matrix.updateCol_ne, if_neg
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : Subsingleton n
A : Matrix m n R
i : n
b : m → R
a : ∀ (x : m) (y : n), A.updateCol i b x y = submatrix (n := Fin 1) (replicateCol (Fin 1) b) id (Function.const n 0) x y
⊢ A.updateCol i b = submatrix (n := Fin 1) (replicateCol (Fin 1) b) id (Function.const n 0)

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : Subsingleton n
A : Matrix m n R
i : n
b : m → R
x : m
y : n
⊢ A.updateCol i b x y = submatrix (n := Fin 1) (replicateCol (Fin 1) b) id (Function.const n 0) x y

Tactic:
simp [Subsingleton.elim i y]

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : Subsingleton m
A : Matrix m n R
i : m
b : n → R
a : ∀ (x : m) (y : n), A.updateRow i b x y = submatrix (m := Fin 1) (replicateRow (Fin 1) b) (Function.const m 0) id x y
⊢ A.updateRow i b = submatrix (m := Fin 1) (replicateRow (Fin 1) b) (Function.const m 0) id

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
inst : Subsingleton m
A : Matrix m n R
i : m
b : n → R
x : m
y : n
⊢ A.updateRow i b x y = submatrix (m := Fin 1) (replicateRow (Fin 1) b) (Function.const m 0) id x y

Tactic:
simp [Subsingleton.elim i x]

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
f : α → β
a : ∀ (i_1 : m) (j : n), (M.updateRow i b).map f i_1 j = (M.map f).updateRow i (f ∘ b) i_1 j
⊢ (M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
f : α → β
i_1 : m
j : n
a : f (if i_1 = i then b j else M i_1 j) = if i_1 = i then (f ∘ b) j else f (M i_1 j)
⊢ (M.updateRow i b).map f i_1 j = (M.map f).updateRow i (f ∘ b) i_1 j

Tactic:
rw [updateRow_apply, map_apply, map_apply, updateRow_apply]

Premises used: Matrix.map_apply, Matrix.updateRow_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
f : α → β
i_1 : m
j : n
⊢ f (if i_1 = i then b j else M i_1 j) = if i_1 = i then (f ∘ b) j else f (M i_1 j)

Tactic:
apply_ite f _ _ _

Premises used: apply_ite
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
f : α → β
i_1 : m
j : n
⊢ f (if i_1 = i then b j else M i_1 j) = if i_1 = i then (f ∘ b) j else f (M i_1 j)

Tactic:
exact apply_ite f _ _ _

Premises used: apply_ite
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
f : α → β
a : ∀ (i : m) (j_1 : n), (M.updateCol j c).map f i j_1 = (M.map f).updateCol j (f ∘ c) i j_1
⊢ (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
f : α → β
i : m
j_1 : n
a : f (if j_1 = j then c i else M i j_1) = if j_1 = j then (f ∘ c) i else f (M i j_1)
⊢ (M.updateCol j c).map f i j_1 = (M.map f).updateCol j (f ∘ c) i j_1

Tactic:
rw [updateCol_apply, map_apply, map_apply, updateCol_apply]

Premises used: Matrix.updateCol_apply, Matrix.map_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
f : α → β
i : m
j_1 : n
⊢ f (if j_1 = j then c i else M i j_1) = if j_1 = j then (f ∘ c) i else f (M i j_1)

Tactic:
apply_ite f _ _ _

Premises used: apply_ite
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
f : α → β
i : m
j_1 : n
⊢ f (if j_1 = j then c i else M i j_1) = if j_1 = j then (f ∘ c) i else f (M i j_1)

Tactic:
exact apply_ite f _ _ _

Premises used: apply_ite
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
a : ∀ (i : n) (j_1 : m), Mᵀ.updateRow j c i j_1 = (M.updateCol j c)ᵀ i j_1
⊢ Mᵀ.updateRow j c = (M.updateCol j c)ᵀ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
i : n
j_1 : m
a : (if i = j then c j_1 else Mᵀ i j_1) = if i = j then c j_1 else M j_1 i
⊢ Mᵀ.updateRow j c i j_1 = (M.updateCol j c)ᵀ i j_1

Tactic:
rw [transpose_apply, updateRow_apply, updateCol_apply]

Premises used: Matrix.updateCol_apply, Matrix.transpose_apply, Matrix.updateRow_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
i : n
j_1 : m
⊢ (if i = j then c j_1 else Mᵀ i j_1) = if i = j then c j_1 else M j_1 i

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
a : ∀ (i_1 : n) (j : m), Mᵀ.updateCol i b i_1 j = (M.updateRow i b)ᵀ i_1 j
⊢ Mᵀ.updateCol i b = (M.updateRow i b)ᵀ

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
i_1 : n
j : m
a : (if j = i then b i_1 else Mᵀ i_1 j) = if j = i then b i_1 else M j i_1
⊢ Mᵀ.updateCol i b i_1 j = (M.updateRow i b)ᵀ i_1 j

Tactic:
rw [transpose_apply, updateRow_apply, updateCol_apply]

Premises used: Matrix.updateCol_apply, Matrix.transpose_apply, Matrix.updateRow_apply
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
i_1 : n
j : m
⊢ (if j = i then b i_1 else Mᵀ i_1 j) = if j = i then b i_1 else M j i_1

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
inst_1 : Star α
rw : ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ
⊢ Mᴴ.updateRow j (star c) = (M.updateCol j c)ᴴ

Tactic:
rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateRow_transpose,
    map_updateCol]

Premises used: Matrix.updateRow_transpose, Matrix.transpose_map, Matrix.map_updateCol, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst : DecidableEq n
inst_1 : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
inst_1 : Star α
rw : ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ
⊢ Mᴴ.updateCol i (star b) = (M.updateRow i b)ᴴ

Tactic:
rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateCol_transpose,
    map_updateRow]

Premises used: Matrix.map_updateRow, Matrix.transpose_map, Matrix.updateCol_transpose, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst : DecidableEq m
inst_1 : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ

Tactic:
rfl
-- 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
⊢ A.updateRow i (A i) = A

Tactic:
Function.update_eq_self i A

Premises used: Function.update_eq_self, Function.update, Matrix, 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 α
i : n
⊢ (A.updateCol i fun (j : m) ↦ A j i) = A

Tactic:
funext fun j => Function.update_eq_self i (A j)

Premises used: Function.update_eq_self, Matrix, funext
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq m
inst_1 : Zero α
i : m
⊢ Eq (α := Matrix m n α) (updateRow 0 i 0) 0

Tactic:
updateRow_eq_self _ i

Premises used: Matrix.updateRow_eq_self
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
m : Type u_2
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
i : n
⊢ Eq (α := Matrix m n α) (updateCol 0 i 0) 0

Tactic:
updateCol_eq_self _ i

Premises used: Matrix.updateCol_eq_self
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
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
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x)

Tactic:
ext j k
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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
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
⊢ (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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
Goal:
n : Type u_3
α : Type v
inst : DecidableEq n
inst_1 : Zero α
v : n → α
i : n
x : α
j : n
a : (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) 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 =
    diagonal (Function.update (β := fun (a : n) ↦ α) v i x) j j

Tactic:
rw [diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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
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
⊢ (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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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
a₂ a₃ : x = x
⊢ (diagonal v).updateCol j (Pi.single (M := fun (a : n) ↦ α) j x) j j = Function.update (β := fun (a : n) ↦ α) v j x j

Tactic:
rw [updateCol_self, Pi.single_eq_same, Function.update_self]

Premises used: Matrix.updateCol_self, Function.update_self, Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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
a₂ a₃ : v j = v j
⊢ (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 [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]

Premises used: Matrix.diagonal_apply_eq, Matrix.updateCol_ne, Function.update_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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 i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
⊢ (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:
rw [diagonal_apply_ne _ hjk]

Premises used: Matrix.diagonal_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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
a₁ : ∀ (hki : k ≠ i), (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0

Tactic:
obtain rfl | hki := eq_or_ne k i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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 : α)
a₁ a₂ : Eq.{v + 1} (α := α) 0 0
⊢ (diagonal v).updateCol k (Pi.single (M := fun (a : n) ↦ α) k x) j k = 0

Tactic:
rw [updateCol_self, Pi.single_eq_of_ne hjk]

Premises used: Matrix.updateCol_self, Pi.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.RowCol
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
a₁ a₂ : Eq.{v + 1} (α := α) 0 0
⊢ (diagonal v).updateCol i (Pi.single (M := fun (a : n) ↦ α) i x) j k = 0

Tactic:
rw [updateCol_ne hki, diagonal_apply_ne _ hjk]

Premises used: Matrix.updateCol_ne, Matrix.diagonal_apply_ne