Theorem: SimpleGraph.disjoint_edgeSet (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
⊢ Disjoint (edgeSet G) (edgeSet H) ↔ Disjoint G H
Tactic:
rw [Set.disjoint_iff_inter_eq_empty, disjoint_iff, ← edgeSet_inf, edgeSet_eq_empty_iff]
State after:
no goals