α : Type u_1
G H : SimpleGraph α
m n : ℕ
s✝ : Finset α
h : m ≤ n
hG : CliqueFree G m
s : Finset α
hs : IsNClique G n s
⊢ False
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s : Finset α
h : m ≤ n
⊢ CliqueFree G m → CliqueFree G n
intro hG s hs
case intro.intro
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s✝ : Finset α
h : m ≤ n
hG : CliqueFree G m
s : Finset α
hs : IsNClique G n s
t : Finset α
hts : t ⊆ s
ht : Finset.card t = m
⊢ False
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s✝ : Finset α
h : m ≤ n
hG : CliqueFree G m
s : Finset α
hs : IsNClique G n s
⊢ False
obtain ⟨t, hts, ht⟩ := s.exists_smaller_set _ (h.trans hs.card_eq.ge)
no goals
case intro.intro
α : Type u_1
G H : SimpleGraph α
m n : ℕ
s✝ : Finset α
h : m ≤ n
hG : CliqueFree G m
s : Finset α
hs : IsNClique G n s
t : Finset α
hts : t ⊆ s
ht : Finset.card t = m
⊢ False
exact hG _ ⟨hs.clique.subset hts, ht⟩