awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
mp : G.CliqueFree 2 → G = ⊥
mpr mpr₁ : G = ⊥ → G.CliqueFree 2
⊢ G.CliqueFree 2 ↔ G = ⊥

Tactic:
classical
  constructor
  · simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_notMem, Sym2.forall, mem_edgeSet]
    exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩
  · rintro rfl
    exact cliqueFree_bot le_rfl

Premises used: le_rfl, SimpleGraph.cliqueFree_bot, Sym2.forall, Set.eq_empty_iff_forall_notMem, SimpleGraph.edgeSet_eq_empty, SimpleGraph.mem_edgeSet, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
x y : α
t : Finset α
n : ℕ
h : G.CliqueFree n
hc : (G ⊔ edge x y).IsNClique n t
by_contra : ∀ (hf : x ∉ t), False
⊢ x ∈ t

Tactic:
by_contra hf
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
x y : α
t : Finset α
n : ℕ
h : G.CliqueFree n
hc : (G ⊔ edge x y).IsNClique n t
hf : x ∉ t
⊢ (↑t : Set α) \ {x} = (↑t : Set α)

Tactic:
have ht : (t : Set α) \ {x} = t := sdiff_eq_left.mpr <| Set.disjoint_singleton_right.mpr hf
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
x y : α
t : Finset α
n : ℕ
h : G.CliqueFree n
hc : (G ⊔ edge x y).IsNClique n t
hf : x ∉ t
ht : (↑t : Set α) \ {x} = (↑t : Set α)
⊢ False

Tactic:
h t ⟨ht ▸ hc.1.sdiff_of_sup_edge, hc.2⟩

Premises used: SimpleGraph.IsNClique.card_eq, Eq.rec, SimpleGraph.IsNClique.isClique, SimpleGraph.IsClique.sdiff_of_sup_edge, SimpleGraph.IsNClique.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
x y : α
t : Finset α
n : ℕ
h : G.CliqueFree n
hc : (G ⊔ edge x y).IsNClique n t
hf : x ∉ t
ht : (↑t : Set α) \ {x} = (↑t : Set α)
⊢ False

Tactic:
exact h t ⟨ht ▸ hc.1.sdiff_of_sup_edge, hc.2⟩

Premises used: SimpleGraph.IsNClique.card_eq, Eq.rec, SimpleGraph.IsNClique.isClique, SimpleGraph.IsClique.sdiff_of_sup_edge, SimpleGraph.IsNClique.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
h : G.CliqueFree n
v w : α
⊢ (G ⊔ edge v w).CliqueFree (n + 1)

Tactic:
fun _ hs ↦ (hs.erase_of_sup_edge_of_mem <|
    (h.mono n.le_succ).mem_of_sup_edge_isNClique hs).not_cliqueFree h

Premises used: SimpleGraph.IsNClique.erase_of_sup_edge_of_mem, Nat.le_succ, SimpleGraph.CliqueFree.mem_of_sup_edge_isNClique, SimpleGraph.CliqueFree, SimpleGraph.CliqueFree.mono, SimpleGraph.IsNClique.not_cliqueFree, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hc : G.IsNClique n s
h : G.CliqueFree (n + 1)
x : α
by_contra! : ∀ (hf : ∀ (y : α) (_ : y ∈ s), G.Adj x y), False
⊢ ∃ y ∈ s, ¬G.Adj x y

Tactic:
by_contra! hf
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hc : G.IsNClique n s
h : G.CliqueFree (n + 1)
x : α
hf : ∀ (y : α) (_ : y ∈ s), G.Adj x y
⊢ False

Tactic:
(hc.insert hf).not_cliqueFree h

Premises used: SimpleGraph.IsNClique.insert, SimpleGraph.IsNClique.not_cliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hc : G.IsNClique n s
h : G.CliqueFree (n + 1)
x : α
hf : ∀ (y : α) (_ : y ∈ s), G.Adj x y
⊢ False

Tactic:
exact (hc.insert hf).not_cliqueFree h

