awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ 3 ≤ #W

Tactic:
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⟩
-- 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)
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
⊢ #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k

Tactic:
lia
-- 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)
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
⊢ #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k

Tactic:
have hap : #W - 1 + 2 * (k - 1) = #W - 3 + 2 * k := by lia
-- 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)
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
neg : (#W - 3 + k + k) * ‖α‖ ≤ (2 * r + k) * ‖α‖
⊢ #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1)) ≤ (2 * r + k) * ‖α‖

Tactic:
rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]

Premises used: add_mul, Finset.card_add_card_compl, add_assoc, two_mul, mul_comm
-- 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)
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
neg : #W - 3 + k ≤ 2 * r
⊢ (#W - 3 + k + k) * ‖α‖ ≤ (2 * r + k) * ‖α‖

Tactic:
gcongr
-- 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)
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 ≤ 2 * r

Tactic:
lia
-- 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)
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))
_₃ : #X * (#W - 3 + 2 * k) + #Xᶜ * (#W - 1 + 2 * (k - 1)) ≤ (2 * r + k) * ‖α‖
⊢ G.minDegree * (2 * r + k + 3) ≤ (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

Premises used: HMul.hMul, Compl.compl, HSub.hSub, Inter.inter, HAdd.hAdd, Finset.card, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
hf : G.CliqueFree (HAdd.hAdd (α := ℕ) 0 1)
hd : (HMul.hMul (α := ℕ) 3 0 - 4) * ‖α‖ / (HMul.hMul (α := ℕ) 3 0 - 1) < G.minDegree
⊢ G.Colorable 0

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
hf : G.CliqueFree (HAdd.hAdd (α := ℕ) 1 1)
hd : (HMul.hMul (α := ℕ) 3 1 - 4) * ‖α‖ / (HMul.hMul (α := ℕ) 3 1 - 1) < G.minDegree
⊢ G.Colorable 1

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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
obtain :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    G.Colorable (r + 2)
⊢ G.Colorable (r + 2)

Tactic:
obtain ⟨H, hle, hmcf⟩ := @Finite.exists_le_maximal _ _ _ (fun H ↦ H.CliqueFree (r + 3)) G hf

Premises used: Finite.exists_le_maximal
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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
apply : H.Colorable (r + 2)
⊢ G.Colorable (r + 2)

Tactic:
apply Colorable.mono_left hle

Premises used: SimpleGraph.Colorable.mono_left
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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
by_contra! : ∀ (hnotcol : ¬H.Colorable (r + 2)), False
⊢ H.Colorable (r + 2)

Tactic:
by_contra! hnotcol
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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)
⊢ ¬H.IsCompleteMultipartite

Tactic:
have hn : ¬ H.IsCompleteMultipartite := fun hc ↦ hnotcol <| hc.colorable_of_cliqueFree hmcf.1
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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
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
⊢ False

Tactic:
obtain ⟨k, _, _, _, _, _, hw, hlt, hm⟩ :=
      exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite hmcf hn

Premises used: SimpleGraph.exists_max_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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
⊢ 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 _
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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)
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) * ‖α‖)
⊢ (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5)

Tactic:
apply (Nat.le_div_iff_mul_le <| Nat.succ_pos _).2
              <| (mul_le_mul_iff_right₀ (_ + 2).succ_pos).1 _

