Fix simpNF linter warnings

This PR fixes 8 simpNF linter warnings across 3 files:

**BumpFunctor.lean:**
- `Bump_apply_of_mem` - Removed @[simp] (simp can prove via Bump_obj + ite_true)
- `Bump_apply_of_not_mem` - Removed @[simp] (simp can prove via Bump_obj + ite_false)

**DirectSumDecompositionDual.lean:**
- `RefinmentMapFunctorial` - Removed @[simp] (argument J cannot be inferred)

**EndoRingIsLocal.lean:**
- `ZeroEndAppIsZero` - Changed LHS to simplified form `fun X => 0`
- `NegApp` - Changed LHS from `(-θ).app X` to `(OppEndo C R F θ).app X`
- `NegAppModule` - Same LHS change as NegApp
- `CompIsComp` - Removed @[simp] (simp can prove via MulDef + NatTrans.comp_app)
- `PowEqCompRight` - Changed LHS from `θ^(n+1)` to `θ ≫ (θ^n)` (already simplified by PowEqCompLeft)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

Author: 2 people

PersistentDecomp/BumpFunctor.lean

@@ -88,12 +88,10 @@ We can also show functoriality in the choice of the element `e`.-/
 
 section API
 
-@[simp]
 lemma Bump_apply_of_mem {x : C} (hx : x ∈ S) :
   (Bump e hz hS).obj x = e := by
   simp only [Bump_obj, hx, ↓reduceIte]
 
-@[simp]
 lemma Bump_apply_of_not_mem {x : C} (hx : x ∉ S) :
   (Bump e hz hS).obj x = z := by
   simp only [Bump_obj, hx, ↓reduceIte]

PersistentDecomp/DirectSumDecompositionDual.lean

@@ -200,7 +200,6 @@ lemma SendsToUniqueGE (I : DirectSumDecomposition M) (J : DirectSumDecomposition
   let B : I := (RefinementMap I J h N)
   rw [UniqueGE I J N A B (⟨h_le, RefinementMapLE I J h N⟩)]
 
-@[simp]
 lemma RefinmentMapFunctorial (I : DirectSumDecomposition M) (J : DirectSumDecomposition M)
     (K : DirectSumDecomposition M) (hij : IsRefinement J I) (hjk : IsRefinement K J)
     (hik : IsRefinement K I) (N : K) :

PersistentDecomp/EndoRingIsLocal.lean

@@ -221,7 +221,7 @@ lemma OneDef : (1 : EndRing C R F) = (𝟙 F) := by
   rfl
 
 @[simp]
-lemma ZeroEndAppIsZero : (ZeroEndomorphism C R F).app = 0 := by
+lemma ZeroEndAppIsZero : (fun X => 0 : ∀ X : C, F.obj X →ₗ[R] F.obj X) = 0 := by
   rfl
 
 @[simp]
@@ -247,19 +247,19 @@ lemma NegDef (θ : EndRing C R F) : -θ = OppEndo C R F θ := by
   rfl
 
 @[simp]
-lemma NegApp (θ : EndRing C R F) (X : C) : (-θ).app X = - (θ.app X) := by
+lemma NegApp (θ : EndRing C R F) (X : C) : (OppEndo C R F θ).app X = - (θ.app X) := by
   rfl
 
 @[simp]
-lemma NegAppModule (θ : EndRing C R F) (X : C) (x : F.obj X) :((-θ).app X) x = - (θ.app X x) := by
+lemma NegAppModule (θ : EndRing C R F) (X : C) (x : F.obj X) :
+    ((OppEndo C R F θ).app X) x = - (θ.app X x) := by
   rfl
 
 @[simp]
 lemma MulDef (e : EndRing C R F) (f : EndRing C R F):
   (e * f) = f ≫ e := by
   rfl
 
-@[simp]
 lemma CompIsComp (e : EndRing C R F) (f : EndRing C R F) (X : C) :
   (e * f).app X = f.app X ≫ e.app X := by
   rfl
@@ -289,8 +289,8 @@ lemma PowEqCompLeft (θ : EndRing C R F) (n : ℕ) : θ^(n+1) = θ ≫ (θ^n) :=
   rfl
 
 @[simp]
-lemma PowEqCompRight (θ : EndRing C R F) (n : ℕ) : θ^(n+1) = (θ^n) ≫ θ := by
-  rw [←MulDef]
+lemma PowEqCompRight (θ : EndRing C R F) (n : ℕ) : θ ≫ (θ^n) = (θ^n) ≫ θ := by
+  rw [←PowEqCompLeft, ←MulDef]
   have h : n = (n+1)-1 := by simp
   nth_rewrite 2 [h]
   rw [mul_pow_sub_one]