chore(GroupTheory/FreeGroup): golf proof using autogenerated lemma (leanprover-community#40902)

I forgot to add this in leanprover-community#40657 apparently.

It seems like we don't need this lemma anyways; but thats beyond the scope of this PR.

Co-authored-by: Batixx <s59fpern@uni-bonn.de>

Author: felixpernegger

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -332,15 +332,13 @@ protected theorem sublist : Red L₁ L₂ → L₂ <+ L₁ :=
 theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length :=
   h.sublist.length_le
 
-set_option linter.auxLemma false in
 @[to_additive (attr := deprecated "Should not be needed." (since := "2026-04-10"))]
 theorem sizeof_of_step : ∀ {L₁ L₂ : List (α × Bool)},
     Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
   | _, _, @Step.not _ L1 L2 x b => by
     induction L1 with
     | nil =>
-      -- This was just `dsimp` prior to https://github.com/leanprover/lean4/pull/13320
-      dsimp [sizeOf, _sizeOf_1]
+      rw [nil_append, nil_append, cons.sizeOf_spec, cons.sizeOf_spec]
       lia
     | cons hd tl ih =>
       dsimp