-- Lean 4 proof step from Mathlib.RingTheory.Ideal.GoingUp (goal)
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
⊢ Eq (α :=
    R →+*
      HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
        Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
          (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
    (@RingHom.comp _ (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) _ _
      Semiring.toNonAssocSemiring _
      (RingHom.comp
        (Quotient.mk
          (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
            (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
        C)
      (Quotient.mk (comap (F := R →+* R[X]) C P)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (quotientMap
        (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
          (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P)
        (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) ⋯)
      (RingHom.comp (Quotient.mk P) C))
have a : ∀ (x : R),
  Eq (α :=
    HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
      Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
      (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
    ((@RingHom.comp _ (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) _ _
            Semiring.toNonAssocSemiring _
            (RingHom.comp
              (Quotient.mk
                (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
                  (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
              C)
            (Quotient.mk (comap (F := R →+* R[X]) C P)) :
          (a : R) → (R ⧸ comap C P)[X] ⧸ map (mapRingHom (Quotient.mk (comap C P))) P)
        x :
      HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
        Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
          (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (quotientMap
              (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
                (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P)
              (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) sorry)
            (RingHom.comp (Quotient.mk P) C) :
          (a : R) → (R ⧸ comap C P)[X] ⧸ map (mapRingHom (Quotient.mk (comap C P))) P)
        x :
      HasQuotient.Quotient (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X] (B :=
        Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (map (F := R[X] →+* (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
          (mapRingHom (Quotient.mk (comap (F := R →+* R[X]) C P))) P))
Tactic: ext