awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (↑(insert w₁ s) : Set α) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (↑(insert w₂ t) : Set α) Set.univ
x : α
hx : x ∈ (↑(insert w₁ s) : Set α)
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
obtain :
  ∀ (y : α) (hy : y ∈ (↑(insert w₂ t) : Set α))
    (hcy :
      Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1))
        ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))),
    False
⊢ False

Tactic:
obtain ⟨y, hy, hcy⟩ := this (a := C v) trivial

Premises used: trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (↑(insert w₁ s) : Set α) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (↑(insert w₂ t) : Set α) Set.univ
x : α
hx : x ∈ (↑(insert w₁ s) : Set α)
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hy : y ∈ (↑(insert w₂ t) : Set α)
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
rw :
  ∀ (h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ)
    (this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ) (x : α)
    (hx : x ∈ insert w₁ (↑s : Set α))
    (hcx :
      Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1)))
    (y : α) (hy : y ∈ insert w₂ (↑t : Set α))
    (hcy :
      Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1))
        ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))),
    False
⊢ False

Tactic:
rw [coe_insert] at *

Premises used: Finset.coe_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
hy : y = w₂
⊢ Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert x (↑s : Set α)) Set.univ

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
hy : y = w₂
h₁ : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert x (↑s : Set α)) Set.univ
⊢ Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert y (↑t : Set α)) Set.univ

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
hy : y = w₂
h₁ : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert x (↑s : Set α)) Set.univ
this₁ : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert y (↑t : Set α)) Set.univ
⊢ G.IsFiveWheelLike r k v x y s t

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v : α
t : Finset α
C : G.Coloring (Fin (r + 1))
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert x (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert y (↑t : Set α)) Set.univ
hw : G.IsFiveWheelLike r k v x y s t
⊢ False

Tactic:
C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)

Premises used: Eq.rec, SimpleGraph.Coloring.valid, Eq.symm, SimpleGraph.IsFiveWheelLike.isPathGraph3Compl, SimpleGraph.IsPathGraph3Compl.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v : α
t : Finset α
C : G.Coloring (Fin (r + 1))
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert x (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert y (↑t : Set α)) Set.univ
hw : G.IsFiveWheelLike r k v x y s t
⊢ False

Tactic:
exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)

Premises used: Eq.rec, SimpleGraph.Coloring.valid, Eq.symm, SimpleGraph.IsFiveWheelLike.isPathGraph3Compl, SimpleGraph.IsPathGraph3Compl.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
hy : y ∈ (↑t : Set α)
apply : G.Adj v y
⊢ False

Tactic:
apply (C.valid _ hcy.symm).elim

Premises used: False.elim, SimpleGraph.Coloring.valid, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
hy : y ∈ (↑t : Set α)
⊢ v ∈ (↑(insert v t) : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
hy : y ∈ (↑t : Set α)
⊢ y ∈ (↑(insert v t) : Set α)

Tactic:
simp [hy]
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
hy : y ∈ (↑t : Set α)
⊢ G.Adj v y

Tactic:
exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hy : y ∈ insert w₂ (↑t : Set α)
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x = w₁
inl : ∀ (hy : y = w₂), False
inl₁ : ∀ (hy : y ∈ (↑t : Set α)), False
⊢ False

Tactic:
cases hy with
    | inl hy =>
    -- But this is a contradiction since `w₁` and `w₂` are adjacent.
      subst_vars; exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)
    | inr hy =>
      apply (C.valid _ hcy.symm).elim
      exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)

Premises used: False.elim, SimpleGraph.Coloring.valid, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hy : y ∈ insert w₂ (↑t : Set α)
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x ∈ (↑s : Set α)
apply : G.Adj v x
⊢ False

Tactic:
apply (C.valid _ hcx.symm).elim

Premises used: False.elim, SimpleGraph.Coloring.valid, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hy : y ∈ insert w₂ (↑t : Set α)
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x ∈ (↑s : Set α)
⊢ v ∈ (↑(insert v s) : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hy : y ∈ insert w₂ (↑t : Set α)
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x ∈ (↑s : Set α)
⊢ x ∈ (↑(insert v s) : Set α)

Tactic:
simp [hx]
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hy : y ∈ insert w₂ (↑t : Set α)
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
hx : x ∈ (↑s : Set α)
⊢ G.Adj v x

Tactic:
exact hw.isNClique_left.1 (by simp) (by simp [hx]) fun h ↦ hw.notMem_left (h ▸ hx)
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₁ (↑s : Set α)) Set.univ
this : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert w₂ (↑t : Set α)) Set.univ
x : α
hx : x ∈ insert w₁ (↑s : Set α)
hcx : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) x : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
y : α
hy : y ∈ insert w₂ (↑t : Set α)
hcy : Eq (α := Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) y : Fin (r + 1)) ((C : (a : α) → Fin (r + 1)) v : Fin (r + 1))
inl : ∀ (hx : x = w₁), False
inr : ∀ (hx : x ∈ (↑s : Set α)), False
⊢ False

Tactic:
cases hx with
  | inl hx =>
    cases hy with
    | inl hy =>
    -- But this is a contradiction since `w₁` and `w₂` are adjacent.
      subst_vars; exact C.valid hw.isPathGraph3Compl.adj (hcy ▸ hcx)
    | inr hy =>
      apply (C.valid _ hcy.symm).elim
      exact hw.isNClique_right.1 (by simp) (by simp [hy]) fun h ↦ hw.notMem_right (h ▸ hy)
  | inr hx =>
    apply (C.valid _ hcx.symm).elim
    exact hw.isNClique_left.1 (by simp) (by simp [hx]) fun h ↦ hw.notMem_left (h ▸ hx)

