awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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')
⊢ 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' ⋯))
have 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 sorry))
  (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' sorry))
Tactic: rw [← hu hv, ← hu hv']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finsubgraph (goal)
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')
⊢ 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' ⋯))
have 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 sorry)
  (Subtype.mk (p := fun (x : V) ↦ x ∈ (↑(Opposite.unop (Opposite.op (finsubgraphOfAdj e))) : G.Subgraph).verts) v' sorry)
Tactic: apply Hom.map_adj (u _) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ G.IsNClique (r + 1) (insert b (insert a s))
have apply : ∀ (b_1 : α) (hb : b_1 ∈ insert a s), G.Adj b b_1
Tactic: apply h1.insert (fun b hb ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ G.Adj b_1 b
have inl : ∀ (h1 : G.IsNClique r (insert b s)) (ha : G.Adj b b_1) (hb : b ∈ insert b s), G.Adj b_1 b
Tactic: obtain (rfl | h) := mem_insert.1 hb
Cleared hypotheses: a, h1, ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ G.Adj b_1 b
have inr : ∀ (h : b ∈ s), G.Adj b_1 b
Tactic: obtain (rfl | h) := mem_insert.1 hb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ G.IsNClique r (insert a (insert b (s.erase c)))
have rw : G.IsNClique r (insert b ((insert a s).erase c))
Tactic: rw [insert_comm, ← erase_insert_of_ne (fun h : a = c ↦ ha (h ▸ hc) |>.elim)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ G.IsNClique r (insert b ((insert a s).erase c))
have hd₁ : ∀ w ∈ insert a s, w ∉ {c} → G.Adj b w
Tactic: simp_rw [adj_comm, ← notMem_singleton] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t
have 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
Tactic: obtain ⟨v, w₁, w₂, p3⟩ := exists_isPathGraph3Compl_of_not_isCompleteMultipartite hnc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₂
⊢ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t
have 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
Tactic: obtain ⟨s, h1, h2, h3, h4⟩ := exists_of_maximal_cliqueFree_not_adj h p3.ne_fst p3.not_adj_fst
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
⊢ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r (#(s ∩ t)) v w₁ w₂ s t
have 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
Tactic: obtain ⟨t, h5, h6, h7, h8⟩ := exists_of_maximal_cliqueFree_not_adj h p3.ne_snd p3.not_adj_snd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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))
⊢ False
have h : 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])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ False
have this : 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])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ False
have 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
Tactic: obtain ⟨x, hx, hcx⟩ := h (a := C v) trivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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))
⊢ False
have 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
Tactic: obtain ⟨y, hy, hcy⟩ := this (a := C v) trivial
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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))
⊢ False
have 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
Tactic: rw [coe_insert] at *
Cleared hypotheses: h, this, x, hx, hcx, y, hy, hcy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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₂
⊢ False
have h₁ : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert x (↑s : Set α)) Set.univ
Tactic: subst_vars
Cleared hypotheses: w₁, w₂, hw, h, this, hx, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ False
have this₁ : Set.SurjOn (β := Fin (r + 1)) (⇑C : (a : α) → Fin (r + 1)) (insert y (↑t : Set α)) Set.univ
Tactic: subst_vars
Cleared hypotheses: w₁, w₂, hw, h, this, hx, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ False
have hw₁ : G.IsFiveWheelLike r k v x y s t
Tactic: subst_vars
Cleared hypotheses: w₁, w₂, hw, h, this, hx, hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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 α)
⊢ False
have apply : G.Adj v y
Tactic: apply (C.valid _ hcy.symm).elim
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
⊢ False
have inl : ∀ (hy : y = w₂), 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)
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ False
have inl₁ : ∀ (hy : y ∈ (↑t : Set α)), 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)
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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 α)
⊢ False
have apply : G.Adj v x
Tactic: apply (C.valid _ hcx.symm).elim
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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))
⊢ False
have inl : ∀ (hx : x = w₁), 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)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ False
have inr : ∀ (hx : x ∈ (↑s : Set α)), 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)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
⊢ k < r
have contrapose! : ∀ (h : r ≤ k), ¬G.CliqueFree (r + 2)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ¬G.CliqueFree (r + 2)
have hs : s ∩ t = s
Tactic: have hs := eq_of_subset_of_card_le inter_subset_left (hw.card_inter ▸ hw.card_left ▸ h)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ¬G.CliqueFree (r + 2)
have this : s ∩ t = t
Tactic: have := eq_of_subset_of_card_le inter_subset_right (hw.card_inter ▸ hw.card_right ▸ h)