case Adj.h.h.a
ι : Sort ?u.216907
𝕜 : Type ?u.216910
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
f : V ↪ W
G : SimpleGraph V
x✝¹ x✝ : V
⊢ Adj (SimpleGraph.comap (↑f) (SimpleGraph.map f G)) x✝¹ x✝ ↔ Adj G x✝¹ x✝
ι : Sort ?u.216907
𝕜 : Type ?u.216910
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
f : V ↪ W
G : SimpleGraph V
⊢ SimpleGraph.comap (↑f) (SimpleGraph.map f G) = G
ext
no goals
case Adj.h.h.a
ι : Sort ?u.216907
𝕜 : Type ?u.216910
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
f : V ↪ W
G : SimpleGraph V
x✝¹ x✝ : V
⊢ Adj (SimpleGraph.comap (↑f) (SimpleGraph.map f G)) x✝¹ x✝ ↔ Adj G x✝¹ x✝
simp