awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Module.Finite R k
rw : Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (RingHom.ker (F := R →+* k) (algebraMap R k))
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (maximalIdeal R)
have rw₁ : Eq (α := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)
Tactic: rw [← eq_maximalIdeal (Algebra.ker_algebraMap_isMaximal_of_isIntegral R k), RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Instances (goal)
Goal:
R_1 : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R_1
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R_1 A
inst_4 : Algebra A B
inst_5 : Algebra R_1 B
inst_6 : IsScalarTower R_1 A B
p : Ideal A
q : Ideal B
inst_7 : q.LiesOver p
R : Type u_4
k : Type u_5
inst_8 : CommRing R
inst_9 : IsLocalRing R
inst_10 : Field k
inst_11 : Algebra R k
inst_12 : Module.Finite R k
⊢ Eq (α := RingHom.{u_4, u_5} (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) k)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (ResidueField R) k)
      (↑(Ideal.quotEquivOfEq ⋯) : R ⧸ Ideal.comap (algebraMap R k) ⊥ →+* ResidueField R))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.quotientBot k) : k ⧸ ⊥ →+* k)
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
        (HasQuotient.Quotient k (B := Ideal k) ⊥)))
have h : ∀ (x : R),
  Eq.{u_5 + 1} (α := k)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap (ResidueField R) k)
              (↑(Ideal.quotEquivOfEq sorry) : R ⧸ Ideal.comap (algebraMap R k) ⊥ →+* ResidueField R))
            (Ideal.Quotient.mk (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) :
          (a : R) → k)
        x :
      k)
    ((RingHom.comp (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(RingEquiv.quotientBot k) : k ⧸ ⊥ →+* k)
              (algebraMap (HasQuotient.Quotient R (B := Ideal R) (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥))
                (HasQuotient.Quotient k (B := Ideal k) ⊥)))
            (Ideal.Quotient.mk (Ideal.comap (F := R →+* k) (algebraMap R k) ⊥)) :
          (a : R) → k)
        x :
      k)
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
⊢ J.ResidueField →+* RatFunc I.ResidueField
have refine_1 : J ≤
  RingHom.ker (F := R[X] →+* RatFunc I.ResidueField)
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
Tactic: refine Ideal.ResidueField.lift _
        ((algebraMap I.ResidueField[X] _).comp (mapRingHom (algebraMap _ _))) ?_ ?_
-- 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
refine_1 :
  J ≤
    RingHom.ker (F := R[X] →+* RatFunc I.ResidueField)
      (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
        (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
⊢ J.ResidueField →+* RatFunc I.ResidueField
have refine_2 : J.primeCompl ≤
  Submonoid.comap (F := R[X] →+* RatFunc I.ResidueField)
    (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
      (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
    (IsUnit.submonoid (RatFunc I.ResidueField))
Tactic: refine Ideal.ResidueField.lift _
        ((algebraMap I.ResidueField[X] _).comp (mapRingHom (algebraMap _ _))) ?_ ?_
-- 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
x : R[X]
hx : x ∉ J
⊢ Membership.mem (γ := Submonoid R[X])
    (Submonoid.comap (F := R[X] →+* RatFunc I.ResidueField)
      (@RingHom.comp _ I.ResidueField[X] _ _ Semiring.toNonAssocSemiring _
        (algebraMap I.ResidueField[X] (RatFunc I.ResidueField)) (mapRingHom (algebraMap R I.ResidueField)))
      (IsUnit.submonoid (RatFunc I.ResidueField)))
    x
have refine_2 : ∃ (i : ℕ), x.coeff i ∉ I
Tactic: suffices ∃ i, x.coeff i ∉ I by simpa [IsUnit.mem_submonoid_iff, Polynomial.ext_iff]
-- 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
x : R[X]
hx : x ∉ J
⊢ ∃ (i : ℕ), x.coeff i ∉ I
have refine_2 : ∀ (hx : ∀ (i : ℕ), x.coeff i ∈ I), x ∈ J
Tactic: contrapose! hx
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
x : R[X]
hx : ∀ (i : ℕ), x.coeff i ∈ I
⊢ x ∈ J
have refine_2 : Membership.mem (γ := Ideal R[X]) (Ideal.map (F := R →+* R[X]) C I) x
Tactic: rwa [hJ, Ideal.mem_map_C_iff]
-- 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)))
    ⋯ ⋯
⊢ Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
    (algebraMap I.ResidueField (RatFunc I.ResidueField))
have H : ∀ (x : R),
  Eq (α := RatFunc I.ResidueField)
    ((@RingHom.comp _ I.ResidueField _ _ Semiring.toNonAssocSemiring _
            (f.comp (algebraMap I.ResidueField J.ResidueField)) (algebraMap R I.ResidueField) :
          (a : R) → RatFunc I.ResidueField)
        x :
      RatFunc I.ResidueField)
    ((@RingHom.comp _ I.ResidueField _ _ Semiring.toNonAssocSemiring _
            (algebraMap I.ResidueField (RatFunc I.ResidueField)) (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 (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)))
    ⋯ ⋯
⊢ J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField
have hf : Eq (α := I.ResidueField →+* RatFunc I.ResidueField) (f.comp (algebraMap I.ResidueField J.ResidueField))
  (algebraMap I.ResidueField (RatFunc I.ResidueField))
Tactic: haveI hf : f.comp (algebraMap I.ResidueField _) = algebraMap _ _ := by
    ext
    simp [f, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R R[X] J.ResidueField]
-- 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))
⊢ J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField
have refine_1 : ∀ (x : I.ResidueField[X]),
  Membership.mem (γ := Submonoid I.ResidueField[X]) I.ResidueField[X]⁰ x →
    Membership.mem (γ := Submonoid I.ResidueField[X])
      (Submonoid.comap (F := I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        J.ResidueField⁰)
      x
Tactic: refine .ofAlgHom ⟨f, fun r ↦ congr($hf r)⟩
      (RatFunc.liftAlgHom (aeval (algebraMap R[X] _ X)) fun 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))
