Lean: linear_combination unfolds `set` variables; use clear_value or an opaque obtain

A variable introduced by set t := (r - D) / (b * r) with ht is a let-binding, and the ring inside linear_combination (and ring_nf) sees through it. Then a combination that is correct in terms of t fails, and the leftover goal is full of b⁻¹ ^ 2 * r⁻¹ ^ 2. Fix: prove the facts you need about t first (e.g. the quadratic it satisfies, via rw [ht]; field_simp; linear_combination ...), then clear_value t so later steps treat it as an atom. To keep an abbreviation opaque from the start, write obtain ⟨r, hr⟩ : ∃ r, r = p₀ ^ 2 + p₁ ^ 2 := ⟨_, rfl⟩ and add c * hr terms to your combinations yourself. Reading the residual: the leftover goal is (goal.lhs - goal.rhs) - Σ cᵢ(hᵢ.lhs - hᵢ.rhs). If it equals k·(hⱼ.lhs - hⱼ.rhs), add k to cⱼ. This fixed every coefficient guess in one round.