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

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
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
h : Disjoint G H
⊢ Disjoint (neighborSet G x) (neighborSet H x)
Tactic:
exact neighborSet_disjoint h
State after:
no goals