Premises used: Iff.mpr, Nat.succ_pos, Iff.mp, Nat.le_div_iff_mul_le, mul_le_mul_iff_right₀
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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)
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
⊢ (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:
rw [← mul_assoc, mul_comm (2 * r + 2 + k + 3), mul_comm _ (_ * ‖α‖)]

Premises used: HMul.hMul, mul_assoc, Fintype.card, HAdd.hAdd, mul_comm, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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)
apply : (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ ≤ (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ
⊢ (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:
apply (Nat.mul_le_mul_right _ (Nat.div_mul_le_self ..)).trans

Premises used: Nat.div_mul_le_self, Nat.mul_le_mul_right, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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
nlinarith₁ :
  (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ < (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ → GT.gt (α := ℤ) 3 0
⊢ (2 * (r + 1) + k) * ‖α‖ * (3 * r + 4).succ ≤ (3 * r + 2) * ‖α‖ * (2 * r + 2 + k + 2).succ

Tactic:
nlinarith
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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)

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
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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)
this : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5)
⊢ False

Tactic:
(hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this

Premises used: LT.lt.trans_le, LE.le.trans, LT.lt.not_ge, SimpleGraph.minDegree_le_minDegree
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
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)
this : (2 * (r + 1) + k) * ‖α‖ / (2 * (r + 1) + k + 3) ≤ (3 * r + 2) * ‖α‖ / (3 * r + 5)
⊢ False

Tactic:
exact (hd.trans_le <| minDegree_le_minDegree hle).not_ge <| hD.trans <| this

Premises used: LT.lt.trans_le, LE.le.trans, LT.lt.not_ge, SimpleGraph.minDegree_le_minDegree
-- Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
Goal:
α : Type u_1
G : SimpleGraph α
r : ℕ
inst : Fintype α
inst_1 : DecidableRel G.Adj
hf : G.CliqueFree (r + 1)
hd : (3 * r - 4) * ‖α‖ / (3 * r - 1) < G.minDegree
⊢ G.Colorable r

Tactic:
match r with
  | 0 | 1 => aesop
  | r + 2 =>
    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
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
n : ℕ∞
⊢ n ≤ G.egirth ↔ ∀ (a : α) (w : G.Walk a a), w.IsCycle → n ≤ (↑w.length : ℕ∞)

Tactic:
simp [egirth]

Premises used: SimpleGraph.egirth
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
h : w.IsCycle
⊢ G.egirth ≤ (↑w.length : ℕ∞)

Tactic:
le_egirth.mp le_rfl a w h

Premises used: le_rfl, Iff.mp, SimpleGraph.le_egirth
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
⊢ G.egirth = ⊤ ↔ G.IsAcyclic

Tactic:
simp [egirth, IsAcyclic]

Premises used: SimpleGraph.IsAcyclic, SimpleGraph.egirth
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G H : SimpleGraph α
h : G ≤ H
a : α
w : G.Walk a a
hw : w.IsCycle
⊢ LE.le (α := ℕ∞) (↑(Walk.mapLe h w).length : ℕ∞) (↑w.length : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)) ↔ ¬G.IsAcyclic

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
refine_1 : (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)) → ¬G.IsAcyclic
refine_2 : ∀ (h : ¬G.IsAcyclic), ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)) ↔ ¬G.IsAcyclic

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hw : w.IsCycle
right : G.egirth = (↑w.length : ℕ∞)
hG : G.IsAcyclic
⊢ False

Tactic:
hG _ hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hw : w.IsCycle
right : G.egirth = (↑w.length : ℕ∞)
hG : G.IsAcyclic
⊢ False

Tactic:
exact hG _ hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
refine_2 :
  ∀ (h : Nonempty.{u_1 + 1} ((i : α) × Subtype (α := G.Walk i i) Walk.IsCycle)),
    ∃ (x : (a : α) × { a_1 : G.Walk a a // a_1.IsCycle }),
      Eq (α := ℕ∞)
        (↑(↑(x.snd (β := fun (a : α) ↦ { a_1 : G.Walk a a // a_1.IsCycle })) : G.Walk x.fst x.fst).length : ℕ∞)
        (⨅ (x : (i : α) × Subtype (α := G.Walk i i) Walk.IsCycle),
          (↑(↑(x.snd (β := fun (i : α) ↦ Subtype (α := G.Walk i i) Walk.IsCycle)) : G.Walk x.fst x.fst).length : ℕ∞))
⊢ ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = (↑w.length : ℕ∞)

Tactic:
simp_rw [← egirth_eq_top, ← Ne.eq_def, egirth, iInf_subtype', iInf_sigma', ENat.iInf_coe_ne_top,
      ← exists_prop, Subtype.exists', Sigma.exists', eq_comm] at h ⊢

Premises used: Sigma.exists', iInf_sigma', SimpleGraph.egirth_eq_top, iInf_subtype', Subtype.exists', Ne.eq_def, ENat.iInf_coe_ne_top, exists_prop, eq_comm, SimpleGraph.egirth