case h
l : Type ?u.25244
m : Type ?u.25247
n : Type u_1
R : Type ?u.25253
α : Type u_2
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
l : Type ?u.25244
m : Type ?u.25247
n : Type u_1
R : Type ?u.25253
α : Type u_2
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j : n
c : α
i' j' : n
⊢ diag (stdBasisMatrix i i c) = Pi.single i c
ext j
no goals
case h
l : Type ?u.25244
m : Type ?u.25247
n : Type u_1
R : Type ?u.25253
α : Type u_2
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
by_cases hij : i = j <;> (try rw [hij]) <;> simp [hij]
case neg
l : Type ?u.25244
m : Type ?u.25247
n : Type u_1
R : Type ?u.25253
α : Type u_2
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
case neg
l : Type ?u.25244
m : Type ?u.25247
n : Type u_1
R : Type ?u.25253
α : Type u_2
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
try rw [hij]
case neg
l : Type ?u.25244
m : Type ?u.25247
n : Type u_1
R : Type ?u.25253
α : Type u_2
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
case neg
l : Type ?u.25244
m : Type ?u.25247
n : Type u_1
R : Type ?u.25253
α : Type u_2
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
rw [hij]