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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h : CliqueFree G s
U : Finset α
⊢ CliqueFreeSet U s
Tactic:
revert h
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ CliqueFree G s → CliqueFreeSet U s

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ CliqueFree G s → CliqueFreeSet U s
Tactic:
contrapose
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ ¬CliqueFreeSet U s → ¬CliqueFree G s

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ ¬CliqueFreeSet U s → ¬CliqueFree G s
Tactic:
rw [CliqueFreeSet]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ (¬∀ (B : Finset α), B ⊆ U → ¬IsNClique G s B) → ¬CliqueFree G s

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ (¬∀ (B : Finset α), B ⊆ U → ¬IsNClique G s B) → ¬CliqueFree G s
Tactic:
push_neg
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ (∃ B, B ⊆ U ∧ IsNClique G s B) → ¬CliqueFree G s

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ (∃ B, B ⊆ U ∧ IsNClique G s B) → ¬CliqueFree G s
Tactic:
intro h
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ¬CliqueFree G s

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ¬CliqueFree G s
Tactic:
rw [CliqueFree]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ¬∀ (t : Finset α), ¬IsNClique G s t

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ¬∀ (t : Finset α), ¬IsNClique G s t
Tactic:
push_neg
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ∃ t, IsNClique G s t

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ∃ t, IsNClique G s t
Tactic:
obtain ⟨B, _, h2⟩ := h
State after:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U B : Finset α
left✝ : B ⊆ U
h2 : IsNClique G s B
⊢ ∃ t, IsNClique G s t

State before:
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U B : Finset α
left✝ : B ⊆ U
h2 : IsNClique G s B
⊢ ∃ t, IsNClique G s t
Tactic:
exact ⟨B, h2⟩
State after:
no goals