Premises used: SimpleGraph.IsNClique.insert, SimpleGraph.IsNClique.not_cliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
hc : G.IsNClique n s
h : G.CliqueFree (n + 1)
x : α
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∃ y ∈ s, ¬G.Adj x y) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ :
  ∀ (hf : ∀ (y : α) (_ : y ∈ s), G.Adj x y), False
⊢ ∃ y ∈ s, ¬G.Adj x y

Tactic:
classical
  by_contra! hf
  exact (hc.insert hf).not_cliqueFree h
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
obtain :
  ∀ (t : Finset α) (hc : (G ⊔ edge x y).IsNClique (n + 1) t),
    ∃ (s : Finset α), x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)
⊢ ∃ (s : Finset α), x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)

Tactic:
obtain ⟨t, hc⟩ := not_forall_not.1 <| h.not_prop_of_gt <| G.lt_sup_edge _ _ hne hn

Premises used: not_forall_not, SimpleGraph.lt_sup_edge, Maximal.not_prop_of_gt, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
right : G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))
⊢ ∃ (s : Finset α), x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)

Tactic:
use (t.erase x).erase y, erase_right_comm (a := x) ▸ (notMem_erase _ _), notMem_erase _ _

Premises used: Finset.notMem_erase, Finset.erase
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
⊢ x ∈ t

Tactic:
have h1 := h.1.mem_of_sup_edge_isNClique hc
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
⊢ y ∈ t

Tactic:
have h2 := h.1.mem_of_sup_edge_isNClique (edge_comm .. ▸ hc)
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
right : G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))

Tactic:
rw [insert_erase <| mem_erase_of_ne_of_mem hne.symm h2, erase_right_comm,
      insert_erase <| mem_erase_of_ne_of_mem hne h1]

Premises used: Finset.mem_erase_of_ne_of_mem, Ne.symm, Finset.erase_right_comm, Finset.insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)

Tactic:
⟨(edge_comm .. ▸ hc).erase_of_sup_edge_of_mem h2, hc.erase_of_sup_edge_of_mem h1⟩

Premises used: SimpleGraph.IsNClique.erase_of_sup_edge_of_mem, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
h2 : y ∈ t
⊢ G.IsNClique n (t.erase y) ∧ G.IsNClique n (t.erase x)

Tactic:
exact ⟨(edge_comm .. ▸ hc).erase_of_sup_edge_of_mem h2, hc.erase_of_sup_edge_of_mem h1⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s₁ s₂ : Set α
n : ℕ
hs : s₁ ⊆ s₂
h₂ : G.CliqueFreeOn s₂ n
⊢ G.CliqueFreeOn s₁ n

Tactic:
fun _t hts => h₂ <| hts.trans hs

