fix proof for leanprover/lean4#5228

leanprover-community · Sep 2, 2024 · 7fe16c1 · 7fe16c1
1 parent 1aac91b
commit 7fe16c1
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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