awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v v' : V
e : G.Adj v v'
intro :
  F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))
⊢ F.Adj
    ((fun (v : V) ↦
        RelHom.toFun (r := Adj (Subgraph.coe (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph)))
          (s := F.Adj) (u (Opposite.op (singletonFinsubgraph v)))
          (Subtype.mk (p := fun (x : V) ↦
            x ∈ Subgraph.verts (G := G) (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph)) v ⋯))
      v)
    ((fun (v : V) ↦
        RelHom.toFun (r := Adj (Subgraph.coe (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph)))
          (s := F.Adj) (u (Opposite.op (singletonFinsubgraph v)))
          (Subtype.mk (p := fun (x : V) ↦
            x ∈ Subgraph.verts (G := G) (↑(Opposite.unop (Opposite.op (singletonFinsubgraph v))) : G.Subgraph)) v ⋯))
      v')

Tactic:
simp only
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v v' : V
e : G.Adj v v'
intro :
  ∀ (hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)),
    F.Adj
      (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
        (u (Opposite.op (singletonFinsubgraph v)))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
      (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
        (u (Opposite.op (singletonFinsubgraph v')))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))
⊢ F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))

Tactic:
have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v v' : V
e : G.Adj v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
intro :
  ∀ (hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')),
    F.Adj
      (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
        (u (Opposite.op (singletonFinsubgraph v)))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
      (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
        (u (Opposite.op (singletonFinsubgraph v')))
        (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))
⊢ F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))

Tactic:
have hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v') :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_right)
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v v' : V
e : G.Adj v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
intro :
  F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.finsubgraphHomFunctor F).map hv) :
          (a : (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (finsubgraphOfAdj e)))) →
            (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (singletonFinsubgraph v))))
        (u (Opposite.op (finsubgraphOfAdj e))))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.finsubgraphHomFunctor F).map hv') :
          (a : (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (finsubgraphOfAdj e)))) →
            (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (singletonFinsubgraph v'))))
        (u (Opposite.op (finsubgraphOfAdj e))))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))
⊢ F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v)))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      (u (Opposite.op (singletonFinsubgraph v')))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))

Tactic:
rw [← hu hv, ← hu hv']
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v v' : V
e : G.Adj v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
apply :
  (↑(Opposite.unop (Opposite.op (finsubgraphOfAdj e))) : G.Subgraph).coe.Adj
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑(Opposite.unop (Opposite.op (finsubgraphOfAdj e))) : G.Subgraph).verts) v ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑(Opposite.unop (Opposite.op (finsubgraphOfAdj e))) : G.Subgraph).verts) v' ⋯)
⊢ F.Adj
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v) : G.Subgraph))) (s := F.Adj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.finsubgraphHomFunctor F).map hv) :
          (a : (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (finsubgraphOfAdj e)))) →
            (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (singletonFinsubgraph v))))
        (u (Opposite.op (finsubgraphOfAdj e))))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v) : G.Subgraph)) v ⋯))
    (RelHom.toFun (r := Adj (Subgraph.coe (↑(singletonFinsubgraph v') : G.Subgraph))) (s := F.Adj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.finsubgraphHomFunctor F).map hv') :
          (a : (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (finsubgraphOfAdj e)))) →
            (fun (X : Type (max u v)) ↦ X) ((G.finsubgraphHomFunctor F).obj (Opposite.op (singletonFinsubgraph v'))))
        (u (Opposite.op (finsubgraphOfAdj e))))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (↑(singletonFinsubgraph v') : G.Subgraph)) v' ⋯))

Tactic:
apply Hom.map_adj (u _) ?_

Premises used: SimpleGraph.Hom.map_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val : Fintype W
this_1 : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v v' : V
e : G.Adj v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
hv' : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v')
⊢ (↑(Opposite.unop (Opposite.op (finsubgraphOfAdj e))) : G.Subgraph).coe.Adj
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑(Opposite.unop (Opposite.op (finsubgraphOfAdj e))) : G.Subgraph).verts) v ⋯)
    (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑(Opposite.unop (Opposite.op (finsubgraphOfAdj e))) : G.Subgraph).verts) v' ⋯)

Tactic:
simp [finsubgraphOfAdj]

Premises used: SimpleGraph.finsubgraphOfAdj
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b s)
h3 : b ∉ s
ha : G.Adj a b
apply : ∀ (b_1 : α) (hb : b_1 ∈ insert a s), G.Adj b b_1
⊢ G.IsNClique (r + 1) (insert b (insert a s))

Tactic:
apply h1.insert (fun b hb ↦ ?_)

Premises used: SimpleGraph.IsNClique.insert
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b_1 : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b_1 s)
h3 : b_1 ∉ s
ha : G.Adj a b_1
b : α
hb : b ∈ insert a s
inl : ∀ (h1 : G.IsNClique r (insert b s)) (ha : G.Adj b b_1) (hb : b ∈ insert b s), G.Adj b_1 b
inr : ∀ (h : b ∈ s), G.Adj b_1 b
⊢ G.Adj b_1 b

