awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
w3 : 3 ≤ #W
hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k
⊢ #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1)) ≤ (2 * r + k) * ‖α‖
have neg : (#W - 3 + k + k) * ‖α‖ ≤ (2 * r + k) * ‖α‖
Tactic: rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
hk : ¬k = 0
w3 : 3 ≤ #W
hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k
⊢ (#W - 3 + k + k) * ‖α‖ ≤ (2 * r + k) * ‖α‖
have neg : #W - 3 + k ≤ 2 * r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
⊢ G.minDegree * (2 * r + k + 3) ≤ (2 * r + k) * ‖α‖
have _ : G.minDegree * (2 * r + k + 3) ≤ ∑ w ∈ W, G.degree w + HMul.hMul (α := ℕ) 2 (∑ w ∈ s ∩ t, G.degree w)
Tactic: calc
    _ ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w := by
      simp_rw [add_assoc, add_comm k, ← add_assoc, ← Wc, add_assoc, ← two_mul, mul_add,
               ← hw.card_inter, card_eq_sum_ones, ← mul_assoc, mul_sum, mul_one, mul_comm 2]
      gcongr with i <;> exact minDegree_le_degree ..
    _ ≤ (#X * (#W - 3) + #Xᶜ * (#W - 1)) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) := by gcongr
    _ = #X * (#W - 3 + 2 * k) + #Xᶜ * ((#W - 1) + 2 * (k - 1)) := by grind
    _ ≤ _ := by
        by_cases hk : k = 0 -- so `s ∩ t = ∅` and hence `Xᶜ = ∅`
        · have Xu : X = univ := by
            rw [← hw.card_inter, card_eq_zero] at hk
            exact eq_univ_of_forall fun _ ↦ by simp [X, hk]
          subst k
          rw [add_zero] at Wc
          simp [Xu, Wc, mul_comm]
        have w3 : 3 ≤ #W := two_lt_card.2 ⟨_, mem_insert_self .., _, by simp [W], _, by simp [W],
          hw.isPathGraph3Compl.ne_fst, hw.isPathGraph3Compl.ne_snd, hw.isPathGraph3Compl.fst_ne_snd⟩
        have hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k := by lia
        rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
        gcongr
        lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
_ : G.minDegree * (2 * r + k + 3) ≤ ∑ w ∈ W, G.degree w + HMul.hMul (α := ℕ) 2 (∑ w ∈ s ∩ t, G.degree w)
⊢ G.minDegree * (2 * r + k + 3) ≤ (2 * r + k) * ‖α‖
have _₁ : ∑ w ∈ W, G.degree w + HMul.hMul (α := ℕ) 2 (∑ w ∈ s ∩ t, G.degree w) ≤
  #X * (#W - 3) + #Xᶜ * (#W - 1) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1))
Tactic: calc
    _ ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w := by
      simp_rw [add_assoc, add_comm k, ← add_assoc, ← Wc, add_assoc, ← two_mul, mul_add,
               ← hw.card_inter, card_eq_sum_ones, ← mul_assoc, mul_sum, mul_one, mul_comm 2]
      gcongr with i <;> exact minDegree_le_degree ..
    _ ≤ (#X * (#W - 3) + #Xᶜ * (#W - 1)) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) := by gcongr
    _ = #X * (#W - 3 + 2 * k) + #Xᶜ * ((#W - 1) + 2 * (k - 1)) := by grind
    _ ≤ _ := by
        by_cases hk : k = 0 -- so `s ∩ t = ∅` and hence `Xᶜ = ∅`
        · have Xu : X = univ := by
            rw [← hw.card_inter, card_eq_zero] at hk
            exact eq_univ_of_forall fun _ ↦ by simp [X, hk]
          subst k
          rw [add_zero] at Wc
          simp [Xu, Wc, mul_comm]
        have w3 : 3 ≤ #W := two_lt_card.2 ⟨_, mem_insert_self .., _, by simp [W], _, by simp [W],
          hw.isPathGraph3Compl.ne_fst, hw.isPathGraph3Compl.ne_snd, hw.isPathGraph3Compl.fst_ne_snd⟩
        have hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k := by lia
        rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
        gcongr
        lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
_ : G.minDegree * (2 * r + k + 3) ≤ ∑ w ∈ W, G.degree w + HMul.hMul (α := ℕ) 2 (∑ w ∈ s ∩ t, G.degree w)
_₁ :
  ∑ w ∈ W, G.degree w + HMul.hMul (α := ℕ) 2 (∑ w ∈ s ∩ t, G.degree w) ≤
    #X * (#W - 3) + #Xᶜ * (#W - 1) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1))
⊢ G.minDegree * (2 * r + k + 3) ≤ (2 * r + k) * ‖α‖
have _₂ : #X * (#W - 3) + #Xᶜ * (#W - 1) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) =
  #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1))
Tactic: calc
    _ ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w := by
      simp_rw [add_assoc, add_comm k, ← add_assoc, ← Wc, add_assoc, ← two_mul, mul_add,
               ← hw.card_inter, card_eq_sum_ones, ← mul_assoc, mul_sum, mul_one, mul_comm 2]
      gcongr with i <;> exact minDegree_le_degree ..
    _ ≤ (#X * (#W - 3) + #Xᶜ * (#W - 1)) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) := by gcongr
    _ = #X * (#W - 3 + 2 * k) + #Xᶜ * ((#W - 1) + 2 * (k - 1)) := by grind
    _ ≤ _ := by
        by_cases hk : k = 0 -- so `s ∩ t = ∅` and hence `Xᶜ = ∅`
        · have Xu : X = univ := by
            rw [← hw.card_inter, card_eq_zero] at hk
            exact eq_univ_of_forall fun _ ↦ by simp [X, hk]
          subst k
          rw [add_zero] at Wc
          simp [Xu, Wc, mul_comm]
        have w3 : 3 ≤ #W := two_lt_card.2 ⟨_, mem_insert_self .., _, by simp [W], _, by simp [W],
          hw.isPathGraph3Compl.ne_fst, hw.isPathGraph3Compl.ne_snd, hw.isPathGraph3Compl.fst_ne_snd⟩
        have hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k := by lia
        rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
        gcongr
        lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
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)
xcle : ∀ x ∈ Xᶜ, 1 ≤ #({z ∈ s ∩ t | ¬G.Adj x z})
bdX : ∑ w ∈ s ∩ t, G.degree w ≤ #X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)
Wc : #W + k = 2 * r + 3
_ : G.minDegree * (2 * r + k + 3) ≤ ∑ w ∈ W, G.degree w + HMul.hMul (α := ℕ) 2 (∑ w ∈ s ∩ t, G.degree w)
_₁ :
  ∑ w ∈ W, G.degree w + HMul.hMul (α := ℕ) 2 (∑ w ∈ s ∩ t, G.degree w) ≤
    #X * (#W - 3) + #Xᶜ * (#W - 1) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1))
_₂ :
  #X * (#W - 3) + #Xᶜ * (#W - 1) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) =
    #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1))
⊢ G.minDegree * (2 * r + k + 3) ≤ (2 * r + k) * ‖α‖
have _₃ : #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1)) ≤ (2 * r + k) * ‖α‖
Tactic: calc
    _ ≤ ∑ w ∈ W, G.degree w + 2 * ∑ w ∈ s ∩ t, G.degree w := by
      simp_rw [add_assoc, add_comm k, ← add_assoc, ← Wc, add_assoc, ← two_mul, mul_add,
               ← hw.card_inter, card_eq_sum_ones, ← mul_assoc, mul_sum, mul_one, mul_comm 2]
      gcongr with i <;> exact minDegree_le_degree ..
    _ ≤ (#X * (#W - 3) + #Xᶜ * (#W - 1)) + 2 * (#X * #(s ∩ t) + #Xᶜ * (#(s ∩ t) - 1)) := by gcongr
    _ = #X * (#W - 3 + 2 * k) + #Xᶜ * ((#W - 1) + 2 * (k - 1)) := by grind
    _ ≤ _ := by
        by_cases hk : k = 0 -- so `s ∩ t = ∅` and hence `Xᶜ = ∅`
        · have Xu : X = univ := by
            rw [← hw.card_inter, card_eq_zero] at hk
            exact eq_univ_of_forall fun _ ↦ by simp [X, hk]
          subst k
          rw [add_zero] at Wc
          simp [Xu, Wc, mul_comm]
        have w3 : 3 ≤ #W := two_lt_card.2 ⟨_, mem_insert_self .., _, by simp [W], _, by simp [W],
          hw.isPathGraph3Compl.ne_fst, hw.isPathGraph3Compl.ne_snd, hw.isPathGraph3Compl.fst_ne_snd⟩
        have hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k := by lia
        rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
        gcongr
        lia
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
⊢ G.Colorable (r + 2)
have obtain : ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
  G.Colorable (r + 2)
Tactic: obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
⊢ G.Colorable (r + 2)
have apply : H.Colorable (r + 2)
Tactic: apply Colorable.mono_left hle
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
⊢ H.Colorable (r + 2)
have by_contra! : ∀ (hnotcol : ¬H.Colorable (r + 2)), False
Tactic: by_contra! hnotcol
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
⊢ False
have hn : ¬H.IsCompleteMultipartite
Tactic: have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
⊢ False
have obtain : ∀ (k : ℕ) (w w_1 w_2 : α) (w_3 w_4 : Finset α) (hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4) (hlt : k < r + 1)
  (hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j), False
Tactic: obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w w_1 w_2 : α
w_3 w_4 : Finset α
hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
⊢ False
have hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
Tactic: have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w w_1 w_2 : α
w_3 w_4 : Finset α
hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5)
have apply : (2 * r + 2 + k + 2).succ * ((2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (3 * r + 4).succ) ≤
  (2 * r + 2 + k + 2).succ * ((3 * r + 2) * ‖α‖)
Tactic: apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w w_1 w_2 : α
w_3 w_4 : Finset α
hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * r + 2 + k + 2).succ * ((2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (3 * r + 4).succ) ≤
    (2 * r + 2 + k + 2).succ * ((3 * r + 2) * ‖α‖)
have rw : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (2 * r + 2 + k + 3) * (3 * r + 4).succ ≤
  (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ
Tactic: rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w w_1 w_2 : α
w_3 w_4 : Finset α
hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) * (2 * r + 2 + k + 3) * (3 * r + 4).succ ≤
    (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ
have apply : (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ ≤ (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ
Tactic: apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w w_1 w_2 : α
w_3 w_4 : Finset α
hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ ≤ (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ
have nlinarith : (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ < (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ →
  -1 +
        ((HMul.hMul (α := ℤ) 3 (↑r : ℤ) + 2) * (↑‖α‖ : ℤ) * (HMul.hMul (α := ℤ) 2 (↑r : ℤ) + 2 + (↑k : ℤ) + 2 + 1) + 1 -
          (2 * HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 + (↑k : ℤ)) * (↑‖α‖ : ℤ) * (HMul.hMul (α := ℤ) 3 (↑r : ℤ) + 4 + 1)) +
      3 * (0 - HSub.hSub (α := ℤ) 0 (↑‖α‖ : ℤ) * (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑r : ℤ) 1)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w w_1 w_2 : α
w_3 w_4 : Finset α
hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
nlinarith :
  (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ < (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ →
    -1 +
          ((HMul.hMul (α := ℤ) 3 (↑r : ℤ) + 2) * (↑‖α‖ : ℤ) * (HMul.hMul (α := ℤ) 2 (↑r : ℤ) + 2 + (↑k : ℤ) + 2 + 1) +
              1 -
            (2 * HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 + (↑k : ℤ)) * (↑‖α‖ : ℤ) * (HMul.hMul (α := ℤ) 3 (↑r : ℤ) + 4 + 1)) +
        3 * (0 - HSub.hSub (α := ℤ) 0 (↑‖α‖ : ℤ) * (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑r : ℤ) 1)) =
      0
⊢ (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ ≤ (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ
have nlinarith₁ : (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ < (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ → GT.gt (α := ℤ) 3 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (hypothesis)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
H : SimpleGraph α
hle : G ≤ H
hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H
hnotcol : ¬H.Colorable (r + 2)
hn : ¬H.IsCompleteMultipartite
k : ℕ
w w_1 w_2 : α
w_3 w_4 : Finset α
hw : H.IsFiveWheelLike (r + 1) k w w_1 w_2 w_3 w_4
hlt : k < r + 1
hm : ∀ (j : ℕ), k < j → H.FiveWheelLikeFree (r + 1) j
hD : H.minDegree ≤ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3)
⊢ False
have this : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5)
Tactic: have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.FiveWheelLike (goal)
Goal:
α : Type u_1
G : SimpleGraph α
r_1 : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
r : ℕ
hf : G.CliqueFree (r + 2 + 1)
hd : (3 * (r + 2) - 4) * ‖α‖ / (3 * (r + 2) - 1) < G.minDegree
⊢ G.Colorable (r + 2)
have There : ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
  G.Colorable (r + 2)
Tactic: classical
    -- There is an edge maximal `Kᵣ₊₃`-free supergraph `H` of `G`
    obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf
    -- If `H` is `r + 2`-colorable then so is `G`
    apply Colorable.mono_left hle
    -- Suppose, for a contradiction, that `H` is not `r + 2`-colorable
    by_contra! hnotcol
    -- so `H` is not complete-multipartite
    have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
    -- Hence `H` contains `Wᵣ₊₁,ₖ` but not `Wᵣ₊₁,ₖ₊₁`, for some `k < r + 1`
    obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn
    -- But the minimum degree of `G`, and hence of `H`, is too large for it to be `Wᵣ₊₁,ₖ₊₁`-free,
    -- a contradiction.
    have hD := hw.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ hmcf.1 <| hm _ <| lt_add_one _
    have : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5) := by
      apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _
      rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]
      apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans
      nlinarith
    exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this