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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : CliqueFreeSet A (t + 2)
hv : v ∈ A
⊢ CliqueFreeSet (nbhdRes G v A) (t + 1)
Tactic:
rw [CliqueFreeSet] at *
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
⊢ ∀ (B : Finset α), B ⊆ nbhdRes G v A → ¬IsNClique G (t + 1) B

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
⊢ ∀ (B : Finset α), B ⊆ nbhdRes G v A → ¬IsNClique G (t + 1) B
Tactic:
intro B hB
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
⊢ ¬IsNClique G (t + 1) B

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
⊢ ¬IsNClique G (t + 1) B
Tactic:
contrapose! hA
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ ∃ B, B ⊆ A ∧ IsNClique G (t + 2) B

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ ∃ B, B ⊆ A ∧ IsNClique G (t + 2) B
Tactic:
refine ⟨insert v B,?_, isSuccClique hv hB hA⟩
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ insert v B ⊆ A

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ insert v B ⊆ A
Tactic:
exact insert_subset hv (subset_trans hB (G.sub_res_nbhd_A v A))
State after:
no goals