Premises used: HasSubset.Subset.trans, SimpleGraph.CliqueFreeOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : (↑t : Set α) ⊆ s
ht : G.IsNClique n t
obtain : ∀ (u : Finset α) (hut : u ⊆ t) (hu : #u = m), False
⊢ False

Tactic:
obtain ⟨u, hut, hu⟩ := exists_subset_card_eq (hmn.trans ht.card_eq.ge)

Premises used: Eq.ge, SimpleGraph.IsNClique.card_eq, Finset.exists_subset_card_eq, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : (↑t : Set α) ⊆ s
ht : G.IsNClique n t
u : Finset α
hut : u ⊆ t
hu : #u = m
⊢ False

Tactic:
hG ((coe_subset.2 hut).trans hts) ⟨ht.isClique.subset hut, hu⟩

Premises used: Iff.mpr, HasSubset.Subset.trans, SimpleGraph.IsNClique.isClique, SimpleGraph.IsNClique.mk, SimpleGraph.IsClique.subset, Finset.coe_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
m n : ℕ
hmn : m ≤ n
hG : G.CliqueFreeOn s m
t : Finset α
hts : (↑t : Set α) ⊆ s
ht : G.IsNClique n t
u : Finset α
hut : u ⊆ t
hu : #u = m
⊢ False

Tactic:
exact hG ((coe_subset.2 hut).trans hts) ⟨ht.isClique.subset hut, hu⟩

Premises used: Iff.mpr, HasSubset.Subset.trans, SimpleGraph.IsNClique.isClique, SimpleGraph.IsNClique.mk, SimpleGraph.IsClique.subset, Finset.coe_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
s : Set α
n : ℕ
hGH : G ≤ H
hH : H.CliqueFreeOn s n
⊢ G.CliqueFreeOn s n

Tactic:
fun _t hts ht => hH hts <| ht.mono hGH

Premises used: SimpleGraph.IsNClique.mono, SimpleGraph.CliqueFreeOn, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFreeOn ∅ n ↔ n ≠ 0

Tactic:
simp [CliqueFreeOn, Set.subset_empty_iff]

Premises used: SimpleGraph.CliqueFreeOn, Set.subset_empty_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
zero : G.CliqueFreeOn {a} 0 ↔ LT.lt (α := ℕ) 1 0
succ : G.CliqueFreeOn {a} (HAdd.hAdd (α := ℕ) 0 1) ↔ 1 < HAdd.hAdd (α := ℕ) 0 1
succ₁ : ∀ (n : ℕ), G.CliqueFreeOn {a} (n + 1 + 1) ↔ 1 < n + 1 + 1
⊢ G.CliqueFreeOn {a} n ↔ 1 < n

Tactic:
obtain _ | _ | n := n
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} 0 ↔ LT.lt (α := ℕ) 1 0

Tactic:
simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

Premises used: Ne.symm, SimpleGraph.CliqueFreeOn, Nat.succ_ne_zero, Finset.subset_singleton_iff', SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.CliqueFreeOn {a} (HAdd.hAdd (α := ℕ) 0 1) ↔ 1 < HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

Premises used: Ne.symm, SimpleGraph.CliqueFreeOn, Nat.succ_ne_zero, Finset.subset_singleton_iff', SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} (n + 1 + 1) ↔ 1 < n + 1 + 1

Tactic:
simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

Premises used: Ne.symm, SimpleGraph.CliqueFreeOn, Nat.succ_ne_zero, Finset.subset_singleton_iff', SimpleGraph.isNClique_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFreeOn Set.univ n ↔ G.CliqueFree n

Tactic:
simp [CliqueFree, CliqueFreeOn]

Premises used: SimpleGraph.CliqueFreeOn, SimpleGraph.CliqueFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
n : ℕ
hG : G.CliqueFree n
⊢ G.CliqueFreeOn s n

Tactic:
fun _t _ ↦ hG _

Premises used: SimpleGraph.CliqueFreeOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
h : #s < n
⊢ G.CliqueFreeOn (↑s : Set α) n

Tactic:
fun _t hts ht => h.not_ge <| ht.2.symm.trans_le <| card_mono hts

Premises used: SimpleGraph.IsNClique.card_eq, Eq.trans_le, SimpleGraph.CliqueFreeOn, LT.lt.not_ge, Eq.symm, Not, Finset.card_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h_1 : a ≠ b
hab : G.Adj a b
⊢ G.IsClique (↑{a, b} : Set α)

Tactic:
simpa [hab.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_1 :
  ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s),
    a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
refine_2 : s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ

Tactic:
refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h_1 : a ≠ b
hab : G.Adj a b
refine_1 : {a, b} ⊆ s
⊢ (↑{a, b} : Set α) ⊆ s

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h_1 : a ≠ b
hab : G.Adj a b
⊢ {a, b} ⊆ s

Tactic:
Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.insert_subset_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : G.CliqueFreeOn s 2
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h_1 : a ≠ b
hab : G.Adj a b
⊢ {a, b} ⊆ s

Tactic:
exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.insert_subset_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_2 :
  s.Pairwise G.Adjᶜ →
    ∀ ⦃t : Finset α⦄, (↑t : Set α) ⊆ s → G.IsClique (↑t : Set α) → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}
⊢ s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2

Tactic:
simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]

