Mem associated Primes ker mk Linear Map of mem associated Primes of inter nonempty

lemma mem_associatedPrimes_ker_mkLinearMap_of_mem_associatedPrimes_of_inter_nonempty{R : Type*} [CommRing R] [IsNoetherianRing R]{M : Type*} [AddCommGroup M] [Module R M](S : Submonoid R) {p : Ideal R}(hp : p ∈ associatedPrimes R M) (hinter : (p.carrier ∩ S).Nonempty) :  p ∈ associatedPrimes R (LinearMap.ker (LocalizedModule.mkLinearMap S M)) := by  rcases ((isAssociatedPrime_iff (R := R) (M := M)).mp hp) with ⟨hpPrime, y, hy⟩  rcases hinter with ⟨r, hrp, hrS⟩  have hry : r • y = 0 := by    rw [hy] at hrp    simpa [Submodule.mem_colon_singleton] using hrp  have hyker : y ∈ LinearMap.ker (LocalizedModule.mkLinearMap S M) := by    rw [LinearMap.mem_ker]    exact (LocalizedModule.mem_ker_mkLinearMap_iff (S := S) (m := y)).2 ⟨r, hrS, hry⟩  refine ((isAssociatedPrime_iff (R := R) (M := LinearMap.ker (LocalizedModule.mkLinearMap S M))).2    ⟨hpPrime, ⟨y, hyker⟩, ?_⟩)  ext z  constructor  · intro hz    rw [hy] at hz    simpa [Submodule.mem_colon_singleton] using hz  · intro hz    rw [hy]    simpa [Submodule.mem_colon_singleton] using hz