Update Mathlib/Algebra/FreeMonoid/Count.lean

Co-authored-by: Ruben Van de Velde <[email protected]>
leanprover-community · Jan 22, 2025 · 36eb824 · 36eb824
1 parent 1895dc6
commit 36eb824
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/FreeMonoid/Count.lean b/Mathlib/Algebra/FreeMonoid/Count.lean
@@ -44,7 +44,7 @@ theorem countP_apply (l : FreeMonoid α) : l.countP p = .ofAdd (l.toList.countP
 lemma countP_of (x : α) : (of x).countP p =
     if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0 := by
   rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]
-  simp only [decide_eq_true_eq, ofAdd_zero]
+  simp only [decide_eq_true_eq]
 
 
 /-- `List.count` as a bundled additive monoid homomorphism. -/