case a.h
α : Type u_1
β : Type ?u.21624
R : Type ?u.21627
n : Type u_2
m : Type ?u.21633
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
⊢ Aᵀ i j = A i j
α : Type u_1
β : Type ?u.21624
R : Type ?u.21627
n : Type u_2
m : Type ?u.21633
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
⊢ IsSymm A
ext (i j)
case pos
α : Type u_1
β : Type ?u.21624
R : Type ?u.21627
n : Type u_2
m : Type ?u.21633
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
g : i = j
⊢ Aᵀ i j = A i j

case neg
α : Type u_1
β : Type ?u.21624
R : Type ?u.21627
n : Type u_2
m : Type ?u.21633
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j
case a.h
α : Type u_1
β : Type ?u.21624
R : Type ?u.21627
n : Type u_2
m : Type ?u.21633
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
⊢ Aᵀ i j = A i j
by_cases g : i = j
no goals
case neg
α : Type u_1
β : Type ?u.21624
R : Type ?u.21627
n : Type u_2
m : Type ?u.21633
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j
simp [h g, h (Ne.symm g)]
no goals
case pos
α : Type u_1
β : Type ?u.21624
R : Type ?u.21627
n : Type u_2
m : Type ?u.21633
inst✝ : Zero α
A : Matrix n n α
h : IsDiag A
i j : n
g : i = j
⊢ Aᵀ i j = A i j
rw [g, transpose_apply]