awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  Eq (α := RatFunc I.ResidueField →+* RatFunc I.ResidueField)
    (↑(AlgHom.comp { toRingHom := f, commutes' := ⋯ }
          (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)) :
      RatFunc I.ResidueField →+* RatFunc I.ResidueField)
    (↑(AlgHom.id I.ResidueField (RatFunc I.ResidueField)) : RatFunc I.ResidueField →+* RatFunc I.ResidueField)
⊢ Eq (α := RatFunc I.ResidueField →ₐ[I.ResidueField] RatFunc I.ResidueField)
    (AlgHom.comp { toRingHom := f, commutes' := ⋯ }
      (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯))
    (AlgHom.id I.ResidueField (RatFunc I.ResidueField))

Tactic:
apply AlgHom.coe_ringHom_injective

Premises used: AlgHom.coe_ringHom_injective
-- 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 :
  Eq.{u_1 + 1} (α := I.ResidueField[X] →+* RatFunc I.ResidueField)
    ((fun (f : RatFunc I.ResidueField →+* RatFunc I.ResidueField) ↦
        (f.comp (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) : I.ResidueField[X] →+* RatFunc I.ResidueField))
      (↑(AlgHom.comp { toRingHom := f, commutes' := ⋯ }
            (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)) :
        RatFunc I.ResidueField →+* RatFunc I.ResidueField))
    ((fun (f : RatFunc I.ResidueField →+* RatFunc I.ResidueField) ↦
        (f.comp (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) : I.ResidueField[X] →+* RatFunc I.ResidueField))
      (↑(AlgHom.id I.ResidueField (RatFunc I.ResidueField)) : RatFunc I.ResidueField →+* RatFunc I.ResidueField))
⊢ Eq (α := RatFunc I.ResidueField →+* RatFunc I.ResidueField)
    (↑(AlgHom.comp { toRingHom := f, commutes' := ⋯ }
          (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)) :
      RatFunc I.ResidueField →+* RatFunc I.ResidueField)
    (↑(AlgHom.id I.ResidueField (RatFunc I.ResidueField)) : RatFunc I.ResidueField →+* RatFunc I.ResidueField)

Tactic:
apply IsFractionRing.injective_comp_algebraMap (A := I.ResidueField[X])

Premises used: IsFractionRing.injective_comp_algebraMap
-- 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 :
  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))
⊢ Eq (α := I.ResidueField[X] →+* RatFunc I.ResidueField)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgHom.comp { toRingHom := f, commutes' := ⋯ }
            {
              toRingHom :=
                RatFunc.liftRingHom
                  (↑(aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
                        I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
                    I.ResidueField[X] →+* J.ResidueField)
                  ⋯,
              commutes' := ⋯ }) :
        RatFunc I.ResidueField →+* RatFunc I.ResidueField)
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)))
    (RingHom.comp (RingHom.id (RatFunc I.ResidueField)) (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)))

Tactic:
simp only [AlgHom.comp_toRingHom, AlgHom.coe_ringHom_mk, RingHom.comp_assoc,
      RatFunc.liftRingHom_comp_algebraMap, RingHomCompTriple.comp_eq, f]

Premises used: AlgHom.comp_toRingHom, AlgHom.coe_ringHom_mk, RingHomCompTriple.comp_eq, RingHom.comp_assoc, RatFunc.liftRingHom_comp_algebraMap
-- 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))
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)

Tactic:
simp [← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R R[X] J.ResidueField]

Premises used: Ideal.ResidueField, Polynomial, IsScalarTower.algebraMap_apply
-- 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))
⊢ 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)

Tactic:
simp [← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R R[X] J.ResidueField]

Premises used: Ideal.ResidueField, Polynomial, IsScalarTower.algebraMap_apply
-- 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_3 :
  Eq (α := J.ResidueField →+* J.ResidueField)
    (↑(AlgHom.comp (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)
            { toRingHom := f, commutes' := ⋯ } :
          J.ResidueField →ₐ[I.ResidueField] J.ResidueField) :
      J.ResidueField →+* J.ResidueField)
    (↑(AlgHom.id I.ResidueField J.ResidueField) : J.ResidueField →+* J.ResidueField)
⊢ Eq (α := J.ResidueField →ₐ[I.ResidueField] J.ResidueField)
    (AlgHom.comp (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)
        { toRingHom := f, commutes' := ⋯ } :
      J.ResidueField →ₐ[I.ResidueField] J.ResidueField)
    (AlgHom.id I.ResidueField J.ResidueField : J.ResidueField →ₐ[I.ResidueField] J.ResidueField)

Tactic:
apply AlgHom.coe_ringHom_injective

Premises used: AlgHom.coe_ringHom_injective
-- 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_3 :
  ∀ (x : R),
    Eq (α := J.ResidueField)
      ((RingHom.comp
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(AlgHom.comp
                        (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X))
                          ⋯)
                        { toRingHom := f, commutes' := ⋯ } :
                      J.ResidueField →ₐ[I.ResidueField] J.ResidueField) :
                  J.ResidueField →+* J.ResidueField)
                (algebraMap R[X] J.ResidueField))
              C :
            (a : R) → J.ResidueField)
          x :
        J.ResidueField)
      ((RingHom.comp
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                (↑(AlgHom.id I.ResidueField J.ResidueField) : J.ResidueField →+* J.ResidueField)
                (algebraMap R[X] J.ResidueField))
              C :
            (a : R) → J.ResidueField)
          x :
        J.ResidueField)
