awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert v (insert x (s.erase a)))

Tactic:
case h5 => exact hw.isNClique_left.insert_insert_erase has hw.notMem_left fun _ hz hZ ↦
               wa ((insert_subset_insert _ fun _ hx ↦ (by simp [hx])) hz) hZ
                 fun h ↦ hbv <| (mem_insert.1 (h ▸ hz)).resolve_right hbs

Premises used: Finset.insert_subset_insert, Finset.mem_insert, SimpleGraph.IsFiveWheelLike.notMem_left, SimpleGraph.IsFiveWheelLike.isNClique_left, Iff.mp, Or.resolve_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₁ (insert x (s.erase a)))

Tactic:
hw.isNClique_fst_left.insert_insert_erase has hw.fst_notMem fun _ hz hZ ↦
               wa (h1s hz) hZ fun h ↦ hbw <| (mem_insert.1 (h ▸ hz)).resolve_right hbs

Premises used: Finset.mem_insert, SimpleGraph.IsFiveWheelLike.fst_notMem, SimpleGraph.IsFiveWheelLike.isNClique_fst_left, Iff.mp, Or.resolve_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₁ (insert x (s.erase a)))

Tactic:
exact hw.isNClique_fst_left.insert_insert_erase has hw.fst_notMem fun _ hz hZ ↦
               wa (h1s hz) hZ fun h ↦ hbw <| (mem_insert.1 (h ▸ hz)).resolve_right hbs

Premises used: Finset.mem_insert, SimpleGraph.IsFiveWheelLike.fst_notMem, SimpleGraph.IsFiveWheelLike.isNClique_fst_left, Iff.mp, Or.resolve_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₁ (insert x (s.erase a)))

Tactic:
case h6 => exact hw.isNClique_fst_left.insert_insert_erase has hw.fst_notMem fun _ hz hZ ↦
               wa (h1s hz) hZ fun h ↦ hbw <| (mem_insert.1 (h ▸ hz)).resolve_right hbs

Premises used: Finset.mem_insert, SimpleGraph.IsFiveWheelLike.fst_notMem, SimpleGraph.IsFiveWheelLike.isNClique_fst_left, Iff.mp, Or.resolve_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
x_1 : α
hz : x_1 ∈ insert v t
hZ : x_1 ≠ b
x_2 : α
hx : x_2 ∈ t
⊢ x_2 ∈ {w₁} ∪ ({w₂} ∪ (s ∪ t))

Tactic:
simp [hx]
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert v (insert x (t.erase b)))

Tactic:
exact hw.isNClique_right.insert_insert_erase hbt hw.notMem_right fun _ hz hZ ↦
               wa ((insert_subset_insert _ fun _ hx ↦ (by simp [hx])) hz)
                 (fun h ↦ hav <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ

Premises used: Finset.insert_subset_insert, SimpleGraph.IsFiveWheelLike.isNClique_right, Finset.mem_insert, Iff.mp, Or.resolve_right, SimpleGraph.IsFiveWheelLike.notMem_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert v (insert x (t.erase b)))

Tactic:
case h7 => exact hw.isNClique_right.insert_insert_erase hbt hw.notMem_right fun _ hz hZ ↦
               wa ((insert_subset_insert _ fun _ hx ↦ (by simp [hx])) hz)
                 (fun h ↦ hav <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ

Premises used: Finset.insert_subset_insert, SimpleGraph.IsFiveWheelLike.isNClique_right, Finset.mem_insert, Iff.mp, Or.resolve_right, SimpleGraph.IsFiveWheelLike.notMem_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₂ (insert x (t.erase b)))

Tactic:
hw.isNClique_snd_right.insert_insert_erase hbt hw.snd_notMem fun _ hz hZ ↦
               wa (h2t hz) (fun h ↦ haw <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ

Premises used: SimpleGraph.IsFiveWheelLike.snd_notMem, SimpleGraph.IsFiveWheelLike.isNClique_snd_right, Finset.mem_insert, Iff.mp, Or.resolve_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₂ (insert x (t.erase b)))

