Theorem: SimpleGraph.neighborSet_disjoint (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
x : V
h : Disjoint G H
⊢ Disjoint (neighborSet G x) (neighborSet H x)
Tactic:
rw [Set.disjoint_iff_inter_eq_empty, ← neighborSet_inf, h.eq_bot, neighborSet_bot]
State after:
no goals