rw [← disjoint_coe, coe_neighborFinset, coe_neighborFinset]
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
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
h : Disjoint G H
⊢ Disjoint (neighborFinset G x) (neighborFinset H x)
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
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
h : Disjoint G H
⊢ Disjoint (neighborSet G x) (neighborSet H x)