Tactic:
obtain (rfl | h) := mem_insert.1 hb

Premises used: Finset.mem_insert, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
b_1 : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h2 : G.IsNClique r (insert b_1 s)
h3 : b_1 ∉ s
b : α
h1 : G.IsNClique r (insert b s)
ha : G.Adj b b_1
hb : b ∈ insert b s
⊢ G.Adj b_1 b

Tactic:
ha.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
b_1 : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h2 : G.IsNClique r (insert b_1 s)
h3 : b_1 ∉ s
b : α
h1 : G.IsNClique r (insert b s)
ha : G.Adj b b_1
hb : b ∈ insert b s
⊢ G.Adj b_1 b

Tactic:
exact ha.symm

Premises used: SimpleGraph.Adj.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b_1 : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b_1 s)
h3 : b_1 ∉ s
ha : G.Adj a b_1
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b_1 b

Tactic:
h2.1 (mem_insert_self _ s) (mem_insert_of_mem h) <| fun h' ↦ (h3 (h' ▸ h)).elim

Premises used: Finset.mem_insert_self, False.elim, Eq.rec, SimpleGraph.IsNClique.isClique, Finset.mem_insert_of_mem, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b_1 : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b_1 s)
h3 : b_1 ∉ s
ha : G.Adj a b_1
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b_1 b

Tactic:
exact h2.1 (mem_insert_self _ s) (mem_insert_of_mem h) <| fun h' ↦ (h3 (h' ▸ h)).elim

Premises used: Finset.mem_insert_self, SimpleGraph.IsNClique.isClique, Finset.mem_insert_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
rw : G.IsNClique r (insert b ((insert a s).erase c))
⊢ G.IsNClique r (insert a (insert b (s.erase c)))

Tactic:
rw [insert_comm, ← erase_insert_of_ne (fun h : a = c ↦ ha (h ▸ hc) |>.elim)]

Premises used: False.elim, Eq.rec, Finset.erase_insert_of_ne, Eq.symm, Finset.insert_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ ∀ w ∈ insert a s, w ∉ {c} → G.Adj b w

Tactic:
simp_rw [adj_comm, ← notMem_singleton] at hd

Premises used: Finset.notMem_singleton, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ∉ {c} → G.Adj b w
⊢ G.IsNClique r (insert b ((insert a s).erase c))

Tactic:
hs.insert_erase (fun _ h ↦ hd _ (mem_sdiff.1 h).1 (mem_sdiff.1 h).2) (mem_insert_of_mem hc)

Premises used: SimpleGraph.IsNClique.insert_erase, Finset.mem_sdiff, Finset.mem_insert_of_mem, And.right, And.left, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ∉ {c} → G.Adj b w
⊢ G.IsNClique r (insert b ((insert a s).erase c))

Tactic:
exact hs.insert_erase (fun _ h ↦ hd _ (mem_sdiff.1 h).1 (mem_sdiff.1 h).2) (mem_insert_of_mem hc)

Premises used: SimpleGraph.IsNClique.insert_erase, Finset.mem_sdiff, Finset.mem_insert_of_mem, And.right, And.left, Iff.mp
-- 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 :
  ∀ (v w₁ w₂ : α) (p3 : G.IsPathGraph3Compl v w₁ w₂),
    ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t
⊢ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t

Tactic:
obtain ⟨v, w₁, w₂, p3⟩ := exists_isPathGraph3Compl_of_not_isCompleteMultipartite hnc

Premises used: SimpleGraph.exists_isPathGraph3Compl_of_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
v w₁ w₂ : α
p3 : G.IsPathGraph3Compl v w₁ w₂
obtain :
  ∀ (s : Finset α) (h1 : v ∉ s) (h2 : w₁ ∉ s) (h3 : G.IsNClique (r + 1) (insert v s))
    (h4 : G.IsNClique (r + 1) (insert w₁ s)),
    ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t
⊢ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t

Tactic:
obtain ⟨s, h1, h2, h3, h4⟩ := exists_of_maximal_cliqueFree_not_adj h p3.ne_fst p3.not_adj_fst

Premises used: SimpleGraph.IsPathGraph3Compl.not_adj_fst, SimpleGraph.IsPathGraph3Compl.ne_fst, SimpleGraph.exists_of_maximal_cliqueFree_not_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
v w₁ w₂ : α
p3 : G.IsPathGraph3Compl v w₁ w₂
s : Finset α
h1 : v ∉ s
h2 : w₁ ∉ s
h3 : G.IsNClique (r + 1) (insert v s)
h4 : G.IsNClique (r + 1) (insert w₁ s)
obtain :
  ∀ (t : Finset α) (h5 : v ∉ t) (h6 : w₂ ∉ t) (h7 : G.IsNClique (r + 1) (insert v t))
    (h8 : G.IsNClique (r + 1) (insert w₂ t)),
    ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t
