Theorem: SimpleGraph.isSuccClique (Turan4/CliqueFreeSets.lean)

State before:
α : 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
⊢ IsNClique G (t + 1) (insert v B)
Tactic:
constructor
State after:
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 card_eq
α : 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
⊢ card (insert v B) = t + 1

State before:
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)
Tactic:
rw [coe_insert]
State after:
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)

State before:
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)
Tactic:
exact isClique_insert hv hB h.1
State after:
no goals

State before:
case card_eq
α : 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
⊢ card (insert v B) = t + 1
Tactic:
rw [card_insert_of_not_mem,add_left_inj,h.2]
State after:
case card_eq
α : 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
⊢ ¬v ∈ B

State before:
case card_eq
α : 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
⊢ ¬v ∈ B
Tactic:
apply not_mem_mono hB (G.not_mem_res_nbhd v A)
State after:
no goals