Theorem: SimpleGraph.neighborFinset_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
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
⊢ neighborFinset (G ⊓ H) x = neighborFinset G x ∩ neighborFinset H x
Tactic:
ext y
State after:
case a
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
y : V
⊢ y ∈ neighborFinset (G ⊓ H) x ↔ y ∈ neighborFinset G x ∩ neighborFinset H x

State before:
case a
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝³ : DecidableEq V
G H : SimpleGraph V
x : V
inst✝² : Fintype ↑(neighborSet (G ⊓ H) x)
inst✝¹ : Fintype ↑(neighborSet G x)
inst✝ : Fintype ↑(neighborSet H x)
y : V
⊢ y ∈ neighborFinset (G ⊓ H) x ↔ y ∈ neighborFinset G x ∩ neighborFinset H x
Tactic:
simp
State after:
no goals