Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: case refine_2.h₁
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : R
⊢ ((((Ideal.ResidueField.lift J
                    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp
                      (mapRingHom (algebraMap R I.ResidueField)))
                    ⋯ ⋯).comp
                ↑(aeval ((algebraMap R[X] J.ResidueField) X))).comp
            C).comp
        (algebraMap R I.ResidueField))
      x✝ =
    (((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp C).comp (algebraMap R I.ResidueField)) x✝

pp: case h₂
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((Ideal.ResidueField.lift J
            ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯
            ⋯).comp
        ↑(aeval ((algebraMap R[X] J.ResidueField) X)))
      X =
    (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) X

Tactic:
<;>

Goal state after:
case refine_2.h₁
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : R
⊢ ((((Ideal.ResidueField.lift J
                    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp
                      (mapRingHom (algebraMap R I.ResidueField)))
                    ⋯ ⋯).comp
                ↑(aeval ((algebraMap R[X] J.ResidueField) X))).comp
            C).comp
        (algebraMap R I.ResidueField))
      x✝ =
    (((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp C).comp (algebraMap R I.ResidueField)) x✝

case h₂
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField := ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
⊢ ((Ideal.ResidueField.lift J
            ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯
            ⋯).comp
        ↑(aeval ((algebraMap R[X] J.ResidueField) X)))
      X =
    (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) X