no goals
ι : Sort ?u.107664
𝕜 : Type ?u.107667
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
G₁ G₂ : SimpleGraph V
inst✝² : Fintype ↑(edgeSet G)
inst✝¹ : Fintype ↑(edgeSet G₁)
inst✝ : Fintype ↑(edgeSet G₂)
⊢ edgeFinset G₁ ⊆ edgeFinset G₂ ↔ G₁ ≤ G₂
simp