Theorem: SimpleGraph.disjoint_edgeFinset (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Finite.lean)

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