case a.h
V : Type u_2
α : Type u_1
β : Type ?u.27033
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i✝ x✝ : V
⊢ (adjMatrix α G)ᵀ i✝ x✝ = adjMatrix α G i✝ x✝
V : Type u_2
α : Type u_1
β : Type ?u.27033
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
⊢ (adjMatrix α G)ᵀ = adjMatrix α G
ext
no goals
case a.h
V : Type u_2
α : Type u_1
β : Type ?u.27033
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Zero α
inst✝ : One α
i✝ x✝ : V
⊢ (adjMatrix α G)ᵀ i✝ x✝ = adjMatrix α G i✝ x✝
simp [adj_comm]