case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ a✝ ∈ (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v}) ↔ a✝ ∈ neighborFinset G vᶜ ∩ neighborFinset G wᶜ
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
⊢ (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v}) = neighborFinset G vᶜ ∩ neighborFinset G wᶜ
ext
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ ¬Adj G v a✝ → ¬Adj G w a✝ → ¬(a✝ = w ∨ a✝ = v)
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ a✝ ∈ (neighborFinset G vᶜ ∩ neighborFinset G wᶜ) \ ({w} ∪ {v}) ↔ a✝ ∈ neighborFinset G vᶜ ∩ neighborFinset G wᶜ
simp only [and_imp, mem_union, mem_sdiff, mem_compl, and_iff_left_iff_imp, mem_neighborFinset,
  mem_inter, mem_singleton]
case a.inl
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v a✝ : V
hnv : ¬Adj G v a✝
h : Adj G v a✝
hnw : ¬Adj G a✝ a✝
⊢ False

case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ False
case a
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v w : V
h : Adj G v w
a✝ : V
⊢ ¬Adj G v a✝ → ¬Adj G w a✝ → ¬(a✝ = w ∨ a✝ = v)
rintro hnv hnw (rfl | rfl)
no goals
case a.inl
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
v a✝ : V
hnv : ¬Adj G v a✝
h : Adj G v a✝
hnw : ¬Adj G a✝ a✝
⊢ False
exact hnv h
case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ Adj G w a✝
case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ False
apply hnw
no goals
case a.inr
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
w a✝ : V
hnw : ¬Adj G w a✝
h : Adj G a✝ w
hnv : ¬Adj G a✝ a✝
⊢ Adj G w a✝
rwa [adj_comm]