internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.sum_res_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
⊢ ∀ (i : α), i ∈ C → degRes G i B ≤ degRes G i A
Tactic:
intro i _
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ degRes G i B ≤ degRes G i A
Theorem: SimpleGraph.sum_res_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ degRes G i B ≤ degRes G i A
Tactic:
rw [degRes, degRes]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ card (nbhdRes G i B) ≤ card (nbhdRes G i A)
Theorem: SimpleGraph.sum_res_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ card (nbhdRes G i B) ≤ card (nbhdRes G i A)
Tactic:
apply card_le_of_subset _
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ nbhdRes G i B ⊆ nbhdRes G i A
Theorem: SimpleGraph.sum_res_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
⊢ nbhdRes G i B ⊆ nbhdRes G i A
Tactic:
intro x hx
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ nbhdRes G i B
⊢ x ∈ nbhdRes G i A
Theorem: SimpleGraph.sum_res_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ nbhdRes G i B
⊢ x ∈ nbhdRes G i A
Tactic:
rw [mem_res_nbhd_iff] at *
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ B ∧ x ∈ neighborFinset G i
⊢ x ∈ A ∧ x ∈ neighborFinset G i
Theorem: SimpleGraph.sum_res_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
i : α
a✝ : i ∈ C
x : α
hx : x ∈ B ∧ x ∈ neighborFinset G i
⊢ x ∈ A ∧ x ∈ neighborFinset G i
Tactic:
exact ⟨hB hx.1, hx.2⟩
Proof state after:
no goals
Theorem: SimpleGraph.pair_subset
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
⊢ {v, w} ⊆ A
Tactic:
intro x
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x ∈ {v, w} → x ∈ A
Theorem: SimpleGraph.pair_subset
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x ∈ {v, w} → x ∈ A
Tactic:
rw [mem_insert,mem_singleton]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x = v ∨ x = w → x ∈ A
Theorem: SimpleGraph.pair_subset
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
⊢ x = v ∨ x = w → x ∈ A
Tactic:
intro h
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = v ∨ x = w
⊢ x ∈ A
Theorem: SimpleGraph.pair_subset
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = v ∨ x = w
⊢ x ∈ A
Tactic:
cases h with
| inl h => exact h ▸ hv
| inr h => exact h ▸ hw
Proof state after:
no goals
Theorem: SimpleGraph.pair_subset
Proof state before:
case inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = v
⊢ x ∈ A
Tactic:
exact h ▸ hv
Proof state after:
no goals
Theorem: SimpleGraph.pair_subset
Proof state before:
case inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
hv : v ∈ A
hw : w ∈ A
x : α
h : x = w
⊢ x ∈ A
Tactic:
exact h ▸ hw
Proof state after:
no goals
Theorem: SimpleGraph.adj_is2Clique
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ IsNClique G 2 {a, b}
Tactic:
rw [isNClique_iff, coe_insert, coe_singleton, isClique_iff, Set.pairwise_pair_of_symmetric G.symm]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ (a ≠ b → Adj G a b) ∧ card {a, b} = 2
Theorem: SimpleGraph.adj_is2Clique
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ (a ≠ b → Adj G a b) ∧ card {a, b} = 2
Tactic:
exact ⟨fun _ => h, card_eq_two.2 ⟨a,b,G.ne_of_adj h,rfl⟩⟩
Proof state after:
no goals
Theorem: SimpleGraph.clique_free_card_lt
Proof 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]
Proof 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
Theorem: SimpleGraph.clique_free_card_lt
Proof 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
Proof 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
Theorem: SimpleGraph.clique_free_card_lt
Proof 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]
Proof 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)
Theorem: SimpleGraph.clique_free_card_lt
Proof 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
Proof 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
Theorem: SimpleGraph.clique_free_card_lt
Proof 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
Proof 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
Theorem: SimpleGraph.clique_free_card_lt
Proof 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)
Proof state after:
no goals
Theorem: SimpleGraph.clique_free_empty
Proof 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
Proof 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
Theorem: SimpleGraph.clique_free_empty
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ CliqueFree G s → CliqueFreeSet U s
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
⊢ ¬CliqueFreeSet U s → ¬CliqueFree G s
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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]
Proof 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
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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
Proof 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
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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
Proof 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
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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]
Proof 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
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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
Proof 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
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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
Proof 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
Theorem: SimpleGraph.cliqueFree_graph_imp_set
Proof 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⟩
Proof state after:
no goals
Theorem: SimpleGraph.two_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
⊢ ∀ (v : α), v ∈ A → degRes G v A = 0
Tactic:
intro v hv
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ degRes G v A = 0
Theorem: SimpleGraph.two_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ degRes G v A = 0
Tactic:
rw [degRes, card_eq_zero]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ nbhdRes G v A = ∅
Theorem: SimpleGraph.two_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ nbhdRes G v A = ∅
Tactic:
contrapose hA
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
⊢ ¬CliqueFreeSet A 2
Theorem: SimpleGraph.two_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
⊢ ¬CliqueFreeSet A 2
Tactic:
obtain ⟨w, hw⟩ := exists_mem_nempty G hA
Proof state after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬CliqueFreeSet A 2
Theorem: SimpleGraph.two_clique_free
Proof state before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬CliqueFreeSet A 2
Tactic:
rw [CliqueFreeSet]
Proof state after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬∀ (B : Finset α), B ⊆ A → ¬IsNClique G 2 B
Theorem: SimpleGraph.two_clique_free
Proof state before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ¬∀ (B : Finset α), B ⊆ A → ¬IsNClique G 2 B
Tactic:
push_neg
Proof state after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ∃ B, B ⊆ A ∧ IsNClique G 2 B
Theorem: SimpleGraph.two_clique_free
Proof state before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
v : α
hv : v ∈ A
hA : ¬nbhdRes G v A = ∅
w : α
hw : w ∈ A ∧ Adj G v w
⊢ ∃ B, B ⊆ A ∧ IsNClique G 2 B
Tactic:
exact ⟨{v, w}, pair_subset hv hw.1, adj_is2Clique hw.2⟩
Proof state after:
no goals
Theorem: SimpleGraph.isClique_insert
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
⊢ IsClique G (insert v ↑B)
Tactic:
intro x hx y hy hne
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x : α
hx : x ∈ insert v ↑B
y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
⊢ Adj G x y
Theorem: SimpleGraph.isClique_insert
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x : α
hx : x ∈ insert v ↑B
y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
⊢ Adj G x y
Tactic:
cases hx with
| inl hx => 
  cases hy with
  | inl hy => rw [hx,hy] at hne; contradiction
  | inr hy => 
    rw [hx]; 
    apply G.subset_res_nbhd hB hy
