-- Module: Mathlib.RingTheory.Polynomial.Quotient
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 p q : R[X]
hp :
  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))
hq :
  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))
mk :
  eval₂ (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)
        (eval₂ (RingHom.comp C (Quotient.mk I)) X p) +
      eval₂ (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)
        (eval₂ (RingHom.comp C (Quotient.mk I)) X q) =
    HAdd.hAdd (α := HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I)) (β :=
      HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
      ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) p :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
      ((Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) q :
        HasQuotient.Quotient R[X] (B := Ideal R[X]) (map (F := R →+* R[X]) C I))
⊢ 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))

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, map_add, Quotient.lift_mk,
        coe_eval₂RingHom] at hp hq ⊢

Premises used: map_add, Ideal.Quotient.lift_mk, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk, Polynomial.coe_eval₂RingHom