Tactic:
exact hw.isNClique_snd_right.insert_insert_erase hbt hw.snd_notMem fun _ hz hZ ↦
               wa (h2t hz) (fun h ↦ haw <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ

Premises used: SimpleGraph.IsFiveWheelLike.snd_notMem, SimpleGraph.IsFiveWheelLike.isNClique_snd_right, Finset.mem_insert, Iff.mp, Or.resolve_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
⊢ G.IsNClique (r + 1) (insert w₂ (insert x (t.erase b)))

Tactic:
case h8 => exact hw.isNClique_snd_right.insert_insert_erase hbt hw.snd_notMem fun _ hz hZ ↦
               wa (h2t hz) (fun h ↦ haw <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ

Premises used: SimpleGraph.IsFiveWheelLike.snd_notMem, SimpleGraph.IsFiveWheelLike.isNClique_snd_right, Finset.mem_insert, Iff.mp, Or.resolve_right, _private.0.SimpleGraph.IsNClique.insert_insert_erase
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
rw : #(insert x (s.erase a ∩ t.erase b)) = k + 1
rw₁ : #(insert x ((s ∩ t.erase b).erase a)) = k + 1
rw₂ : #(insert x (((s ∩ t).erase b).erase a)) = k + 1
rw₃ : #(insert x ((s ∩ t).erase a)) = k + 1
rw₄ : #(insert x (s ∩ t)) = k + 1
rw₅ : #(s ∩ t) + 1 = k + 1
rw₆ rw₇ : k + 1 = k + 1
⊢ #(insert x (s.erase a) ∩ insert x (t.erase b)) = k + 1

Tactic:
rw [← insert_inter_distrib, erase_inter, inter_erase, erase_eq_of_notMem <|
        notMem_mono inter_subset_left hbs, erase_eq_of_notMem <| notMem_mono inter_subset_right hat,
        card_insert_of_notMem (fun h ↦ G.irrefl (hW h)), hw.card_inter]

Premises used: Finset.inter_erase, Finset.inter_subset_right, Finset.card_insert_of_notMem, SimpleGraph.IsFiveWheelLike.card_inter, Finset.insert_inter_distrib, SimpleGraph.irrefl, Finset.notMem_mono, Finset.erase_eq_of_notMem, Finset.erase_inter, Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
h2 : #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2
a b c d : α
haj : ¬G.Adj x a
hbj : ¬G.Adj x b
hab : a ≠ b
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hcj : ¬G.Adj x a
hbc : b ≠ a
hca : True
hdj : ¬G.Adj x b
had : a ≠ b
hdb : True
ha : a = w₁ ∨ a ∈ s
hb : b = w₂ ∨ b ∈ t
hc : a = v ∨ a ∈ s
hd : b = v ∨ b ∈ t
has : a ∈ s
hbt : b ∈ t
hav : a ≠ v
hbv : b ≠ v
haw : a ≠ w₂
hbw : b ≠ w₁
hxv : v ≠ x
hxw₁ : w₁ ≠ x
hxw₂ : w₂ ≠ x
wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
h1s : insert w₁ s ⊆ W
h2t : insert w₂ t ⊆ W
case : #(insert x (s.erase a ∩ t.erase b)) = k + 1
case₁ : #(insert x ((s ∩ t.erase b).erase a)) = k + 1
case₂ : #(insert x (((s ∩ t).erase b).erase a)) = k + 1
case₃ : #(insert x ((s ∩ t).erase a)) = k + 1
case₄ : #(insert x (s ∩ t)) = k + 1
case₅ : #(s ∩ t) + 1 = k + 1
case₆ case₇ : k + 1 = k + 1
⊢ #(insert x (s.erase a) ∩ insert x (t.erase b)) = k + 1

Tactic:
case h9 =>
    -- Finally check that this new `IsFiveWheelLike` structure has `k + 1` common clique
    -- vertices i.e. `#((insert x (s.erase a)) ∩ (insert x (s.erase b))) = k + 1`.
    rw [← insert_inter_distrib, erase_inter, inter_erase, erase_eq_of_notMem <|
        notMem_mono inter_subset_left hbs, erase_eq_of_notMem <| notMem_mono inter_subset_right hat,
        card_insert_of_notMem (fun h ↦ G.irrefl (hW h)), hw.card_inter]

Premises used: Finset.inter_erase, Finset.inter_subset_right, Finset.card_insert_of_notMem, SimpleGraph.IsFiveWheelLike.card_inter, Finset.insert_inter_distrib, SimpleGraph.irrefl, Finset.notMem_mono, Finset.erase_eq_of_notMem, Finset.erase_inter, Finset.inter_subset_left
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x : α
hx : x ∈ X
by_contra! : ∀ (h : #({z ∈ W | ¬G.Adj x z}) < 3), False
⊢ 3 ≤ #({z ∈ W | ¬G.Adj x z})

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x : α
hx : x ∈ X
h : #({z ∈ W | ¬G.Adj x z}) < 3
⊢ ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y

Tactic:
simpa [X] using hx
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x : α
hx : x ∈ X
h : #({z ∈ W | ¬G.Adj x z}) < 3
obtain : ∀ (w w_1 : α) (hW : G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase w)) (insert x (t.erase w_1))), False
⊢ False

Tactic:
obtain ⟨_, _, hW⟩ := hw.exists_isFiveWheelLike_succ_of_not_adj_le_two hcf
      (by simpa [X] using hx) <| Nat.le_of_succ_le_succ h

Premises used: SimpleGraph.IsFiveWheelLike.exists_isFiveWheelLike_succ_of_not_adj_le_two, Nat.le_of_succ_le_succ
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x : α
hx : x ∈ X
h : #({z ∈ W | ¬G.Adj x z}) < 3
w w_1 : α
hW : G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase w)) (insert x (t.erase w_1))
⊢ False