| inr hx => 
  cases hy with
  | inl hy => 
    rw [hy, G.adj_comm]
    apply G.subset_res_nbhd hB hx
  | inr hy => exact h hx hy hne
Proof state after:
no goals
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
hx : x = v
⊢ Adj G x y
Tactic:
cases hy with
| inl hy => rw [hx,hy] at hne; contradiction
| inr hy => 
  rw [hx]; 
  apply G.subset_res_nbhd hB hy
Proof state after:
no goals
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y = v
⊢ Adj G x y
Tactic:
rw [hx,hy] at hne
Proof state after:
case inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : v ≠ v
hx : x = v
hy : y = v
⊢ Adj G x y
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inl.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : v ≠ v
hx : x = v
hy : y = v
⊢ Adj G x y
Tactic:
contradiction
Proof state after:
no goals
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G x y
Tactic:
rw [hx]
Proof state after:
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G v y
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G v y
Tactic:
apply G.subset_res_nbhd hB hy
Proof state after:
no goals
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
hx : x ∈ ↑B
⊢ Adj G x y
Tactic:
cases hy with
| inl hy => 
  rw [hy, G.adj_comm]
  apply G.subset_res_nbhd hB hx
| inr hy => exact h hx hy hne
Proof state after:
no goals
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y = v
⊢ Adj G x y
Tactic:
rw [hy, G.adj_comm]
Proof state after:
case inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y = v
⊢ Adj G v x
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inr.inl
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y = v
⊢ Adj G v x
Tactic:
apply G.subset_res_nbhd hB hx
Proof state after:
no goals
Theorem: SimpleGraph.isClique_insert
Proof state before:
case inr.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x ∈ ↑B
hy : y ∈ ↑B
⊢ Adj G x y
Tactic:
exact h hx hy hne
Proof state after:
no goals
Theorem: SimpleGraph.isSuccClique
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ IsNClique G (t + 1) (insert v B)
Tactic:
constructor
Proof state after:
case clique
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ IsClique G ↑(insert v B)

case card_eq
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ card (insert v B) = t + 1
Theorem: SimpleGraph.isSuccClique
Proof state before:
case clique
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ IsClique G ↑(insert v B)
Tactic:
rw [coe_insert]
Proof state after:
case clique
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ IsClique G (insert v ↑B)
Theorem: SimpleGraph.isSuccClique
Proof state before:
case clique
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ IsClique G (insert v ↑B)
Tactic:
exact isClique_insert hv hB h.1
Proof state after:
no goals
Theorem: SimpleGraph.isSuccClique
Proof state before:
case card_eq
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ card (insert v B) = t + 1
Tactic:
rw [card_insert_of_not_mem,add_left_inj,h.2]
Proof state after:
case card_eq
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ ¬v ∈ B
Theorem: SimpleGraph.isSuccClique
Proof state before:
case card_eq
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
t : ℕ
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsNClique G t B
⊢ ¬v ∈ B
Tactic:
apply not_mem_mono hB (G.not_mem_res_nbhd v A)
Proof state after:
no goals