∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S) (hf : Function.Surjective ⇑f) (p : Ideal R) [inst_3 : p.IsPrime],
  (Ideal.Quotient.liftₐ (Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))
          (Polynomial.aeval (1 ⊗ₜ[R] f Polynomial.X)) ⋯).comp
      (Algebra.TensorProduct.lift
        (Algebra.ofId p.ResidueField
          (Polynomial p.ResidueField ⧸
            Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f)))
        (f.liftOfSurjective hf
          ((Ideal.Quotient.mkₐ R
                (Ideal.map (Polynomial.mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker ↑f))).comp
            (Polynomial.mapAlgHom (Algebra.ofId R p.ResidueField)))
          ⋯)
        ⋯) =
    AlgHom.id p.ResidueField (p.Fiber S)