-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
/-- If `s` is an independent set, its complement meets every edge of `G`. -/
lemma IsIndepSet.nonempty_mem_compl_mem_edge
    [Fintype α] [DecidableEq α] {s : Finset α} (indA : G.IsIndepSet s) {e} (he : e ∈ G.edgeSet) :
    { b ∈ sᶜ | b ∈ e }.Nonempty

Proof state:
case neg
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∉ s
⊢ False

Tactic:
exact (c vins).left rfl

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : G.IsIndepSet ↑s
e : Sym2 α
he : e ∈ G.edgeSet
⊢ (filter (fun b => b ∈ e) sᶜ).Nonempty

Tactic:
obtain ⟨v , w⟩ := e

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : G.IsIndepSet ↑s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
⊢ (filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∈ s
wnins : w ∉ s
⊢ False

Tactic:
exact (c wnins).right rfl

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : G.IsIndepSet ↑s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : ¬(filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty
⊢ False

Tactic:
rw [IsIndepSet] at indA

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : ¬(filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty
⊢ False

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
⊢ False

Tactic:
by_cases vins : v ∈ s

Result:
case pos
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∈ s
⊢ False

case neg
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∉ s
⊢ False

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∈ sᶜ → x ∉ Quot.mk (Sym2.Rel α) (v, w)
⊢ False

Tactic:
simp_rw [mem_compl, Sym2.mem_iff, not_or] at c

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
⊢ False

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ¬(filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty
⊢ False

Tactic:
rw [not_nonempty_iff_eq_empty, filter_eq_empty_iff] at c

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∈ sᶜ → x ∉ Quot.mk (Sym2.Rel α) (v, w)
⊢ False

Proof state:
case pos
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∈ s
⊢ False

Tactic:
have wins : w ∈ s := by by_contra wnins; exact (c wnins).right rfl

Result:
case pos
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∈ s
wins : w ∈ s
⊢ False

Proof state:
case pos
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∈ s
wins : w ∈ s
⊢ False

Tactic:
exact (indA vins wins (Adj.ne he)) he

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : ¬(filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty
⊢ False

Tactic:
rw [mem_edgeSet] at he

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ¬(filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty
⊢ False

Proof state:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : G.IsIndepSet ↑s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
⊢ (filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty

Tactic:
by_contra c

Result:
case mk.mk
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : G.IsIndepSet ↑s
e : Sym2 α
v w : α
he : Quot.mk (Sym2.Rel α) (v, w) ∈ G.edgeSet
c : ¬(filter (fun b => b ∈ Quot.mk (Sym2.Rel α) (v, w)) sᶜ).Nonempty
⊢ False

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∈ s
⊢ w ∈ s

Tactic:
by_contra wnins

Result:
α : Type u_1
G : SimpleGraph α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
indA : (↑s).Pairwise fun v w => ¬G.Adj v w
e : Sym2 α
v w : α
he : G.Adj v w
c : ∀ ⦃x : α⦄, x ∉ s → ¬x = v ∧ ¬x = w
vins : v ∈ s
wnins : w ∉ s
⊢ False