case inl
α : Type u_1
β : Type ?u.560
R : Type ?u.563
n : Type u_2
m : Type ?u.569
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i : n
⊢ diagonal (diag A) i i = A i i

case inr
α : Type u_1
β : Type ?u.560
R : Type ?u.563
n : Type u_2
m : Type ?u.569
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i j : n
hij : i ≠ j
⊢ diagonal (diag A) i j = A i j
α : Type u_1
β : Type ?u.560
R : Type ?u.563
n : Type u_2
m : Type ?u.569
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i j : n
⊢ diagonal (diag A) i j = A i j
obtain rfl | hij := Decidable.eq_or_ne i j
no goals
case inl
α : Type u_1
β : Type ?u.560
R : Type ?u.563
n : Type u_2
m : Type ?u.569
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i : n
⊢ diagonal (diag A) i i = A i i
rw [diagonal_apply_eq, diag]
no goals
case inr
α : Type u_1
β : Type ?u.560
R : Type ?u.563
n : Type u_2
m : Type ?u.569
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : IsDiag A
i j : n
hij : i ≠ j
⊢ diagonal (diag A) i j = A i j
rw [diagonal_apply_ne _ hij, h hij]