-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal R
inst_3 : I.IsPrime
J : Ideal R[X]
inst_4 : J.IsPrime
inst_5 : J.LiesOver I
inst_6 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_7 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    ⋯ ⋯
hf :
  Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))
refine_2 :
  ∀ (x : R),
    Eq (α := RatFunc I.ResidueField)
      ((RingHom.comp
              (RingHom.comp
                (RingHom.comp
                  (Ideal.ResidueField.lift J
                    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
                      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField))
                      (mapRingHom (algebraMap R I.ResidueField)))
                    ⋯ ⋯)
                  (↑(aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
                        I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
                    I.ResidueField[X] →+* J.ResidueField))
                C)
              (algebraMap R I.ResidueField) :
            (a : R) → RatFunc I.ResidueField)
          x :
        RatFunc I.ResidueField)
      ((@RingHom.comp _ I.ResidueField _ _ Semiring.toNonAssocSemiring _
              (RingHom.comp (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) C) (algebraMap R I.ResidueField) :
            (a : R) → RatFunc I.ResidueField)
          x :
        RatFunc I.ResidueField)
refine_2₁ :
  Eq (α := RatFunc I.ResidueField)
    ((RingHom.comp
            (Ideal.ResidueField.lift J
              (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
                (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
              ⋯ ⋯)
            (↑(aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
                  I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
              I.ResidueField[X] →+* J.ResidueField) :
          (a : I.ResidueField[X]) → RatFunc I.ResidueField)
        X :
      RatFunc I.ResidueField)
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField) : (a : I.ResidueField[X]) → RatFunc I.ResidueField) X :
      RatFunc I.ResidueField)
⊢ Eq (α := I.ResidueField[X] →+* RatFunc I.ResidueField)
    (RingHom.comp
      (Ideal.ResidueField.lift J
        (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
          (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
        ⋯ ⋯)
      (↑(aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
        I.ResidueField[X] →+* J.ResidueField))
    (algebraMap I.ResidueField[X] (RatFunc I.ResidueField))

Tactic:
ext