Premises used: False.elim, SimpleGraph.Coloring.valid, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ #s = r

Tactic:
simp [← Nat.succ_inj, ← hw.isNClique_left.2, hw.notMem_left]

Premises used: Nat.succ_inj, SimpleGraph.IsNClique.card_eq, SimpleGraph.IsFiveWheelLike.notMem_left, SimpleGraph.IsFiveWheelLike.isNClique_left
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ #t = r

Tactic:
hw.symm.card_left

Premises used: SimpleGraph.IsFiveWheelLike.symm, SimpleGraph.IsFiveWheelLike.card_left
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
h : G.CliqueFree (r + 2)
contrapose! : ∀ (h : r ≤ k), ¬G.CliqueFree (r + 2)
⊢ k < r

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
h : r ≤ k
⊢ s ∩ t = s

Tactic:
have hs := eq_of_subset_of_card_le inter_subset_left (hw.card_inter ▸ hw.card_left ▸ h)
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
h : r ≤ k
hs : s ∩ t = s
⊢ s ∩ t = t

Tactic:
have := eq_of_subset_of_card_le inter_subset_right (hw.card_inter ▸ hw.card_right ▸ h)
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
h : r ≤ k
hs : s ∩ t = s
this : s ∩ t = t
⊢ ¬G.CliqueFree (r + 2)

Tactic:
(hw.isNClique_fst_left.insert_insert (hs ▸ this.symm ▸ hw.isNClique_snd_right)
    hw.snd_notMem_left hw.isPathGraph3Compl.adj).not_cliqueFree

Premises used: _private.0.SimpleGraph.IsNClique.insert_insert, SimpleGraph.IsFiveWheelLike.snd_notMem_left, SimpleGraph.IsFiveWheelLike.isNClique_fst_left, SimpleGraph.IsNClique.not_cliqueFree, SimpleGraph.IsFiveWheelLike.isPathGraph3Compl, SimpleGraph.IsPathGraph3Compl.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
h : r ≤ k
hs : s ∩ t = s
this : s ∩ t = t
⊢ ¬G.CliqueFree (r + 2)

Tactic:
exact (hw.isNClique_fst_left.insert_insert (hs ▸ this.symm ▸ hw.isNClique_snd_right)
    hw.snd_notMem_left hw.isPathGraph3Compl.adj).not_cliqueFree

Premises used: _private.0.SimpleGraph.IsNClique.insert_insert, SimpleGraph.IsFiveWheelLike.snd_notMem_left, SimpleGraph.IsFiveWheelLike.isNClique_fst_left, SimpleGraph.IsNClique.not_cliqueFree, SimpleGraph.IsFiveWheelLike.isPathGraph3Compl, SimpleGraph.IsPathGraph3Compl.adj
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
obtain :
  ∀ (w w_1 w_2 : α) (s t : Finset α) (hw : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t),
    ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
      G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
obtain ⟨_, _, _, s, t, hw⟩ :=
    exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hnc

Premises used: SimpleGraph.exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w w_1 w_2 : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t
P : ℕ → Prop :=
  fun (k : ℕ) ↦ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ P #(s ∩ t)

Tactic:
have hk : P #(s ∩ t) := ⟨_, _, _, _, _, hw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w w_1 w_2 : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t
P : ℕ → Prop :=
  fun (k : ℕ) ↦ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t
hk : P #(s ∩ t)
obtain :
  ∀ (w w_3 w_4 : α) (w_5 w_6 : Finset α) (hw : G.IsFiveWheelLike r (Nat.findGreatest P r) w w_3 w_4 w_5 w_6),
    ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
      G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
obtain ⟨_, _, _, _, _, hw⟩ := Nat.findGreatest_spec (hw.card_inter_lt_of_cliqueFree h.1).le hk

Premises used: SimpleGraph.IsFiveWheelLike.card_inter_lt_of_cliqueFree, Nat.findGreatest_spec, LT.lt.le, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w w_1 w_2 : α
s t : Finset α
hw_1 : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t
P : ℕ → Prop :=
  fun (k : ℕ) ↦ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t
hk : P #(s ∩ t)
w_3 w_4 w_5 : α
w_6 w_7 : Finset α
hw : G.IsFiveWheelLike r (Nat.findGreatest P r) w_3 w_4 w_5 w_6 w_7
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
⟨_, _, _, _, _, _, hw, hw.card_inter_lt_of_cliqueFree h.1,
         fun _ hj _ _ _ _ _ hv ↦ hj.not_ge <| Nat.le_findGreatest
           (hv.card_inter_lt_of_cliqueFree h.1).le ⟨_, _, _, _, _, hv⟩⟩

Premises used: SimpleGraph.IsFiveWheelLike.card_inter_lt_of_cliqueFree, Nat.le_findGreatest, LT.lt.le, And.left, And.intro, Exists.intro, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w w_1 w_2 : α
s t : Finset α
hw_1 : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t
P : ℕ → Prop :=
  fun (k : ℕ) ↦ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t
hk : P #(s ∩ t)
w_3 w_4 w_5 : α
w_6 w_7 : Finset α
hw : G.IsFiveWheelLike r (Nat.findGreatest P r) w_3 w_4 w_5 w_6 w_7
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j

Tactic:
exact ⟨_, _, _, _, _, _, hw, hw.card_inter_lt_of_cliqueFree h.1,
         fun _ hj _ _ _ _ _ hv ↦ hj.not_ge <| Nat.le_findGreatest
           (hv.card_inter_lt_of_cliqueFree h.1).le ⟨_, _, _, _, _, hv⟩⟩