-- 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]
⊢ 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 : ∀ (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) 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) 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) 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) 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) 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) (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))
Tactic: refine Polynomial.induction_on' f ?_ ?_