rw [coe_insert]
case clique
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ IsClique G ↑(insert v B)
case clique
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ IsClique G (insert v ↑B)