diff --git a/Mathlib/Algebra/DirectSum/Decomposition.lean b/Mathlib/Algebra/DirectSum/Decomposition.lean
index 8de190c040407..f47be7b117efd 100644
--- a/Mathlib/Algebra/DirectSum/Decomposition.lean
+++ b/Mathlib/Algebra/DirectSum/Decomposition.lean
@@ -143,6 +143,10 @@ theorem decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j
   rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ _ hij, ZeroMemClass.coe_zero]
 #align direct_sum.decompose_of_mem_ne DirectSum.decompose_of_mem_ne
 
+theorem degree_eq_of_mem_mem {x : M} {i j : ι} (hxi : x ∈ ℳ i) (hxj : x ∈ ℳ j) (hx : x ≠ 0) :
+    i = j := by
+  contrapose! hx; rw [← decompose_of_mem_same ℳ hxj, decompose_of_mem_ne ℳ hxi hx]
+
 /-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
 an additive monoid to a direct sum of components. -/
 -- Porting note: deleted [simps] and added the corresponding lemmas by hand