Premises used: not_exists, Finset.card_eq_two, SimpleGraph.CliqueFreeOn, SimpleGraph.isNClique_iff, not_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
hst : (↑{a, b} : Set α) ⊆ s
ht : G.IsClique (↑{a, b} : Set α)
⊢ a ∈ s ∧ b ∈ s

Tactic:
simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst

Premises used: Set.singleton_subset_iff, Finset.coe_singleton, Set.insert_subset_iff, Finset.coe_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique (↑{a, b} : Set α)
hst : a ∈ s ∧ b ∈ s
⊢ False

Tactic:
h hst.1 hst.2 hab (ht ?_ ?_ hab)

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique (↑{a, b} : Set α)
hst : a ∈ s ∧ b ∈ s
refine_2 : a ∈ (↑{a, b} : Set α)
refine_2₁ : b ∈ (↑{a, b} : Set α)
⊢ False

Tactic:
refine h hst.1 hst.2 hab (ht ?_ ?_ hab)

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique (↑{a, b} : Set α)
hst : a ∈ s ∧ b ∈ s
⊢ a ∈ (↑{a, b} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
h : s.Pairwise G.Adjᶜ
a b : α
hab : a ≠ b
ht : G.IsClique (↑{a, b} : Set α)
hst : a ∈ s ∧ b ∈ s
⊢ b ∈ (↑{a, b} : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
refine_1 :
  ∀ (h : G.CliqueFreeOn s 2) (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ s),
    a ≠ b → ∀ (hab : G.Adj a b), (↑{a, b} : Set α) ⊆ s
refine_2 refine_2₁ : s.Pairwise G.Adjᶜ → G.CliqueFreeOn s 2
refine_2₂ :
  s.Pairwise G.Adjᶜ →
    ∀ ⦃t : Finset α⦄, (↑t : Set α) ⊆ s → G.IsClique (↑t : Set α) → ∀ (x x_1 : α), x ≠ x_1 → ¬t = {x, x_1}
refine_2₃ :
  ∀ (h : s.Pairwise G.Adjᶜ) (a b : α) (hab : a ≠ b) (hst : (↑{a, b} : Set α) ⊆ s) (ht : G.IsClique (↑{a, b} : Set α)),
    False
refine_2₄ :
  ∀ (h : s.Pairwise G.Adjᶜ) (a b : α) (hab : a ≠ b) (ht : G.IsClique (↑{a, b} : Set α)) (hst : a ∈ s ∧ b ∈ s), False
⊢ G.CliqueFreeOn s 2 ↔ s.Pairwise G.Adjᶜ

Tactic:
classical
  refine ⟨fun h a ha b hb _ hab => h ?_ ⟨by simpa [hab.ne], card_pair hab.ne⟩, ?_⟩
  · push_cast
    exact Set.insert_subset_iff.2 ⟨ha, Set.singleton_subset_iff.2 hb⟩
  simp only [CliqueFreeOn, isNClique_iff, card_eq_two, not_and, not_exists]
  rintro h t hst ht a b hab rfl
  simp only [coe_insert, coe_singleton, Set.insert_subset_iff, Set.singleton_subset_iff] at hst
  refine h hst.1 hst.2 hab (ht ?_ ?_ hab) <;> simp

Premises used: Set.singleton_subset_iff, Finset.coe_singleton, not_exists, Finset.card_eq_two, Set.insert_subset_iff, SimpleGraph.CliqueFreeOn, SimpleGraph.isNClique_iff, Finset.coe_insert, not_and, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n

Tactic:
fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)

Premises used: SimpleGraph.CliqueFreeOn, And.right, SimpleGraph.IsNClique.insert, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
refine : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a) (ht : G.IsNClique n t), (↑(insert a t) : Set α) ⊆ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n

Tactic:
refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
push_cast : insert a (↑t : Set α) ⊆ s
⊢ (↑(insert a t) : Set α) ⊆ s

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ insert a (↑t : Set α) ⊆ s

Tactic:
Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.inter_subset_left, Set.insert_subset_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ insert a (↑t : Set α) ⊆ s

Tactic:
exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩

