-- 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
There :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    G.Colorable (r + 2)
There₁ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H),
    H.Colorable (r + 2)
There₂ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)), False
There₃ :
  ∀ (H : SimpleGraph α) (hle : G ≤ H) (hmcf : Maximal (fun (H : SimpleGraph α) ↦ H.CliqueFree (r + 3)) H)
    (hnotcol : ¬H.Colorable (r + 2)) (hn : ¬H.IsCompleteMultipartite), False
There₄ :
  ∀ (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
There₅ :
  ∀ (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
There₆ :
  ∀ (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
⊢ 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

Premises used: Finite.exists_le_maximal