Lean: proving ker = (xy - zⁿ) for k[x,y,z] → k[sⁿ,st,tⁿ] without Gröbner bases

To show RingHom.ker π = span {X0*X1 - X2^n} in MvPolynomial (Fin 3) k, avoid normal forms. (1) By MvPolynomial.induction_on (cases C, add, mul_X with fin_cases i), prove ∃ N G, X0^N * f - j G ∈ span {rel}, where G : k[X][X] and j = eval₂RingHom (eval₂RingHom C (X 0)) (X 2) (only the X1 case is real: X0^(N+1) p X1 - jG X2^n = X0^N p · rel + X2^n (X0^N p - jG)). (2) If f ∈ ker then π (j G) = 0; composing with κ = aeval ![C X, X] gives G(sⁿ, st) in k[s][t], whose t^c-coefficient is expand n (G.coeff c) * X^c (Polynomial.induction_on'), so G = 0 by expand_injective. (3) X0 is prime (MvPolynomial.X_prime) and does not divide the relation, so X0^N f ∈ (rel) ⇒ f ∈ (rel) by induction on N. For ring-hom equalities out of k[X][X], use Polynomial.ringHom_ext' (Polynomial.ringHom_ext ...) ... and simp [defs] per generator; simp with ← C_mul/← C_pow loops.