linear_combination with square roots: treat r⁻¹ as an atom, read coefficients off the residual

For identities involving r = √((1+c)/2) and divisions by r (e.g. explicit sections of the Hopf map), skip field_simp: simp only [div_eq_mul_inv, mul_inv] and add hinv : r * r⁻¹ = 1 and hr2 : r ^ 2 = (1+c)/2 as hypotheses. ring normalizes (2*r)⁻¹ to 2⁻¹ * r⁻¹ and treats r⁻¹ as an atom, so you can write e.g. linear_combination a * hu + b * hp + (1-c)/2 * (r*s+1) * hinv + ... * hr2 (use r²s²-1 = (rs+1)(rs-1)). When it fails, the 'ring failed' goal is exactly (goal) - (your combination); if it equals k·(lhs - rhs) of one hypothesis, add k to that coefficient. Two or three iterations converge, and each check is a fast single-file lake env lean run. Note field_simp can leave r / r = 1 when it cannot see r ≠ 0; close it with div_self hr.ne'.