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))
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)
refine_1 : ∀ (r : R[X]) (hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x), x = 0
⊢ x = 0

Tactic:
obtain ⟨r, hr⟩ := map_surjective _ Ideal.Quotient.mk_surjective
      (IsLocalization.integerNormalization (R ⧸ I)⁰ x)

Premises used: Polynomial.map_surjective, nonZeroDivisors, Ideal.Quotient.mk_surjective, HasQuotient.Quotient, IsLocalization.integerNormalization
-- 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_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
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
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x

Tactic:
obtain ⟨b, hb0, hb⟩ := IsLocalization.integerNormalization_spec (R ⧸ I)⁰ x

Premises used: nonZeroDivisors, HasQuotient.Quotient, IsLocalization.integerNormalization_spec
-- 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_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
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
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x

Tactic:
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective b

Premises used: Ideal.Quotient.mk_surjective, 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))
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

Tactic:
simpa [Ideal.Quotient.eq_zero_iff_mem] using hb0

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- 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_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
refine : map (algebraMap R I.ResidueField) r = s • x
⊢ ∃ s ∉ I, map (algebraMap R I.ResidueField) r = s • x

Tactic:
refine ⟨s, by simpa [Ideal.Quotient.eq_zero_iff_mem] using hb0, ?_⟩
-- 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_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
⊢ map (algebraMap R I.ResidueField) r = s • x

Tactic:
simpa [← hr, map_map, ← Ideal.Quotient.algebraMap_eq] using hb

Premises used: Ideal.Quotient.algebraMap_eq, Polynomial.map_map
-- 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_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
refine_1 : ∀ (s : R) (hs : s ∉ I) (hr : map (algebraMap R I.ResidueField) r = s • x), x = 0
⊢ 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

Premises used: Algebra.algebraMap, Polynomial.map
-- 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_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
⊢ 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

Premises used: Algebra.algebraMap, Ideal.ResidueField, Polynomial, Polynomial.aeval, Polynomial.X, DFunLike.coe
-- 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_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 :
  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)
⊢ r ∈ J

Tactic:
simpa [hx, aeval_map_algebraMap, aeval_algebraMap_apply, Algebra.smul_def] using hr

Premises used: Polynomial.aeval_map_algebraMap, Algebra.smul_def, Polynomial.aeval_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_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

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
-- 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_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
⊢ Ne (α := I.ResidueField) ((algebraMap R I.ResidueField : (a : R) → I.ResidueField) s : I.ResidueField)
    (0 : I.ResidueField)

Tactic:
simpa
-- 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_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
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)
⊢ x = 0

Tactic:
refine ((IsUnit.mk0 (algebraMap R I.ResidueField s) (by simpa)).map C).mul_right_injective ?_

Premises used: Polynomial.C, Algebra.algebraMap, Ideal.ResidueField, IsUnit.mul_right_injective, IsUnit.mk0, IsUnit.map, DFunLike.coe
-- 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_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
refine_1 : map (algebraMap R I.ResidueField) r = HSMul.hSMul (β := I.ResidueField[X]) s 0
⊢ 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:
simp only [← algebraMap_eq, ← Algebra.smul_def, algebraMap_smul, ← hr]

Premises used: algebraMap_smul, Algebra.smul_def, Polynomial.algebraMap_eq
-- 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_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
⊢ map (algebraMap R I.ResidueField) r = HSMul.hSMul (β := I.ResidueField[X]) s 0

Tactic:
simpa [Polynomial.ext_iff, Ideal.mem_map_C_iff] using hJ.le hx

Premises used: Polynomial.ext_iff, Eq.le, Ideal.mem_map_C_iff