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))
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)
⊢ 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₁ : Eq (α := J.ResidueField)
  ((@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) :
        (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: 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))
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)
have 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)
Tactic: simp [f, RatFunc.liftAlgHom, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
⊢ ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
have obtain : ∀ (p : P.ResidueField[X])
  (hp :
    Eq (α := Ideal P.ResidueField[X])
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})),
  ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
Tactic: obtain ⟨p, hp : _ = Ideal.span _⟩ := (inferInstance :
    (I.map (mapRingHom (algebraMap R P.ResidueField))).IsPrincipal)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
⊢ ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
have this₁ : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
Tactic: have := Polynomial.isLocalization (R ⧸ P)⁰ P.ResidueField
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
⊢ Membership.mem (γ := Ideal P.ResidueField[X])
    (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
      (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
    p
have rw : Membership.mem (γ := Ideal P.ResidueField[X]) (Ideal.span {p}) p
Tactic: rw [Ideal.map_map, RingHom.algebraMap_toAlgebra, mapRingHom_comp,
      ← IsScalarTower.algebraMap_eq, hp]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
⊢ ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
have this₁ : Membership.mem (γ := Ideal P.ResidueField[X])
  (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
    (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
  p
Tactic: have : p ∈ (I.map (mapRingHom (algebraMap R (R ⧸ P)))).map (algebraMap _ _) := by
    rw [Ideal.map_map, RingHom.algebraMap_toAlgebra, mapRingHom_comp,
      ← IsScalarTower.algebraMap_eq, hp]
    exact Ideal.mem_span_singleton_self _
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this_2 : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
this :
  Membership.mem (γ := Ideal P.ResidueField[X])
    (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
      (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
    p
⊢ ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
have obtain : ∀ (s : ↥(Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰)) (r : (R ⧸ P)[X])
  (hr :
    Membership.mem (γ := Ideal (R ⧸ P)[X]) (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I)
      r)
  (e :
    HMul.hMul (β := P.ResidueField[X]) p
        ((algebraMap (R ⧸ P)[X] P.ResidueField[X] : (a : (R ⧸ P)[X]) → P.ResidueField[X])
            (↑(Subtype.mk (p := fun (x : (R ⧸ P)[X]) ↦
                      Membership.mem (γ := Ideal (R ⧸ P)[X])
                        (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I) x)
                      r hr,
                    s).2 :
              (R ⧸ P)[X]) :
          P.ResidueField[X]) =
      (algebraMap (R ⧸ P)[X] P.ResidueField[X] : (a : (R ⧸ P)[X]) → P.ResidueField[X])
        (↑(Subtype.mk (p := fun (x : (R ⧸ P)[X]) ↦
                  Membership.mem (γ := Ideal (R ⧸ P)[X])
                    (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I) x)
                  r hr,
                s).1 :
          (R ⧸ P)[X])),
  ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
Tactic: obtain ⟨⟨⟨r, hr⟩, s⟩, e⟩ := (IsLocalization.mem_map_algebraMap_iff ((R ⧸ P)⁰.map C) _).mp this
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this_2 : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
this :
  Membership.mem (γ := Ideal P.ResidueField[X])
    (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
      (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
    p
s : ↥(Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr :
  Membership.mem (α := (R ⧸ P)[X]) (γ := Ideal (R ⧸ P)[X])
    (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I)
    ((mapRingHom (algebraMap R (R ⧸ P)) : (a : R[X]) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
e :
  HMul.hMul (β := P.ResidueField[X]) p
      ((algebraMap (R ⧸ P)[X] P.ResidueField[X] : (a : (R ⧸ P)[X]) → P.ResidueField[X])
          (↑((Subtype.mk (p := fun (x : (R ⧸ P)[X]) ↦
                      Membership.mem (γ := Ideal (R ⧸ P)[X])
                        (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I) x)
                      ((mapRingHom (algebraMap R (R ⧸ P)) : (a : R[X]) → (R ⧸ P)[X]) r) hr,
                    s) :
                  ↥(Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I) ×
                    ↥(Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰)).2 :
            (R ⧸ P)[X]) :
        P.ResidueField[X]) =
    (algebraMap (R ⧸ P)[X] P.ResidueField[X] : (a : (R ⧸ P)[X]) → P.ResidueField[X])
      (↑(Subtype.mk (p := fun (x : (R ⧸ P)[X]) ↦
                Membership.mem (γ := Ideal (R ⧸ P)[X])
                  (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I) x)
                ((mapRingHom (algebraMap R (R ⧸ P)) : (a : R[X]) → (R ⧸ P)[X]) r) hr,
              s).1 :
        (R ⧸ P)[X])
⊢ ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
have e₁ : p * map (algebraMap (R ⧸ P) P.ResidueField) (↑s : (R ⧸ P)[X]) = map (algebraMap R P.ResidueField) r
Tactic: simp only [algebraMap_def, coe_mapRingHom,
    Polynomial.map_map, ← IsScalarTower.algebraMap_eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this_2 : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
this :
  Membership.mem (γ := Ideal P.ResidueField[X])
    (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
      (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
    p
s : ↥(Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr :
  Membership.mem (α := (R ⧸ P)[X]) (γ := Ideal (R ⧸ P)[X])
    (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I)
    ((mapRingHom (algebraMap R (R ⧸ P)) : (a : R[X]) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
e : p * map (algebraMap (R ⧸ P) P.ResidueField) (↑s : (R ⧸ P)[X]) = map (algebraMap R P.ResidueField) r
⊢ ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
have refine_1 : LE.le (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) r})
  (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
Tactic: refine ⟨r, hr', le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this_2 : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
this :
  Membership.mem (γ := Ideal P.ResidueField[X])
    (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
      (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
    p
s : ↥(Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr :
  Membership.mem (α := (R ⧸ P)[X]) (γ := Ideal (R ⧸ P)[X])
    (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I)
    ((mapRingHom (algebraMap R (R ⧸ P)) : (a : R[X]) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
e : p * map (algebraMap (R ⧸ P) P.ResidueField) (↑s : (R ⧸ P)[X]) = map (algebraMap R P.ResidueField) r
refine_1 :
  LE.le (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) r})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
⊢ ∃ p ∈ I,
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
have refine_2 : LE.le (α := Ideal P.ResidueField[X])
  (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
  (Ideal.span {map (algebraMap R P.ResidueField) r})
Tactic: refine ⟨r, hr', le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this_2 : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
this :
  Membership.mem (γ := Ideal P.ResidueField[X])
    (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
      (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
    p
s : ↥(Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr :
  Membership.mem (α := (R ⧸ P)[X]) (γ := Ideal (R ⧸ P)[X])
    (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I)
    ((mapRingHom (algebraMap R (R ⧸ P)) : (a : R[X]) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
e : p * map (algebraMap (R ⧸ P) P.ResidueField) (↑s : (R ⧸ P)[X]) = map (algebraMap R P.ResidueField) r
⊢ LE.le (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (Ideal.span {map (algebraMap R P.ResidueField) r})
have refine_2 : Membership.mem (γ := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) r}) p
Tactic: simp only [hp, Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.ResidueField.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
p : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I) (Ideal.span {p})
this_1 : Algebra (R ⧸ P)[X] P.ResidueField[X] := RingHom.toAlgebra (mapRingHom (algebraMap (R ⧸ P) P.ResidueField))
this_2 : IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]
this :
  Membership.mem (γ := Ideal P.ResidueField[X])
    (Ideal.map (R := (R ⧸ P)[X]) (F := (R ⧸ P)[X] →+* P.ResidueField[X]) (algebraMap (R ⧸ P)[X] P.ResidueField[X])
      (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I))
    p
s : ↥(Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰)
r : R[X]
hr' : r ∈ I
hr :
  Membership.mem (α := (R ⧸ P)[X]) (γ := Ideal (R ⧸ P)[X])
    (Ideal.map (F := R[X] →+* (R ⧸ P)[X]) (mapRingHom (algebraMap R (R ⧸ P))) I)
    ((mapRingHom (algebraMap R (R ⧸ P)) : (a : R[X]) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
e : p * map (algebraMap (R ⧸ P) P.ResidueField) (↑s : (R ⧸ P)[X]) = map (algebraMap R P.ResidueField) r
⊢ Membership.mem (γ := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) r}) p
have refine_2 : Membership.mem (γ := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) r})
  (HMul.hMul (α := P.ResidueField[X]) (map (algebraMap R P.ResidueField) r)
    (↑(IsUnit.unit (a :=
            (algebraMap (R ⧸ P)[X] P.ResidueField[X] : (a : (R ⧸ P)[X]) → P.ResidueField[X]) (↑s : (R ⧸ P)[X])) sorry)⁻¹ :
      P.ResidueField[X]))
Tactic: rw [(IsLocalization.map_units P.ResidueField[X] s).unit.eq_mul_inv_iff_mul_eq.mpr e]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
⊢ IsLocalRing R
have this : Nontrivial R
Tactic: haveI : Nontrivial R := f.domain_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
this : Nontrivial R
⊢ IsLocalRing R
have h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
Tactic: apply IsLocalRing.of_nonunits_add
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
this : Nontrivial R
a b : R
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
have h : Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) a : S) →
  Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) b : S) →
    HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ nonunits S
Tactic: simp_rw [← map_mem_nonunits_iff f, f.map_add]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
⊢ [IsLocalHom (R := R) (S := S) f, (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S),
      LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S),
      LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S)),
      Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)].TFAE
have tfae_1_to_2 : ∀ (a : IsLocalHom (R := R) (S := S) f), (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
Tactic: tfae_have 1 → 2
  | _, _, ⟨a, ha, rfl⟩ => map_nonunit f a ha
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
⊢ [IsLocalHom (R := R) (S := S) f, (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S),
      LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S),
      LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S)),
      Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)].TFAE
have tfae_2_to_4 : ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
  LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
Tactic: tfae_have 2 → 4 := Set.image_subset_iff.1