case Adj.h.h.a
V : Type u_2
α : Type u_1
β : Type ?u.29980
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ Adj (IsAdjMatrix.toGraph (_ : IsAdjMatrix (adjMatrix α G))) x✝¹ x✝ ↔ Adj G x✝¹ x✝
V : Type u_2
α : Type u_1
β : Type ?u.29980
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
⊢ IsAdjMatrix.toGraph (_ : IsAdjMatrix (adjMatrix α G)) = G
ext
case Adj.h.h.a
V : Type u_2
α : Type u_1
β : Type ?u.29980
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ¬Adj G x✝¹ x✝ → False ↔ Adj G x✝¹ x✝
case Adj.h.h.a
V : Type u_2
α : Type u_1
β : Type ?u.29980
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ Adj (IsAdjMatrix.toGraph (_ : IsAdjMatrix (adjMatrix α G))) x✝¹ x✝ ↔ Adj G x✝¹ x✝
simp only [IsAdjMatrix.toGraph_Adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]
no goals
case Adj.h.h.a
V : Type u_2
α : Type u_1
β : Type ?u.29980
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ¬Adj G x✝¹ x✝ → False ↔ Adj G x✝¹ x✝
apply Classical.not_not