Theorem: SimpleGraph.disjoint_left (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 G H ↔ ∀ (x y : V), Adj G x y → ¬Adj H x y
Tactic:
simp only [← disjoint_edgeSet, Set.disjoint_left, Sym2.forall, mem_edgeSet]
State after:
no goals