Tactic:
hm hW
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
x : α
hx : x ∈ X
h : #({z ∈ W | ¬G.Adj x z}) < 3
w w_1 : α
hW : G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase w)) (insert x (t.erase w_1))
⊢ False

Tactic:
exact hm hW
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
⊢ ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})

Tactic:
have dXle : ∀ x ∈ X, 3 ≤ #{z ∈ W | ¬ G.Adj x z} := by
    intro _ hx
    by_contra! h
    obtain ⟨_, _, hW⟩ := hw.exists_isFiveWheelLike_succ_of_not_adj_le_two hcf
      (by simpa [X] using hx) <| Nat.le_of_succ_le_succ h
    exact hm hW
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
x w : α
hz : w ∈ insert w₁ s ∧ ¬G.Adj x w
⊢ w ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
⊢ ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})

Tactic:
have one_le (x : α) : 1 ≤ #{z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬ G.Adj x z} :=
    let ⟨_, hz⟩ := hw.isNClique_fst_left.exists_not_adj_of_cliqueFree_succ hcf x
    card_pos.2 ⟨_, mem_filter.2 ⟨by grind, hz.2⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
⊢ ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)

Tactic:
have bdW := sum_degree_le_of_le_not_adj dXle (fun y _ ↦ one_le y)
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
x : α
hx : x ∈ Xᶜ
apply : {z ∈ s ∩ t | ¬G.Adj x z}.Nonempty
⊢ 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})

Tactic:
apply card_pos.2

Premises used: Iff.mpr, Finset.card_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
x : α
hx : x ∈ Xᶜ
contrapose! : ∀ (hx : ∀ (y : α) (_ : y ∈ s ∩ t), G.Adj x y), x ∉ Xᶜ
⊢ ∃ y ∈ s ∩ t, ¬G.Adj x y

Tactic:
contrapose! hx
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r k : ℕ
v w₁ w₂ : α
s t : Finset α
inst : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
inst_1 : DecidableRel G.Adj
inst_2 : Fintype α
hm : G.FiveWheelLikeFree r (k + 1)
X : Finset α := {x : α | ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y}
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
dXle : ∀ x ∈ X, 3 ≤ #({z ∈ W | ¬G.Adj x z})
one_le : ∀ (x : α), 1 ≤ #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
bdW : ∑ w ∈ W, G.degree w ≤ #X * (#W - 3) + #Xᶜ * (#W - 1)
x : α
hx : ∀ (y : α) (_ : y ∈ s ∩ t), G.Adj x y
⊢ x ∉ Xᶜ

Tactic:
simpa [X] using hx