case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ a✝ ∈ neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w}) ↔
    a✝ ∈ (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
⊢ neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w}) = (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})
ext
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ ¬a✝ ∈ neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w}) ↔
    ¬a✝ ∈ (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ a✝ ∈ neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w}) ↔
    a✝ ∈ (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})
rw [← not_iff_not]
no goals
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w a✝ : V
⊢ ¬a✝ ∈ neighborFinset G vᶜ \ {v} ∩ (neighborFinset G wᶜ \ {w}) ↔
    ¬a✝ ∈ (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v})
simp [imp_iff_not_or, or_assoc, or_comm, or_left_comm]