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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
⊢ ∀ (v : α), v ∈ A → degRes G v A = 0
Tactic:
intro v hv
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ degRes G v A = 0

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ degRes G v A = 0
Tactic:
rw [degRes, card_eq_zero]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ nbhdRes G v A = ∅

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ nbhdRes G v A = ∅
Tactic:
contrapose hA
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
⊢ ¬CliqueFreeSet A 2

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
⊢ ¬CliqueFreeSet A 2
Tactic:
obtain ⟨w, hw⟩ := exists_mem_nempty G hA
State after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬CliqueFreeSet A 2

State before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬CliqueFreeSet A 2
Tactic:
rw [CliqueFreeSet]
State after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬∀ (B : Finset α), B ⊆ A → ¬IsNClique G 2 B

State before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬∀ (B : Finset α), B ⊆ A → ¬IsNClique G 2 B
Tactic:
push_neg
State after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ∃ B, B ⊆ A ∧ IsNClique G 2 B

State before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ∃ B, B ⊆ A ∧ IsNClique G 2 B
Tactic:
exact ⟨{v, w}, pair_subset hv hw.1, adj_is2Clique hw.2⟩
State after:
no goals