awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
have obtain : ∀ (w w_1 w_2 : α) (s t : Finset α) (hw : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t),
  ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
Tactic: obtain ⟨_, _, _, s, t, hw⟩ :=
    exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hnc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : DecidableEq α
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 2)) G
hnc : ¬G.IsCompleteMultipartite
w w_1 w_2 : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t
P : ℕ → Prop :=
  fun (k : ℕ) ↦ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
have hk : P #(s ∩ t)
Tactic: have hk : P #(s ∩ t) := ⟨_, _, _, _, _, hw⟩
-- 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
w w_1 w_2 : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t
P : ℕ → Prop :=
  fun (k : ℕ) ↦ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t
hk : P #(s ∩ t)
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
have obtain : ∀ (w w_3 w_4 : α) (w_5 w_6 : Finset α) (hw : G.IsFiveWheelLike r (Nat.findGreatest P r) w w_3 w_4 w_5 w_6),
  ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
Tactic: obtain ⟨_, _, _, _, _, hw⟩ := Nat.findGreatest_spec (hw.card_inter_lt_of_cliqueFree h.1).le hk
-- 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
w w_1 w_2 : α
s t : Finset α
hw : G.IsFiveWheelLike r (#(s ∩ t)) w w_1 w_2 s t
P : ℕ → Prop :=
  fun (k : ℕ) ↦ ∃ (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α), G.IsFiveWheelLike r k v w₁ w₂ s t
hk : P #(s ∩ t)
⊢ ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
have obtain : ∀ (w w_3 w_4 : α) (w_5 w_6 : Finset α) (hw : G.IsFiveWheelLike r (Nat.findGreatest P r) w w_3 w_4 w_5 w_6),
  ∃ (k : ℕ) (v : α) (w₁ : α) (w₂ : α) (s : Finset α) (t : Finset α),
    G.IsFiveWheelLike r k v w₁ w₂ s t ∧ k < r ∧ ∀ (j : ℕ), k < j → G.FiveWheelLikeFree r j
Tactic: classical
  obtain ⟨_, _, _, _, _, hw⟩ := Nat.findGreatest_spec (hw.card_inter_lt_of_cliqueFree h.1).le hk
  exact ⟨_, _, _, _, _, _, hw, hw.card_inter_lt_of_cliqueFree h.1,
         fun _ hj _ _ _ _ _ hv ↦ hj.not_ge <| Nat.le_findGreatest
           (hv.card_inter_lt_of_cliqueFree h.1).le ⟨_, _, _, _, _, hv⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 r : ℕ
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 1 + 1)) G
⊢ G.Colorable (r + 1) ↔ G.IsCompleteMultipartite
have refine : ∀ (hc : G.Colorable (r + 1)), G.IsCompleteMultipartite
Tactic: refine ⟨fun hc ↦ ?_, fun hc ↦ hc.colorable_of_cliqueFree h.1⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 r : ℕ
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 1 + 1)) G
hc : G.Colorable (r + 1)
⊢ G.IsCompleteMultipartite
have contrapose : ∀ (hc : ¬G.IsCompleteMultipartite), ¬G.Colorable (r + 1)
Tactic: contrapose hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 r : ℕ
h : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 1 + 1)) G
hc : ¬G.IsCompleteMultipartite
⊢ ¬G.Colorable (r + 1)
have obtain : ∀ (w w_1 w_2 : α) (w_3 w_4 : Finset α) (hw : G.IsFiveWheelLike r (#(w_3 ∩ w_4)) w w_1 w_2 w_3 w_4), ¬G.Colorable (r + 1)
Tactic: obtain ⟨_, _, _, _, _, hw⟩ :=
      exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ Eq (α := ℕ) (∑ w ∈ W, G.degree w) (∑ v : α, #(G.neighborFinset v ∩ W))
have simp_rw : Eq (α := ℕ) (∑ x ∈ W, ∑ x ∈ G.neighborFinset x, 1) (∑ x : α, ∑ x ∈ G.neighborFinset x ∩ W, 1)
Tactic: simp_rw [degree, card_eq_sum_ones]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ ∑ v : α, #(G.neighborFinset v ∩ W) ≤ #X * (#W - i) + #Xᶜ * (#W - j)
have simp_rw : HAdd.hAdd (α := ℕ) (∑ x ∈ X, #({w ∈ W | G.Adj x w})) (∑ x ∈ Xᶜ, #({w ∈ W | G.Adj x w})) ≤
  HAdd.hAdd (α := ℕ) (∑ x ∈ X, (#W - i)) (∑ x ∈ Xᶜ, (#W - j))
Tactic: simp_rw [← union_compl X, sum_union disjoint_compl_right (s₁ := X), neighborFinset_eq_filter,
             filter_inter, univ_inter, card_eq_sum_ones X, card_eq_sum_ones Xᶜ, sum_mul, one_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
⊢ HAdd.hAdd (α := ℕ) (∑ x ∈ X, #({w ∈ W | G.Adj x w})) (∑ x ∈ Xᶜ, #({w ∈ W | G.Adj x w})) ≤
    HAdd.hAdd (α := ℕ) (∑ x ∈ X, (#W - i)) (∑ x ∈ Xᶜ, (#W - j))
have h₁ : ∀ i_1 ∈ X, #({w ∈ W | G.Adj i_1 w}) ≤ #W - i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
i j : ℕ
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableRel G.Adj
W X : Finset α
hx : ∀ x ∈ X, i ≤ #({z ∈ W | ¬G.Adj x z})
hxc : ∀ y ∈ Xᶜ, j ≤ #({z ∈ W | ¬G.Adj y z})
h₁ : ∀ i_1 ∈ X, #({w ∈ W | G.Adj i_1 w}) ≤ #W - i
⊢ HAdd.hAdd (α := ℕ) (∑ x ∈ X, #({w ∈ W | G.Adj x w})) (∑ x ∈ Xᶜ, #({w ∈ W | G.Adj x w})) ≤
    HAdd.hAdd (α := ℕ) (∑ x ∈ X, (#W - i)) (∑ x ∈ Xᶜ, (#W - j))
have h₂ : ∀ i ∈ Xᶜ, #({w ∈ W | G.Adj i w}) ≤ #W - j
Tactic: gcongr
-- 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)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
⊢ ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
have obtain : ∀ (a : α) (ha : a ∈ insert w₁ s) (haj : ¬G.Adj x a),
  ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
Tactic: obtain ⟨a, ha, haj⟩ := hw.isNClique_fst_left.exists_not_adj_of_cliqueFree_succ hcf x
-- 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)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
⊢ ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
have obtain : ∀ (b : α) (hb : b ∈ insert w₂ t) (hbj : ¬G.Adj x b),
  ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
Tactic: obtain ⟨b, hb, hbj⟩ := hw.isNClique_snd_right.exists_not_adj_of_cliqueFree_succ hcf x
-- 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)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
b : α
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
⊢ ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
have obtain : ∀ (c : α) (hc : c ∈ insert v s) (hcj : ¬G.Adj x c),
  ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
Tactic: obtain ⟨c, hc, hcj⟩ := hw.isNClique_left.exists_not_adj_of_cliqueFree_succ hcf x
-- 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)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
b : α
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
c : α
hc : c ∈ insert v s
hcj : ¬G.Adj x c
⊢ ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
have obtain : ∀ (d : α) (hd : d ∈ insert v t) (hdj : ¬G.Adj x d),
  ∃ (a : α) (b : α) (c : α) (d : α),
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s
Tactic: obtain ⟨d, hd, hdj⟩ := hw.isNClique_right.exists_not_adj_of_cliqueFree_succ hcf x
-- 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 : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have obtain : ∀ (a b c d : α) (ha : a ∈ insert w₁ s) (haj : ¬G.Adj x a) (hb : b ∈ insert w₂ t) (hbj : ¬G.Adj x b)
  (hc : c ∈ insert v s) (hcj : ¬G.Adj x c) (hd : d ∈ insert v t) (hdj : ¬G.Adj x d) (hab : a ≠ b) (had : a ≠ d)
  (hbc : b ≠ c) (hat : a ∉ t) (hbs : b ∉ s),
  ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
Tactic: obtain ⟨a, b, c, d, ha, haj, hb, hbj, hc, hcj, hd, hdj, hab, had, hbc, hat, hbs⟩ :=
    hw.exist_not_adj_of_adj_inter hcf hW
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
⊢ c = a ∧ d = b
have by_contra! : ∀ (hf : ∀ (_ : c = a), d ≠ b), 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : ∀ (_ : c = a), d ≠ b
⊢ False
have apply : ∃ (a : α) (b : α) (c : α),
  a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
    b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: apply h2.not_gt <| two_lt_card_iff.2 _
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : ∀ (_ : c = a), d ≠ b
⊢ ∃ (a : α) (b : α) (c : α),
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
have pos : ∀ (h : a = c),
  ∃ (a : α) (b : α) (c : α),
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: by_cases h : a = c
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hf : ∀ (_ : c = a), d ≠ b
pos :
  ∀ (h : a = c),
    ∃ (a : α) (b : α) (c : α),
      a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
          c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ ∃ (a : α) (b : α) (c : α),
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
have neg : ∀ (h : ¬a = c),
  ∃ (a : α) (b : α) (c : α),
    a ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
      b ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧
        c ∈ {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z} ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: by_cases h : a = c
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hca : c = a
Tactic: have ⟨hca, hdb⟩ : c = a ∧ d = b := by
    by_contra! hf
    apply h2.not_gt <| two_lt_card_iff.2 _
    by_cases h : a = c
    · exact ⟨a, b, d, by grind⟩
    · exact ⟨a, b, c, 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hdb : d = b
Tactic: have ⟨hca, hdb⟩ : c = a ∧ d = b := by
    by_contra! hf
    apply h2.not_gt <| two_lt_card_iff.2 _
    by_cases h : a = c
    · exact ⟨a, b, d, by grind⟩
    · exact ⟨a, b, c, 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
hcj₁ : ¬G.Adj x a
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hbc₁ : b ≠ a
Tactic: simp_rw [hca, hdb, mem_insert] at *
Cleared hypotheses: ha, hb, hc, hcj, hd, hdj, had, hbc, hca, hdb
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
hcj₁ : ¬G.Adj x a
hbc₁ : b ≠ a
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hca₁ : True
Tactic: simp_rw [hca, hdb, mem_insert] at *
Cleared hypotheses: ha, hb, hc, hcj, hd, hdj, had, hbc, hca, hdb
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
hcj₁ : ¬G.Adj x a
hbc₁ : b ≠ a
hca₁ : True
hdj₁ : ¬G.Adj x b
had₁ : a ≠ b
hdb₁ : True
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have ha₁ : a = w₁ ∨ a ∈ s
Tactic: simp_rw [hca, hdb, mem_insert] at *
Cleared hypotheses: ha, hb, hc, hcj, hd, hdj, had, hbc, hca, hdb
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hb₁ : b = w₂ ∨ b ∈ t
Tactic: simp_rw [hca, hdb, mem_insert] at *
Cleared hypotheses: ha, hb, hc, hcj, hd, hdj, had, hbc, hca, hdb
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hc₁ : a = v ∨ a ∈ s
Tactic: simp_rw [hca, hdb, mem_insert] at *
Cleared hypotheses: ha, hb, hc, hcj, hd, hdj, had, hbc, hca, hdb
-- 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 : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
hc : c ∈ insert v s
hcj : ¬G.Adj x c
hd : d ∈ insert v t
hdj : ¬G.Adj x d
hab : a ≠ b
had : a ≠ d
hbc : b ≠ c
hat : a ∉ t
hbs : b ∉ s
W : Finset α := {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t)))
hca : c = a
hdb : d = b
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
⊢ ∃ (a : α) (b : α), G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
have hd₁ : b = v ∨ b ∈ t
Tactic: simp_rw [hca, hdb, mem_insert] at *
Cleared hypotheses: ha, hb, hc, hcj, hd, hdj, had, hbc, hca, hdb