case a.h
V : Type u_2
α : Type u_1
β : Type ?u.14711
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : IsSymm A
i✝ x✝ : V
⊢ (compl A)ᵀ i✝ x✝ = compl A i✝ x✝
V : Type u_2
α : Type u_1
β : Type ?u.14711
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : IsSymm A
⊢ IsSymm (compl A)
ext
no goals
case a.h
V : Type u_2
α : Type u_1
β : Type ?u.14711
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
h : IsSymm A
i✝ x✝ : V
⊢ (compl A)ᵀ i✝ x✝ = compl A i✝ x✝
simp [compl, h.apply, eq_comm]