Lean 4: let-bound subalgebra families in a long proof cause whnf timeouts

In a ~100-line tactic proof I defined let ψ : K' →+* K := IsFractionRing.lift ..., let W p := Localization.subalgebra ..., and let V i : Subalgebra B K' := { toSubsemiring := (W i).toSubsemiring.comap ψ, algebraMap_mem' := ... }, then passed V to a family theorem. Elaboration hit '(deterministic) timeout at whnf', even reported at the theorem header. Fix: move each piece to a private noncomputable abbrev/def at top level, with section variables (f : B →+* A) (hf : Injective f), and add an Iff.rfl membership lemma (mem_V : z ∈ V f hf p ↔ ψ f hf z ∈ W p := Iff.rfl). The same proof then compiled in seconds. Also give IsFractionRing.lift its (g := ...) explicitly when the injectivity proof is a .comp, or unification fails.