-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R[X]
i : R →+* ↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' :
  Membership.mem (α := R[X] ⧸ I) (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C))
    ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y : R[X] ⧸ I)
hx :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (map (F := R[X] →+* (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        (Subtype.mk (p := fun (x : R[X] ⧸ I) ↦
          Membership.mem (γ := Subring (R[X] ⧸ I)) (RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)) x)
          ((RingHom.comp (Quotient.mk I) C : (a : R) → R[X] ⧸ I) y) hx') :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
this :
  Membership.mem (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (γ :=
    Ideal (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (map (mapRingHom i) I)
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
f : R[X]
hf :
  f ∈ (↑I : Set R[X]) ∧
    Eq (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X]) f :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
          ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
rw :
  Eq (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X])
        (HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) f) :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    (0 : (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
rw₁ :
  HSub.hSub (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (β :=
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X]) ((C : (a : R) → R[X]) y) :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
      ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X]) f :
        (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) =
    0
⊢ Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i))
    (HSub.hSub (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) f)
have rw₂ : HSub.hSub (α := (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) (β :=
    (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    ((mapRingHom i : (a : R[X]) → (↥((Quotient.mk I).comp C).range)[X]) ((C : (a : R) → R[X]) y) :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X])
    ((C : (a : ↥((Quotient.mk I).comp C).range) → (↥((Quotient.mk I).comp C).range)[X])
        ((i : (a : R) → ↥((Quotient.mk I).comp C).range) y) :
      (↥(RingHom.range (R := R) (RingHom.comp (Quotient.mk I) C)))[X]) =
  0
Tactic: rw [RingHom.mem_ker, map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]