diff --git a/Mathlib/GroupTheory/Index.lean b/Mathlib/GroupTheory/Index.lean
index 62cf28d8f4961c..c8e29161e5566c 100644
--- a/Mathlib/GroupTheory/Index.lean
+++ b/Mathlib/GroupTheory/Index.lean
@@ -615,3 +615,26 @@ theorem index_center_le_pow [Finite (commutatorSet G)] [Group.FG G] :
 end FiniteIndex
 
 end Subgroup
+
+namespace MonoidHom
+
+open Finset
+
+variable {G M F : Type*} [Group G] [Fintype G] [Monoid M] [DecidableEq M]
+  [FunLike F G M] [MonoidHomClass F G M]
+
+@[to_additive]
+lemma card_fiber_eq_of_mem_range (f : F) {x y : M} (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) :
+    (univ.filter <| fun g => f g = x).card = (univ.filter <| fun g => f g = y).card := by
+  rcases hx with ⟨x, rfl⟩
+  rcases hy with ⟨y, rfl⟩
+  rcases mul_left_surjective x y with ⟨y, rfl⟩
+  conv_lhs =>
+    rw [← map_univ_equiv (Equiv.mulRight y⁻¹), filter_map, card_map]
+  congr 2 with g
+  simp only [Function.comp, Equiv.toEmbedding_apply, Equiv.coe_mulRight, map_mul]
+  let f' := MonoidHomClass.toMonoidHom f
+  show f' g * f' y⁻¹ = f' x ↔ f' g = f' x * f' y
+  rw [← f'.coe_toHomUnits y⁻¹, map_inv, Units.mul_inv_eq_iff_eq_mul, f'.coe_toHomUnits]
+
+end MonoidHom
diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
index f37be62c258738..6095f071ddd4f6 100644
--- a/Mathlib/RingTheory/IntegralDomain.lean
+++ b/Mathlib/RingTheory/IntegralDomain.lean
@@ -192,15 +192,6 @@ end EuclideanDivision
 
 variable [Fintype G]
 
-theorem card_fiber_eq_of_mem_range {H : Type*} [Group H] [DecidableEq H] (f : G →* H) {x y : H}
-    (hx : x ∈ Set.range f) (hy : y ∈ Set.range f) :
-    -- Porting note: the `filter` had an index `ₓ` that I removed.
-    (univ.filter fun g => f g = x).card = (univ.filter fun g => f g = y).card := by
-  rcases hx with ⟨x, rfl⟩
-  rcases hy with ⟨y, rfl⟩
-  exact card_equiv (Equiv.mulRight (x⁻¹ * y)) (by simp [mul_inv_eq_one])
-#align card_fiber_eq_of_mem_range card_fiber_eq_of_mem_range
-
 /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero.
 -/
 theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 := by
@@ -236,7 +227,7 @@ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0
       _ = (0 : R) := smul_zero _
     · -- remaining goal 1
       show (univ.filter fun g : G => f.toHomUnits g = u).card = c
-      apply card_fiber_eq_of_mem_range f.toHomUnits
+      apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits
       · simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu
       · exact ⟨1, f.toHomUnits.map_one⟩
     -- remaining goal 2