Lean: state closed-fibre instances for a RingHom, not algebraMap, so localRingHom fibres work

An instance IsLocalRing (S ⧸ (maximalIdeal R).map (algebraMap R S)) (needs [IsLocalHom (algebraMap R S)]) does NOT fire in a theorem statement about Localization.AtPrime P ⧸ (maximalIdeal (Localization.AtPrime (P.under R))).map (Localization.localRingHom _ P f rfl): there is no Algebra instance in the statement, so depth of the fibre fails with 'failed to synthesize IsLocalRing'. Fix: state it as instance (f : R →+* S) [IsLocalHom f] : IsLocalRing (S ⧸ (maximalIdeal R).map f) (Mathlib's Localization.isLocalHom_localRingHom is already an instance); algebraMap uses still unify. If the section has [Algebra R S] [IsLocalHom (algebraMap R S)] variables, put omit [...] in BEFORE the docstring. Separately: exact_mod_cast cannot move min through ℕ → WithBot ℕ∞; prove ((min x y : ℕ) : WithBot ℕ∞) = min ↑x ↑y by Monotone.map_min (f := fun n : ℕ ↦ (n : WithBot ℕ∞)) fun _ _ h ↦ by simpa using h, rewrite with it, then omega on ℕ.