chore: clean up FiveWheelLike (#31813)

Restores lemmas in Mathlib.Combinatorics.SimpleGraph.FiveWheelLike that had been commented out during nightly testing, but which now build again (unmodified).

Author: thorimur

Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean

@@ -346,13 +346,6 @@ lemma exists_isFiveWheelLike_succ_of_not_adj_le_two (hW : ∀ ⦃y⦄, y ∈ s 
         notMem_mono inter_subset_left hbs, erase_eq_of_notMem <| notMem_mono inter_subset_right hat,
         card_insert_of_notMem (fun h ↦ G.irrefl (hW h)), hw.card_inter]
 
-#adaptation_note
-/--
-Due to a change in `grind` between `nightly-2025-10-31` and `nightly-2025-11-02`,
-this proof is no longer working. I've temporarily commented it out to get a build of
-`nightly-testing`.
--/
-/-
 /--
 If `G` is a `Kᵣ₊₂`-free graph with `n` vertices containing a `Wᵣ,ₖ` but no `Wᵣ,ₖ₊₁`
 then `G.minDegree ≤ (2 * r + k) * n / (2 * r + k + 3)`
@@ -415,16 +408,11 @@ lemma minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ [Fintype α]
         rw [hap, ← add_mul, card_add_card_compl, mul_comm, two_mul, ← add_assoc]
         gcongr
         cutsat
--/
+
 end IsFiveWheelLike
 
 variable [DecidableEq α]
 
-#adaptation_note
-/--
-I've temporarily commented it out to get a build of `nightly-testing`. See the note above.
--/
-/-
 /-- **Andrasfái-Erdős-Sós** theorem
 
 If `G` is a `Kᵣ₊₁`-free graph with `n` vertices and `(3 * r - 4) * n / (3 * r - 1) < G.minDegree`
@@ -459,6 +447,6 @@ theorem colorable_of_cliqueFree_lt_minDegree [Fintype α] [DecidableRel G.Adj]
       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
--/
+
 end AES
 end SimpleGraph