diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean
index c199075721237..55083d6852a86 100644
--- a/Mathlib/GroupTheory/FreeGroup/Basic.lean
+++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean
@@ -287,7 +287,8 @@ theorem red_iff_irreducible {x1 b1 x2 b2} (h : (x1, b1) ≠ (x2, b2)) :
   generalize eq : [(x1, not b1), (x2, b2)] = L'
   intro L h'
   cases h'
-  simp [List.cons_eq_append, List.nil_eq_append] at eq
+  simp only [List.cons_eq_append, List.cons.injEq, Prod.mk.injEq, and_false, List.nil_eq_append,
+    exists_const, or_self, or_false, List.cons_ne_nil] at eq
   rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩
   simp at h