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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h : 0 < s
⊢ CliqueFreeSet ∅ s
Tactic:
rw [← Finset.card_empty] at h
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h✝ : 0 < s
h : card ∅ < s
⊢ CliqueFreeSet ∅ s

α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h : 0 < s
⊢ Type ?u.2299

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h✝ : 0 < s
h : card ∅ < s
⊢ CliqueFreeSet ∅ s

α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h : 0 < s
⊢ Type ?u.2299
Tactic:
exact G.clique_free_card_lt h
State after:
no goals