refine_1 :
  ∀ (x : I.ResidueField[X]),
    Membership.mem (γ := Submonoid I.ResidueField[X]) I.ResidueField[X]⁰ x →
      Membership.mem (γ := Submonoid I.ResidueField[X])
        (Submonoid.comap (F := I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
          (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
          J.ResidueField⁰)
        x
⊢ J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField
have refine_2 : Eq (α := RatFunc I.ResidueField →ₐ[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))
  (AlgHom.id I.ResidueField (RatFunc I.ResidueField))
Tactic: refine .ofAlgHom ⟨f, fun r ↦ congr($hf r)⟩
      (RatFunc.liftAlgHom (aeval (algebraMap R[X] _ X)) fun 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))
refine_1 :
  ∀ (x : I.ResidueField[X]),
    Membership.mem (γ := Submonoid I.ResidueField[X]) I.ResidueField[X]⁰ x →
      Membership.mem (γ := Submonoid I.ResidueField[X])
        (Submonoid.comap (F := I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
          (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
            I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
          J.ResidueField⁰)
        x
refine_2 :
  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))
⊢ J.ResidueField ≃ₐ[I.ResidueField] RatFunc I.ResidueField
have refine_3 : Eq (α := J.ResidueField →ₐ[I.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)
  (AlgHom.id I.ResidueField J.ResidueField : J.ResidueField →ₐ[I.ResidueField] J.ResidueField)
Tactic: refine .ofAlgHom ⟨f, fun r ↦ congr($hf r)⟩
      (RatFunc.liftAlgHom (aeval (algebraMap R[X] _ X)) fun 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))
x : I.ResidueField[X]
⊢ Membership.mem (γ := Submonoid I.ResidueField[X]) I.ResidueField[X]⁰ x →
    Membership.mem (γ := Submonoid I.ResidueField[X])
      (Submonoid.comap (F := I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        (aeval ((algebraMap R[X] J.ResidueField : (a : R[X]) → J.ResidueField) X) :
          I.ResidueField[X] →ₐ[I.ResidueField] J.ResidueField)
        J.ResidueField⁰)
      x
have refine_1 : Function.Injective.{u_1 + 1, u_1 + 1} (α := I.ResidueField[X]) (β := 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)
Tactic: suffices Function.Injective (aeval (R := I.ResidueField) (algebraMap R[X] J.ResidueField X)) by
      simp [← this.eq_iff]
-- 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 : I.ResidueField[X]
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := I.ResidueField[X]) (β := 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)
have refine_1 : ∀ (a : I.ResidueField[X]),
  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)
          a :
        J.ResidueField)
      (0 : J.ResidueField) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- 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)
⊢ x = 0
have refine_1 : ∀ (r : R[X]) (hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x), x = 0
Tactic: obtain ⟨r, hr⟩ := map_surjective _ Ideal.Quotient.mk_surjective
      (IsLocalization.integerNormalization (R ⧸ I)⁰ 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))
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 ∉ I, map (algebraMap R I.ResidueField) r = s • x
have obtain : ∀ (b : R ⧸ I) (hb0 : Membership.mem (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ b)
  (hb : map (R := R ⧸ I) (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = b • x),
  ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x
Tactic: obtain ⟨b, hb0, hb⟩ := IsLocalization.integerNormalization_spec (R ⧸ I)⁰ 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))
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
b : R ⧸ I
hb0 : Membership.mem (γ := Submonoid (R ⧸ I)) (R ⧸ I)⁰ b
hb : map (R := R ⧸ I) (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = b • x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x
have obtain : ∀ (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
Tactic: obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective b
Cleared hypotheses: b, hb0, hb