-- 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 ⧸ 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])
obtain :
  ∀ (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)
⊢ ∃ 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', rfl⟩ := (Ideal.mem_map_iff_of_surjective _
    (Polynomial.map_surjective _ Ideal.Quotient.mk_surjective)).mp hr

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl