-- Mathlib/Data/Matrix/RowCol.lean
theorem diagonal_updateCol_single [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
    (diagonal v).updateCol i (Pi.single i x) = diagonal (Function.update v i x)

Proof state:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Tactic:
obtain rfl | hjk := eq_or_ne j k

Result:
case a.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = diagonal (Function.update v i x) j j

case a.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ (diagonal v).updateCol i (Pi.single i x) = diagonal (Function.update v i x)

Tactic:
ext j k

Result:
case a
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Proof state:
case a.inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol k (Pi.single k x) j k = 0

Tactic:
rw [updateCol_self, Pi.single_eq_of_ne hjk]

Result:
no goals

Proof state:
case a.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = diagonal (Function.update v i x) j j

Tactic:
rw [diagonal_apply_eq]

Result:
case a.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Proof state:
case a.inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Tactic:
rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]

Result:
no goals

Proof state:
case a.inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
rw [updateCol_ne hki, diagonal_apply_ne _ hjk]

Result:
no goals

Proof state:
case a.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Tactic:
rw [diagonal_apply_ne _ hjk]

Result:
case a.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Proof state:
case a.inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ (diagonal v).updateCol j (Pi.single j x) j j = Function.update v j x j

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

Result:
no goals

Proof state:
case a.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Tactic:
obtain rfl | hji := eq_or_ne j i

Result:
case a.inl.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j : n
⊢ (diagonal v).updateCol j (Pi.single j x) j j = Function.update v j x j

case a.inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Proof state:
case a.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
obtain rfl | hki := eq_or_ne k i

Result:
case a.inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol k (Pi.single k x) j k = 0

case a.inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0