-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Quotient (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I)
f : R[X]
mk :
  ∀ (p q : R[X]),
    Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
        ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
              (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
            ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
                (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
              (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) p)) :
          HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
        (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) p :
          Quot (α := R[X]) (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop)) →
      Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
          ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                  ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
                (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
              ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
                  (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
                (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) q)) :
            HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
          (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) q :
            Quot (α := R[X]) (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop)) →
        Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
          ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
                  ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
                (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
              ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
                  (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
                (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) (p + q))) :
            HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
          (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) (p + q) :
            Quot (α := R[X]) (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop))
⊢ Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) ⋯)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) ⋯ :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) f)) :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) f :
      Quot (α := R[X]) (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop))
have mk₁ : ∀ (n : ℕ) (a : R),
  Eq (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    ((eval₂RingHom (Quotient.lift I (RingHom.comp (Quotient.mk (map (F := R →+* R[X]) C I)) C) sorry)
            ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) X) :
          (a : (R ⧸ I)[X]) → R[X] ⧸ map C I)
        ((Quotient.lift (map (F := R →+* R[X]) C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) sorry :
            (a : R[X] ⧸ map C I) → (R ⧸ I)[X])
          (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) ((monomial n : (a : R) → R[X]) a))) :
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
    (Quot.mk (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop) ((monomial n : (a : R) → R[X]) a) :
      Quot (α := R[X]) (⇑(Submodule.quotientRel (map C I)) : R[X] → R[X] → Prop))
Tactic: refine Polynomial.induction_on' f ?_ ?_