-- 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 p q : R[X]
hp :
  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) =
    (Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) p
hq :
  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) =
    (Quotient.mk (map (F := R →+* R[X]) C I) : (a : R[X]) → R[X] ⧸ map C I) q
mk :
  HAdd.hAdd (α := 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))
      (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))
⊢ 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))
have mk₁ : 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)) =
  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))
Tactic: rw [hp, hq]