-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
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_1 : 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
r : ↥s
this :
  Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj.{vJ, u, uJ, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (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)))
          i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    c))
                i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget CommRingCat).mapCocone c).pt).obj i))
          ((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)) :
        (fun (X : Type u) ↦ X)
          (Functor.obj.{vJ, u, uJ, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (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)))
            i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    c))
                i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget CommRingCat).mapCocone c).pt).obj i))
          0 :
        (fun (X : Type u) ↦ X)
          (Functor.obj.{vJ, u, uJ, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (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)))
            i)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α :=
        (fun (X : Type u) ↦ X)
          ((F ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier)).obj
            k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier)).map
                  f) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj k))
            ((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)) :
          (fun (X : Type u) ↦ X)
            ((F ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).obj
              k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier)).map
                  g) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj k))
            0 :
          (fun (X : Type u) ↦ X)
            ((F ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).obj
              k))
H :
  Eq (α := (↑(Functor.obj.{vJ, u, uJ, u + 1} (Functor.obj (Functor.const J) c.pt) i) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (g' ≫ c.ι.app i) :
          (a : (↑P : Type u)) → (↑(((Functor.const J).obj c.pt).obj i) : Type u))
        (↑r : (↑P : Type u)) :
      (↑(Functor.obj.{vJ, u, uJ, u + 1} (Functor.obj (Functor.const J) c.pt) i) : Type u))
    (0 : (↑(Functor.obj.{vJ, u, uJ, u + 1} (Functor.obj (Functor.const J) c.pt) i) : Type u))
obtain :
  ∀ (k : J) (f g : i ⟶ k)
    (e :
      Eq (α :=
        (fun (X : Type u) ↦ X)
          ((F ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier)).obj
            k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier)).map
                  f) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj k))
            ((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)) :
          (fun (X : Type u) ↦ X)
            ((F ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).obj
              k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier)).map
                  g) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj k))
            0 :
          (fun (X : Type u) ↦ X)
            ((F ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).obj
              k))),
    ∃ (i' : J) (hi' : i ⟶ i'),
      Eq (α := (↑(F.obj i') : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (F.map hi') :
              (a : (↑(F.obj i) : Type u)) → (↑(F.obj i') : 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') : Type u))
        (0 : (↑(F.obj i') : Type u))
⊢ ∃ (i' : J) (hi' : i ⟶ i'),
    Eq (α := (↑(F.obj i') : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.map hi') :
            (a : (↑(F.obj i) : Type u)) → (↑(F.obj i') : 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') : Type u))
      (0 : (↑(F.obj i') : Type u))

Tactic:
obtain ⟨k, f, g, e⟩ := this.mp (by simpa using H)

Premises used: Iff.mp