refine_3₁ :
  Eq (α := J.ResidueField)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgHom.comp
                    (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)
                    { toRingHom := f, commutes' := ⋯ } :
                  J.ResidueField →ₐ[I.ResidueField] J.ResidueField) :
              J.ResidueField →+* J.ResidueField)
            (algebraMap R[X] J.ResidueField) :
          (a : R[X]) → J.ResidueField)
        X :
      J.ResidueField)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgHom.id I.ResidueField J.ResidueField) : J.ResidueField →+* J.ResidueField)
            (algebraMap R[X] J.ResidueField) :
          (a : R[X]) → J.ResidueField)
        X :
      J.ResidueField)
⊢ Eq (α := J.ResidueField →+* J.ResidueField)
    (↑(AlgHom.comp (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)
            { toRingHom := f, commutes' := ⋯ } :
          J.ResidueField →ₐ[I.ResidueField] J.ResidueField) :
      J.ResidueField →+* J.ResidueField)
    (↑(AlgHom.id I.ResidueField J.ResidueField) : J.ResidueField →+* J.ResidueField)

Tactic:
ext
-- 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))
x : R
refine_3 :
  Eq (α := J.ResidueField) ((algebraMap R J.ResidueField : (a : R) → J.ResidueField) x : J.ResidueField)
    ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) ((C : (a : R) → R[X]) x) : J.ResidueField)
⊢ Eq (α := J.ResidueField)
    ((RingHom.comp
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgHom.comp
                      (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)
                      { toRingHom := f, commutes' := ⋯ } :
                    J.ResidueField →ₐ[I.ResidueField] J.ResidueField) :
                J.ResidueField →+* J.ResidueField)
              (algebraMap R[X] J.ResidueField))
            C :
          (a : R) → J.ResidueField)
        x :
      J.ResidueField)
    ((RingHom.comp
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgHom.id I.ResidueField J.ResidueField) : J.ResidueField →+* J.ResidueField)
              (algebraMap R[X] J.ResidueField))
            C :
          (a : R) → J.ResidueField)
        x :
      J.ResidueField)

Tactic:
simp [f, RatFunc.liftAlgHom, ← IsScalarTower.algebraMap_apply]

Premises used: RatFunc.liftAlgHom, IsScalarTower.algebraMap_apply
-- 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))
x : R
⊢ Eq (α := J.ResidueField) ((algebraMap R J.ResidueField : (a : R) → J.ResidueField) x : J.ResidueField)
    ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) ((C : (a : R) → R[X]) x) : J.ResidueField)

Tactic:
rfl
-- 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))
⊢ Eq (α := J.ResidueField)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgHom.comp
                    (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) ⋯)
                    { toRingHom := f, commutes' := ⋯ } :
                  J.ResidueField →ₐ[I.ResidueField] J.ResidueField) :
              J.ResidueField →+* J.ResidueField)
            (algebraMap R[X] J.ResidueField) :
          (a : R[X]) → J.ResidueField)
        X :
      J.ResidueField)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgHom.id I.ResidueField J.ResidueField) : J.ResidueField →+* J.ResidueField)
            (algebraMap R[X] J.ResidueField) :
          (a : R[X]) → J.ResidueField)
        X :
      J.ResidueField)

Tactic:
simp [f, RatFunc.liftAlgHom]

Premises used: RatFunc.liftAlgHom
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
J : Ideal R[X]
inst_2 : J.IsPrime
inst_3 : J.LiesOver I
inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
p : R[X]
⊢ Eq (α := RatFunc I.ResidueField)
    (((residueFieldMapCAlgEquiv I J hJ : J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField) :
          (a : J.ResidueField) → RatFunc I.ResidueField)
        ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) p) :
      RatFunc I.ResidueField)
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField) : (a : I.ResidueField[X]) → RatFunc I.ResidueField)
        (map (algebraMap R I.ResidueField) p) :
      RatFunc I.ResidueField)

Tactic:
simp [residueFieldMapCAlgEquiv]

Premises used: Polynomial.residueFieldMapCAlgEquiv
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
J : Ideal R[X]
inst_2 : J.IsPrime
inst_3 : J.LiesOver I
inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
r : I.ResidueField
⊢ Eq (α := J.ResidueField)
    (((AlgEquiv.symm (residueFieldMapCAlgEquiv I J hJ) : RatFunc I.ResidueField ≃ₐ[I.ResidueField] J.ResidueField) :
          (a : RatFunc I.ResidueField) → J.ResidueField)
        ((RatFunc.C : (a : I.ResidueField) → RatFunc I.ResidueField) r) :
      J.ResidueField)
    ((algebraMap I.ResidueField J.ResidueField : (a : I.ResidueField) → J.ResidueField) r : J.ResidueField)

Tactic:
(residueFieldMapCAlgEquiv I J hJ).symm.commutes r

Premises used: Polynomial.residueFieldMapCAlgEquiv, AlgEquiv.symm, AlgEquiv.commutes
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
J : Ideal R[X]
inst_2 : J.IsPrime
inst_3 : J.LiesOver I
inst_4 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst_5 : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map (F := R →+* R[X]) C I
⊢ Eq (α := RatFunc I.ResidueField)
    (((residueFieldMapCAlgEquiv I J hJ : J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField) :
          (a : J.ResidueField) → RatFunc I.ResidueField)
        (((AlgEquiv.symm (residueFieldMapCAlgEquiv I J hJ) : RatFunc I.ResidueField ≃ₐ[I.ResidueField] J.ResidueField) :
            (a : RatFunc I.ResidueField) → J.ResidueField)
          RatFunc.X) :
      RatFunc I.ResidueField)
    (((residueFieldMapCAlgEquiv I J hJ : J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField) :
          (a : J.ResidueField) → RatFunc I.ResidueField)
        ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
      RatFunc I.ResidueField)

Tactic:
simp