⊢ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t

Tactic:
obtain ⟨t, h5, h6, h7, h8⟩ := exists_of_maximal_cliqueFree_not_adj h p3.ne_snd p3.not_adj_snd

Premises used: SimpleGraph.IsPathGraph3Compl.ne_snd, SimpleGraph.IsPathGraph3Compl.not_adj_snd, SimpleGraph.exists_of_maximal_cliqueFree_not_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
v w₁ w₂ : α
p3 : G.IsPathGraph3Compl v w₁ w₂
s : Finset α
h1 : v ∉ s
h2 : w₁ ∉ s
h3 : G.IsNClique (r + 1) (insert v s)
h4 : G.IsNClique (r + 1) (insert w₁ s)
t : Finset α
h5 : v ∉ t
h6 : w₂ ∉ t
h7 : G.IsNClique (r + 1) (insert v t)
h8 : G.IsNClique (r + 1) (insert w₂ t)
⊢ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t

Tactic:
⟨_, _, _, _, _, p3, h1, h5, h2, h6, h3, h4, h7, h8, rfl⟩

Premises used: SimpleGraph.IsFiveWheelLike.mk, Exists.intro, rfl
-- 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
v w₁ w₂ : α
p3 : G.IsPathGraph3Compl v w₁ w₂
s : Finset α
h1 : v ∉ s
h2 : w₁ ∉ s
h3 : G.IsNClique (r + 1) (insert v s)
h4 : G.IsNClique (r + 1) (insert w₁ s)
t : Finset α
h5 : v ∉ t
h6 : w₂ ∉ t
h7 : G.IsNClique (r + 1) (insert v t)
h8 : G.IsNClique (r + 1) (insert w₂ t)
⊢ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t

Tactic:
exact ⟨_, _, _, _, _, p3, h1, h5, h2, h6, h3, h4, h7, h8, rfl⟩
-- 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
p2 : G.IsPathGraph3Compl v w₁ w₂
d1 : v ∉ s
d2 : v ∉ t
d3 : w₁ ∉ s
d4 : w₂ ∉ t
c1 : G.IsNClique (r + 1) (insert v s)
c2 : G.IsNClique (r + 1) (insert w₁ s)
c3 : G.IsNClique (r + 1) (insert v t)
c4 : G.IsNClique (r + 1) (insert w₂ t)
hk rwa rwa₁ rwa₂ rwa₃ : #(s ∩ t) = k
⊢ #(t ∩ s) = k

Tactic:
rwa [inter_comm]

Premises used: Finset.inter_comm
-- 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
⊢ w₁ ∉ t

Tactic:
fun h ↦ hw.isPathGraph3Compl.not_adj_fst <| hw.isNClique_right.1 (mem_insert_self ..)
    (mem_insert_of_mem h) hw.isPathGraph3Compl.ne_fst

Premises used: Finset.mem_insert_self, SimpleGraph.IsFiveWheelLike.isNClique_right, SimpleGraph.IsPathGraph3Compl.not_adj_fst, SimpleGraph.IsNClique.isClique, Finset.mem_insert_of_mem, SimpleGraph.IsPathGraph3Compl.ne_fst, Not, SimpleGraph.IsFiveWheelLike.isPathGraph3Compl
-- 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
⊢ w₂ ∉ s

Tactic:
hw.symm.fst_notMem_right

Premises used: SimpleGraph.IsFiveWheelLike.fst_notMem_right, SimpleGraph.IsFiveWheelLike.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))
⊢ ‖Fin (r + 1)‖ ≤ #(insert w₁ s)

Tactic:
simp [hw.isNClique_fst_left.2]

Premises used: SimpleGraph.IsNClique.card_eq, SimpleGraph.IsFiveWheelLike.isNClique_fst_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
C : G.Coloring (Fin (r + 1))
⊢ Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (↑(insert w₁ s) : Set α) Set.univ

Tactic:
have h := C.surjOn_of_card_le_isClique hw.isNClique_fst_left.1 (by simp [hw.isNClique_fst_left.2])
-- 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
⊢ ‖Fin (r + 1)‖ ≤ #(insert w₂ t)

Tactic:
simp [hw.isNClique_snd_right.2]

Premises used: SimpleGraph.IsNClique.card_eq, SimpleGraph.IsFiveWheelLike.isNClique_snd_right
-- 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
⊢ Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (↑(insert w₂ t) : Set α) Set.univ

Tactic:
have := C.surjOn_of_card_le_isClique hw.isNClique_snd_right.1 (by simp [hw.isNClique_snd_right.2])
-- 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
obtain :
  ∀ (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))),
    False
⊢ False

Tactic:
obtain ⟨x, hx, hcx⟩ := h (a := C v) trivial

Premises used: trivial