-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
g : S ⟶ c.pt
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn :
  ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f.toRingHom)
hπ :
  Function.Surjective (α := (↑P : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) π) :
      (a : (↑P : Type u)) → (↑S : Type u))
s : Finset (↑P : Type u)
hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : (r : ↥s) → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' :
  ∀ (r : ↥s),
    Eq (α := (↑(F.obj (i' r)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.map (hi' r)) :
            (a : (↑(F.obj i) : Type u)) → (↑(F.obj (i' r)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) g' :
                (a : (↑P : Type u)) → (↑(F.obj i) : Type u))
              (↑r : (↑P : Type u)) :
            (↑(F.obj i) : Type u)) :
        (↑(F.obj (i' r)) : Type u))
      (0 : (↑(F.obj (i' r)) : Type u))
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : (↑P : Type u)
⊢ Eq (α := (↑c.pt : Type u))
    ((CommRingCat.Hom.hom g : (a : (↑S : Type u)) → (↑c.pt : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) π :
              (a : (↑P : Type u)) → (↑S : Type u))
            x :
          (↑S : Type u)) :
      (↑c.pt : Type u))
    (((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                  (((CommRingCat.Hom.hom π).liftOfSurjective hπ :
                      (a : { g : (↑P : Type u) →+* (↑(F.1 c'.pt) : Type u) // ker (CommRingCat.Hom.hom π) ≤ ker g }) →
                        (↑S : Type u) →+* (↑(F.1 c'.pt) : Type u))
                    (Subtype.mk (p := fun (g : (↑P : Type u) →+* (↑(F.1 c'.pt) : Type u)) ↦
                      LE.le (α := Ideal (↑P : Type u)) (ker (CommRingCat.Hom.hom π)) (ker g))
                      (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none))) ⋯)) ≫
                c.ι.app c'.pt) :
            (↑S : Type u) →+* (↑c.pt : Type u)) :
          (a : (↑S : Type u)) → (↑c.pt : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) π :
              (a : (↑P : Type u)) → (↑S : Type u))
            x :
          (↑S : Type u)) :
      (↑c.pt : Type u))
have refine_3 : Eq (α := (↑c.pt : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (π ≫ g) :
        (a : (↑P : Type u)) → (↑c.pt : Type u))
      x :
    (↑c.pt : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y :=
          Functor.obj.{vJ, u, uJ, u + 1} (Functor.obj (Functor.const J) c.pt)
            (Functor.obj.{u, vJ, u, uJ} (C := WidePushoutShape ↥s)
              (Functor.obj (Functor.const (WidePushoutShape ↥s)) c'.pt) none))
          (g' ≫
            F.map (c'.ι.app none) ≫
              c.ι.app
                (Functor.obj.{u, vJ, u, uJ} (C := WidePushoutShape ↥s)
                  (Functor.obj (Functor.const (WidePushoutShape ↥s)) c'.pt) none)) :
        (a : (↑P : Type u)) →
          (↑(((Functor.const J).obj c.pt).obj (((Functor.const (WidePushoutShape ↥s)).obj c'.pt).obj none)) : Type u))
      x :
    (↑(Functor.obj.{vJ, u, uJ, u + 1} (Functor.obj (Functor.const J) c.pt)
          (Functor.obj.{u, vJ, u, uJ} (C := WidePushoutShape ↥s)
            (Functor.obj (Functor.const (WidePushoutShape ↥s)) c'.pt) none)) :
      Type u))
Tactic: suffices (π ≫ g) x = (g' ≫ F.map (c'.ι.app none) ≫ c.ι.app _) x by
      simpa only [CommRingCat.hom_comp, CommRingCat.hom_ofHom,
        RingHom.liftOfRightInverse_comp_apply, coe_comp, Function.comp_apply] using this