awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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_1 : I.ResidueField[X]
x : I.ResidueField[X]
hx :
  Eq (α := J.ResidueField)
    (((aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
          (a : I.ResidueField[X]) → J.ResidueField)
        x :
      J.ResidueField)
    (0 : J.ResidueField)
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hb0 : Membership.mem (α := R ⧸ I) (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I)
hb :
  map (R := R ⧸ I) (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) =
    HSMul.hSMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) s : R ⧸ I) x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x
have refine : map (algebraMap R I.ResidueField) r = s • x
Tactic: refine ⟨s, by simpa [Ideal.Quotient.eq_zero_iff_mem] using hb0, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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_1 : I.ResidueField[X]
x : I.ResidueField[X]
hx :
  Eq (α := J.ResidueField)
    (((aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
          (a : I.ResidueField[X]) → J.ResidueField)
        x :
      J.ResidueField)
    (0 : J.ResidueField)
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
⊢ x = 0
have refine_1 : ∀ (s : R) (hs : s ∉ I) (hr : map (algebraMap R I.ResidueField) r = s • x), x = 0
Tactic: obtain ⟨s, hs, hr⟩ : ∃ s ∉ I, r.map (algebraMap _ _) = s • x := by
      obtain ⟨b, hb0, hb⟩ := IsLocalization.integerNormalization_spec (R ⧸ I)⁰ x
      obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective b
      refine ⟨s, by simpa [Ideal.Quotient.eq_zero_iff_mem] using hb0, ?_⟩
      simpa [← hr, map_map, ← Ideal.Quotient.algebraMap_eq] using hb
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (hypothesis)
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_1 : I.ResidueField[X]
x : I.ResidueField[X]
hx :
  Eq (α := J.ResidueField)
    (((aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
          (a : I.ResidueField[X]) → J.ResidueField)
        x :
      J.ResidueField)
    (0 : J.ResidueField)
r : R[X]
hr_1 : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
⊢ r ∈ J
have hr₁ : Eq (α := J.ResidueField)
  (((aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
        (a : I.ResidueField[X]) → J.ResidueField)
      (map (algebraMap R I.ResidueField) r) :
    J.ResidueField)
  (((aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
        (a : I.ResidueField[X]) → J.ResidueField)
      (s • x) :
    J.ResidueField)
Tactic: apply_fun aeval (algebraMap R[X] J.ResidueField X) at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (hypothesis)
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_1 : I.ResidueField[X]
x : I.ResidueField[X]
hx :
  Eq (α := J.ResidueField)
    (((aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField) :
          (a : I.ResidueField[X]) → J.ResidueField)
        x :
      J.ResidueField)
    (0 : J.ResidueField)
r : R[X]
hr_1 : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
⊢ x = 0
have hx₁ : r ∈ J
Tactic: replace hx : r ∈ J := by
      apply_fun aeval (algebraMap R[X] J.ResidueField X) at hr
      simpa [hx, aeval_map_algebraMap, aeval_algebraMap_apply, Algebra.smul_def] using hr
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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_1 : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr_1 : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ x = 0
have refine_1 : Eq.{u_1 + 1} (α := I.ResidueField[X])
  ((fun (x : I.ResidueField[X]) ↦
      HMul.hMul (α := I.ResidueField[X])
        ((C : (a : I.ResidueField) → I.ResidueField[X]) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) s) :
          I.ResidueField[X])
        x)
    x)
  ((fun (x : I.ResidueField[X]) ↦
      HMul.hMul (α := I.ResidueField[X])
        ((C : (a : I.ResidueField) → I.ResidueField[X]) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) s) :
          I.ResidueField[X])
        x)
    0)
Tactic: refine ((IsUnit.mk0 (algebraMap R I.ResidueField s) (by simpa)).map C).mul_right_injective ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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_1 : I.ResidueField[X]
x : I.ResidueField[X]
r : R[X]
hr_1 : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hs : s ∉ I
hr : map (algebraMap R I.ResidueField) r = s • x
hx : r ∈ J
⊢ Eq.{u_1 + 1} (α := I.ResidueField[X])
    ((fun (x : I.ResidueField[X]) ↦
        HMul.hMul (α := I.ResidueField[X])
          ((C : (a : I.ResidueField) → I.ResidueField[X]) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) s) :
            I.ResidueField[X])
          x)
      x)
    ((fun (x : I.ResidueField[X]) ↦
        HMul.hMul (α := I.ResidueField[X])
          ((C : (a : I.ResidueField) → I.ResidueField[X]) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) s) :
            I.ResidueField[X])
          x)
      0)
have refine_1 : map (algebraMap R I.ResidueField) r = HSMul.hSMul (β := I.ResidueField[X]) s 0
Tactic: simp only [← algebraMap_eq, ← Algebra.smul_def, algebraMap_smul, ← hr]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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 →ₐ[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))
have refine_2 : Eq (α := RatFunc I.ResidueField →+* RatFunc I.ResidueField)
  (↑(AlgHom.comp { toRingHom := f, commutes' := sorry }
        (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) sorry)) :
    RatFunc I.ResidueField →+* RatFunc I.ResidueField)
  (↑(AlgHom.id I.ResidueField (RatFunc I.ResidueField)) : RatFunc I.ResidueField →+* RatFunc I.ResidueField)
Tactic: apply AlgHom.coe_ringHom_injective
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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 →+* 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)
have 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' := sorry }
          (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) sorry)) :
      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))
Tactic: apply IsFractionRing.injective_comp_algebraMap (A := I.ResidueField[X])
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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 (α := 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)))
have 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)))
      sorry sorry)
    (↑(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: simp only [AlgHom.comp_toRingHom, AlgHom.coe_ringHom_mk, RingHom.comp_assoc,
      RatFunc.liftRingHom_comp_algebraMap, RingHomCompTriple.comp_eq, f]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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 (α := 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))
have 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)))
                  sorry sorry)
                (↑(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: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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 →ₐ[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)
have refine_3 : Eq (α := J.ResidueField →+* J.ResidueField)
  (↑(AlgHom.comp (RatFunc.liftAlgHom (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X)) sorry)
          { toRingHom := f, commutes' := sorry } :
        J.ResidueField →ₐ[I.ResidueField] J.ResidueField) :
    J.ResidueField →+* J.ResidueField)
  (↑(AlgHom.id I.ResidueField J.ResidueField) : J.ResidueField →+* J.ResidueField)
Tactic: apply AlgHom.coe_ringHom_injective
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
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 →+* 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)
have 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)) sorry)
                      { toRingHom := f, commutes' := sorry } :
                    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: ext