Premises used: Iff.mpr, HasSubset.Subset.trans, Set.inter_subset_left, Set.insert_subset_iff, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
refine : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a) (ht : G.IsNClique n t), (↑(insert a t) : Set α) ⊆ s
refine₁ : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s ∩ G.neighborSet a) (ht : G.IsNClique n t), insert a (↑t : Set α) ⊆ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n

Tactic:
classical
  refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
  push_cast
  exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
⊢ s ∈ G.cliqueSet n ↔ G.IsNClique n s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.cliqueSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ
simp_rw : G.cliqueSet n = ∅ ↔ ∀ (t : Finset α), ¬G.IsNClique n t
simp_rw₁ : (∀ (x : Finset α), x ∉ G.cliqueSet n) ↔ ∀ (t : Finset α), ¬G.IsNClique n t
⊢ G.cliqueSet n = ∅ ↔ G.CliqueFree n

Tactic:
simp_rw [CliqueFree, Set.eq_empty_iff_forall_notMem, mem_cliqueSet_iff]

Premises used: Set.eq_empty_iff_forall_notMem, SimpleGraph.CliqueFree, SimpleGraph.mem_cliqueSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
n : ℕ
h : G ≤ H
⊢ G.cliqueSet n ⊆ H.cliqueSet n

Tactic:
fun _ ↦ IsNClique.mono h

Premises used: SimpleGraph.IsNClique.mono, Set.Mem, setOf, Set.Subset, SimpleGraph.cliqueSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G H : SimpleGraph α
h : G ≤ H
⊢ G.cliqueSet ≤ H.cliqueSet

Tactic:
fun _ ↦ cliqueSet_mono h

Premises used: SimpleGraph.cliqueSet_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s ∈ G.cliqueSet 0 ↔ Membership.mem (γ := Set (Finset α)) {∅} s

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s ∈ G.cliqueSet 1 ↔ Membership.mem (γ := Set (Finset α)) (Set.range singleton) s

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
n : ℕ
hn : 1 < n
⊢ Eq.{u_1 + 1} (α := Set (Finset α)) (cliqueSet ⊥ n) ∅

Tactic:
(cliqueFree_bot hn).cliqueSet

Premises used: SimpleGraph.cliqueFree_bot, SimpleGraph.CliqueFree.cliqueSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
h :
  ∀ (s : Finset β),
    Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s ↔
      s ∈ map f '' G.cliqueSet n
⊢ cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n = map f '' G.cliqueSet n

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
n : ℕ
hn : n ≠ 1
G : SimpleGraph α
f : α ↪ β
s : Finset β
h :
  Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s →
    s ∈ map f '' G.cliqueSet n
h₁ :
  s ∈ map f '' G.cliqueSet n →
    Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s
⊢ Membership.mem (γ := Set (Finset β)) (cliqueSet (SimpleGraph.map (⇑f : (a : α) → β) G) n) s ↔
    s ∈ map f '' G.cliqueSet n

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
rw : ∀ x ∈ s, Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x
⊢ map f (s.preimage (⇑f : (a : α) → β) ⋯) = s

Tactic:
rw [map_eq_image, image_preimage, filter_true_of_mem]

Premises used: Finset.filter_true_of_mem, Finset.image_preimage, Finset.map_eq_image
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
a : β
ha : a ∈ s
obtain :
  ∀ (b : β) (hb : b ∈ s) (hba : b ≠ a),
    Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a

Tactic:
obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a

Premises used: Iff.mpr, Finset.exists_mem_ne, Exists.intro, Finset.card_pos, Ne.lt_of_le'
-- Module: Mathlib.Combinatorics.SimpleGraph.Clique
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset β
hs : IsClique (SimpleGraph.map (⇑f : (a : α) → β) G) (↑s : Set β)
hn : #s ≠ 1
a : β
ha : a ∈ s
b : β
hb : b ∈ s
hba : b ≠ a
obtain :
  ∀ (c w : α),
    G.Adj c w →
      ∀ (hc : (f : (a : α) → β) c = a),
        (f : (a : α) → β) w = b → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
⊢ Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a

Tactic:
obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm

Premises used: Ne.symm