refactor(ring_theory/localization): Golf two proofs (#7520)
refactor(ring_theory/localization): Golf two proofs (#7520)

Golfing two proofs and changing their order.





leanprover-community/mathlib,leanprover-community/mathlib