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

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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
⊢ ∀ (B : Finset α), B ⊆ A → ¬IsNClique G s B
Tactic:
intro B hB
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ ¬IsNClique G s B

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ ¬IsNClique G s B
Tactic:
rw [isNClique_iff]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ ¬(IsClique G ↑B ∧ card B = s)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ ¬(IsClique G ↑B ∧ card B = s)
Tactic:
push_neg
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ IsClique G ↑B → card B ≠ s

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ IsClique G ↑B → card B ≠ s
Tactic:
intro
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
_✝ : IsClique G ↑B
⊢ card B ≠ s

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
_✝ : IsClique G ↑B
⊢ card B ≠ s
Tactic:
exact _root_.ne_of_lt (lt_of_le_of_lt (card_le_of_subset hB) h)
State after:
no goals