awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have has : a ∈ s
Tactic: have ⟨has, hbt, hav, hbv, haw, hbw⟩ : a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁ := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hbt : b ∈ t
Tactic: have ⟨has, hbt, hav, hbv, haw, hbw⟩ : a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁ := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hav : a ≠ v
Tactic: have ⟨has, hbt, hav, hbv, haw, hbw⟩ : a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁ := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hbv : b ≠ v
Tactic: have ⟨has, hbt, hav, hbv, haw, hbw⟩ : a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁ := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have haw : a ≠ w₂
Tactic: have ⟨has, hbt, hav, hbv, haw, hbw⟩ : a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁ := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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₂
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hbw : b ≠ w₁
Tactic: have ⟨has, hbt, hav, hbv, haw, hbw⟩ : a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁ := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
⊢ v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x
have refine_1 : v ≠ x
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
refine_1 : v ≠ x
⊢ v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x
have refine_2 : w₁ ≠ x
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
refine_1 : v ≠ x
refine_2 : w₁ ≠ x
⊢ v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x
have refine_3 : w₂ ≠ x
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
⊢ v ≠ x
have pos : ∀ (hax : x = a), v ≠ x
Tactic: by_cases hax : x = a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
pos : ∀ (hax : x = a), v ≠ x
⊢ v ≠ x
have neg : ∀ (hax : ¬x = a), v ≠ x
Tactic: by_cases hax : x = a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
⊢ w₁ ≠ x
have pos : ∀ (hax : x = a), w₁ ≠ x
Tactic: by_cases hax : x = a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
pos : ∀ (hax : x = a), w₁ ≠ x
⊢ w₁ ≠ x
have neg : ∀ (hax : ¬x = a), w₁ ≠ x
Tactic: by_cases hax : x = a
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
⊢ w₂ ≠ x
have pos : ∀ (hbx : x = b), w₂ ≠ x
Tactic: by_cases hbx : x = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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₁
pos : ∀ (hbx : x = b), w₂ ≠ x
⊢ w₂ ≠ x
have neg : ∀ (hbx : ¬x = b), w₂ ≠ x
Tactic: by_cases hbx : x = b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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₁
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hxv : v ≠ x
Tactic: have ⟨hxv, hxw₁, hxw₂⟩ : v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x := by
    refine ⟨?_, ?_, ?_⟩
    · by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
    · by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_fst_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
    · by_cases hbx : x = b <;> rintro rfl
      · grind
      · exact hbj <| hw.isNClique_snd_right.1 (mem_insert_self ..) (mem_insert_of_mem hbt) hbx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hxw₁ : w₁ ≠ x
Tactic: have ⟨hxv, hxw₁, hxw₂⟩ : v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x := by
    refine ⟨?_, ?_, ?_⟩
    · by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
    · by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_fst_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
    · by_cases hbx : x = b <;> rintro rfl
      · grind
      · exact hbj <| hw.isNClique_snd_right.1 (mem_insert_self ..) (mem_insert_of_mem hbt) hbx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hxw₂ : w₂ ≠ x
Tactic: have ⟨hxv, hxw₁, hxw₂⟩ : v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x := by
    refine ⟨?_, ?_, ?_⟩
    · by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
    · by_cases hax : x = a <;> rintro rfl
      · grind
      · exact haj <| hw.isNClique_fst_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
    · by_cases hbx : x = b <;> rintro rfl
      · grind
      · exact hbj <| hw.isNClique_snd_right.1 (mem_insert_self ..) (mem_insert_of_mem hbt) hbx
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
w : α
hz : w ∈ W
haz : w ≠ a
hbz : w ≠ b
⊢ G.Adj w x
have by_contra! : ∀ (hf : ¬G.Adj w x), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
w : α
hz : w ∈ W
haz : w ≠ a
hbz : w ≠ b
hf : ¬G.Adj w x
⊢ False
have apply : 2 < #({z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z})
Tactic: apply h2.not_gt
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
w : α
hz : w ∈ W
haz : w ≠ a
hbz : w ≠ b
hf : ¬G.Adj w x
⊢ ¬G.Adj x w
have rwa : ∀ (hf : ¬G.Adj x w), ¬G.Adj x w
Tactic: rwa [adj_comm] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have wa : ∀ ⦃w : α⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x
Tactic: have wa : ∀ ⦃w⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x := by
    intro _ hz haz hbz
    by_contra! hf
    apply h2.not_gt
    exact two_lt_card.2 ⟨_, by simp [has, hcj], _, by simp [hbt, hdj], _,
                         mem_filter.2 ⟨hz, by rwa [adj_comm] at hf⟩, hab, haz.symm, hbz.symm⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have h1s : insert w₁ s ⊆ W
Tactic: have ⟨h1s, h2t⟩ : insert w₁ s ⊆ W ∧ insert w₂ t ⊆ W := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have h2t : insert w₂ t ⊆ W
Tactic: have ⟨h1s, h2t⟩ : insert w₁ s ⊆ W ∧ insert w₂ t ⊆ W := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have refine : G.IsNClique (r + 1) (insert v (insert x (s.erase a)))
Tactic: refine ⟨a, b, ⟨by grind, by grind, by grind, by grind, by grind, ?h5, ?h6, ?h7, ?h8, ?h9⟩⟩