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
f : R[X] →ₐ[R] S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑f : (a : R[X]) → S)
p : Ideal R
inst_3 : p.IsPrime
a : p.ResidueField
b : R[X]
⊢ Eq.{u_1 + 1} (α :=
    HasQuotient.Quotient p.ResidueField[X] (B := Ideal p.ResidueField[X])
      (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField))
        (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S))))
    ((fiberEquivQuotient f hf p :
          (a : p.Fiber S) →
            p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker (↑f : R[X] →+* S)))
        (a ⊗ₜ[R] (f : (a : R[X]) → S) b) :
      HasQuotient.Quotient p.ResidueField[X] (B := Ideal p.ResidueField[X])
        (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField))
          (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S))))
    ((Ideal.Quotient.mk
            (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField))
              (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S))) :
          (a : p.ResidueField[X]) →
            p.ResidueField[X] ⧸ Ideal.map (mapRingHom (algebraMap R p.ResidueField)) (RingHom.ker (↑f : R[X] →+* S)))
        (HMul.hMul (α := p.ResidueField[X]) (β := p.ResidueField[X])
          ((C : (a : p.ResidueField) → p.ResidueField[X]) a : p.ResidueField[X])
          (map (algebraMap R p.ResidueField) b)) :
      HasQuotient.Quotient p.ResidueField[X] (B := Ideal p.ResidueField[X])
        (Ideal.map (F := R[X] →+* p.ResidueField[X]) (mapRingHom (algebraMap R p.ResidueField))
          (RingHom.ker (F := RingHom.{u_1, u_2} R[X] S) (↑f : R[X] →+* S))))

Tactic:
simp [fiberEquivQuotient, ← Ideal.Quotient.mk_algebraMap]

Premises used: Polynomial.fiberEquivQuotient, Ideal.Quotient.mk_algebraMap
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R
inst_1 : P.IsPrime
I : Ideal R[X]
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)
⊢ ∃ 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)

Premises used: inferInstance, Ideal.span
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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))
⊢ IsLocalization (Submonoid.map (F := R ⧸ P →+* (R ⧸ P)[X]) C (R ⧸ P)⁰) P.ResidueField[X]

Tactic:
have := Polynomial.isLocalization (R ⧸ P)⁰ P.ResidueField
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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]
rw : Membership.mem (γ := Ideal P.ResidueField[X]) (Ideal.span {p}) p
⊢ 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:
rw [Ideal.map_map, RingHom.algebraMap_toAlgebra, mapRingHom_comp,
      ← IsScalarTower.algebraMap_eq, hp]

Premises used: Ideal.map_map, IsScalarTower.algebraMap_eq, RingHom.algebraMap_toAlgebra, Polynomial.mapRingHom_comp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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.span {p}) p

Tactic:
Ideal.mem_span_singleton_self _

Premises used: Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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.span {p}) p

Tactic:
exact Ideal.mem_span_singleton_self _

Premises used: Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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

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 _
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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
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)
⊢ ∃ 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

Premises used: Polynomial.C, nonZeroDivisors, Submonoid.map, HasQuotient.Quotient, Iff.mp, IsLocalization.mem_map_algebraMap_iff
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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 * 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

Premises used: Polynomial.algebraMap_def, Polynomial.coe_mapRingHom, IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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)

Tactic:
⟨r, hr', le_antisymm ?_ ?_⟩

Premises used: le_antisymm, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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)
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})
⊢ ∃ 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:
refine ⟨r, hr', le_antisymm ?_ ?_⟩
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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.span {map (algebraMap R P.ResidueField) r})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)

Tactic:
simpa [-le_of_subsingleton, Ideal.span_le] using Ideal.mem_map_of_mem _ hr'

Premises used: Ideal.span_le, Ideal.mem_map_of_mem, le_of_subsingleton
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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_2 : Membership.mem (γ := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) r}) p
⊢ 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:
simp only [hp, Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe]

Premises used: Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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_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])) ⋯)⁻¹ :
        P.ResidueField[X]))
⊢ Membership.mem (γ := Ideal P.ResidueField[X]) (Ideal.span {map (algebraMap R P.ResidueField) r}) p

Tactic:
rw [(IsLocalization.map_units P.ResidueField[X] s).unit.eq_mul_inv_iff_mul_eq.mpr e]

Premises used: Iff.mpr, Ideal.ResidueField, Polynomial, Units.eq_mul_inv_iff_mul_eq, IsLocalization.map_units, IsUnit.unit
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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})
    (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])) ⋯)⁻¹ :
        P.ResidueField[X]))

Tactic:
Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _)

Premises used: Set.Mem, Ideal.mul_mem_right, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial
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})
    (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])) ⋯)⁻¹ :
        P.ResidueField[X]))

Tactic:
exact Ideal.mul_mem_right _ _ (Ideal.mem_span_singleton_self _)

Premises used: Ideal.mul_mem_right, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
F : Type u_4
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
inst_4 : IsLocalHom.{u_1, u_2, u_4} (R := R) (S := S) f
⊢ IsLocalHom (R := R) (S := S) (F := R →+* S) (↑f : R →+* S)

Tactic:
⟨IsLocalHom.map_nonunit (f := f)⟩

Premises used: IsLocalHom.map_nonunit, IsLocalHom.mk