Theorem: SimpleGraph.neighborSet_inf (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
⊢ neighborSet (G ⊓ H) x = neighborSet G x ∩ neighborSet H x
Tactic:
ext y
State after:
case h
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x y : V
⊢ y ∈ neighborSet (G ⊓ H) x ↔ y ∈ neighborSet G x ∩ neighborSet H x

State before:
case h
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
x y : V
⊢ y ∈ neighborSet (G ⊓ H) x ↔ y ∈ neighborSet G x ∩ neighborSet H x
Tactic:
simp only [mem_neighborSet, inf_adj, Set.mem_inter_iff]
State after:
no goals