-- 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 ⧸ 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)
have 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)
Tactic: obtain ⟨r, hr', rfl⟩ := (Ideal.mem_map_iff_of_surjective _
    (Polynomial.map_surjective _ Ideal.Quotient.mk_surjective)).mp hr
Cleared hypotheses: r, hr, e