-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
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))) ⋯)
              (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))
⊢ 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))

Tactic:
ext