simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]
α : Type u_1
G H : SimpleGraph α
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype ↑H.edgeSet
⊢ Disjoint G.edgeFinset H.edgeFinset ↔ Disjoint G H
no goals