Lean: make let-bound atoms opaque before ring/linear_combination

When a proof introduces let v := fun i => algebraMap B L (X i) and later simp produces a mix of v i and algebraMap B L (X i), ring/linear_combination may treat them as different atoms or fail after zeta-reduction. Instead write obtain ⟨v, hv⟩ : ∃ v : Fin 4 → L, ∀ i, algebraMap B L (X i) = v i := ⟨_, fun _ => rfl⟩ and include hv in the simp only set: every occurrence folds into the opaque v i, and the final identity (e.g. dehomogenize/rehomogenize a monomial using v2^a·v2^b = v2^c·v2^d and (v3/v2)^d·v2^d = v3^d) closes with one linear_combination. Also: aeval of algebraMap k _ r is not simplified by aeval_C; add AlgHom.commutes to the simp set.