-- 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
f : R ⟶ S
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))
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
have have₁ have₂ :
  ∀
    (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)),
    ∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk
have₃ have₄ have₅ :
  ∀
    (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))
    (k : (x : (↑S : Type u)) → J) (f₁ : (x : (↑S : Type u)) → i ⟶ k x) (f₂ : (x : (↑S : Type u)) → j ⟶ k x)
    (h :
      ∀ (x : (↑S : Type u)),
        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 x)))
          ((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₁ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((a.hom' : (a : (↑S : Type u)) → (↑(F.obj i) : Type u)) x : (↑(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 x)))
          ((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₂ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((b.hom' : (a : (↑S : Type u)) → (↑(F.obj j) : Type u)) x : (↑(F.obj j) : 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 x)))),
    ∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk
have₆ :
  ∀
    (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))
    (k : (x : (↑S : Type u)) → J) (f₁ : (x : (↑S : Type u)) → i ⟶ k x) (f₂ : (x : (↑S : Type u)) → j ⟶ k x)
    (h :
      ∀ (x : (↑S : Type u)),
        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 x)))
          ((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₁ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((a.hom' : (a : (↑S : Type u)) → (↑(F.obj i) : Type u)) x : (↑(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 x)))
          ((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₂ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((b.hom' : (a : (↑S : Type u)) → (↑(F.obj j) : Type u)) x : (↑(F.obj j) : 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 x)))),
    let J' :=
      { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun (x : ↥hf.finset) ↦ Sum.inl (),
        snd := fun (x : ↥hf.finset) ↦ Sum.inr () : MulticospanShape.{0, u} };
    let D : MulticospanIndex.{0, u, vJ, uJ} J' J :=
      { left := Sum.elim (fun (x : Unit) ↦ i) fun (x : Unit) ↦ j, right := fun (x : J'.R) ↦ k (↑x : (↑S : Type u)),
        fst := fun (x : J'.R) ↦ f₁ (↑x : (↑S : Type u)), snd := fun (x : J'.R) ↦ f₂ (↑x : (↑S : Type u)) };
    ∀ (c' : Cocone D.multicospan), ∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk
have₇ :
  ∀
    (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))
    (k : (x : (↑S : Type u)) → J) (f₁ : (x : (↑S : Type u)) → i ⟶ k x) (f₂ : (x : (↑S : Type u)) → j ⟶ k x)
    (h :
      ∀ (x : (↑S : Type u)),
        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 x)))
          ((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₁ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((a.hom' : (a : (↑S : Type u)) → (↑(F.obj i) : Type u)) x : (↑(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 x)))
          ((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₂ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((b.hom' : (a : (↑S : Type u)) → (↑(F.obj j) : Type u)) x : (↑(F.obj j) : 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 x)))),
    let J' :=
      { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun (x : ↥hf.finset) ↦ Sum.inl (),
        snd := fun (x : ↥hf.finset) ↦ Sum.inr () : MulticospanShape.{0, u} };
    let D : MulticospanIndex.{0, u, vJ, uJ} J' J :=
      { left := Sum.elim (fun (x : Unit) ↦ i) fun (x : Unit) ↦ j, right := fun (x : J'.R) ↦ k (↑x : (↑S : Type u)),
        fst := fun (x : J'.R) ↦ f₁ (↑x : (↑S : Type u)), snd := fun (x : J'.R) ↦ f₂ (↑x : (↑S : Type u)) };
    ∀ (c' : Cocone D.multicospan),
      Eq (α := S ⟶ F.obj c'.pt) (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))
        (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))
hf₁ :
  ∀
    (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))
    (k : (x : (↑S : Type u)) → J) (f₁ : (x : (↑S : Type u)) → i ⟶ k x) (f₂ : (x : (↑S : Type u)) → j ⟶ k x)
    (h :
      ∀ (x : (↑S : Type u)),
        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 x)))
          ((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₁ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((a.hom' : (a : (↑S : Type u)) → (↑(F.obj i) : Type u)) x : (↑(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 x)))
          ((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₂ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((b.hom' : (a : (↑S : Type u)) → (↑(F.obj j) : Type u)) x : (↑(F.obj j) : 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 x)))),
    let J' :=
      { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun (x : ↥hf.finset) ↦ Sum.inl (),
        snd := fun (x : ↥hf.finset) ↦ Sum.inr () : MulticospanShape.{0, u} };
    let D : MulticospanIndex.{0, u, vJ, uJ} J' J :=
      { left := Sum.elim (fun (x : Unit) ↦ i) fun (x : Unit) ↦ j, right := fun (x : J'.R) ↦ k (↑x : (↑S : Type u)),
        fst := fun (x : J'.R) ↦ f₁ (↑x : (↑S : Type u)), snd := fun (x : J'.R) ↦ f₂ (↑x : (↑S : Type u)) };
    ∀ (c' : Cocone D.multicospan),
      Eq (α := (↑S : Type u) →+* (↑(F.obj c'.pt) : Type u))
        (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))))
        (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ())))))
hf₂ :
  ∀
    (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))
    (k : (x : (↑S : Type u)) → J) (f₁ : (x : (↑S : Type u)) → i ⟶ k x) (f₂ : (x : (↑S : Type u)) → j ⟶ k x)
    (h :
      ∀ (x : (↑S : Type u)),
        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 x)))
          ((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₁ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((a.hom' : (a : (↑S : Type u)) → (↑(F.obj i) : Type u)) x : (↑(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 x)))
          ((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₂ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((b.hom' : (a : (↑S : Type u)) → (↑(F.obj j) : Type u)) x : (↑(F.obj j) : 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 x)))),
    let J' :=
      { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun (x : ↥hf.finset) ↦ Sum.inl (),
        snd := fun (x : ↥hf.finset) ↦ Sum.inr () : MulticospanShape.{0, u} };
    let D : MulticospanIndex.{0, u, vJ, uJ} J' J :=
      { left := Sum.elim (fun (x : Unit) ↦ i) fun (x : Unit) ↦ j, right := fun (x : J'.R) ↦ k (↑x : (↑S : Type u)),
        fst := fun (x : J'.R) ↦ f₁ (↑x : (↑S : Type u)), snd := fun (x : J'.R) ↦ f₂ (↑x : (↑S : Type u)) };
    ∀ (c' : Cocone D.multicospan),
      Eq (α := (↑R : Type u) →+* (↑(F.obj c'.pt) : Type u))
        (comp (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))))
          (CommRingCat.Hom.hom f))
        (comp (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ())))))
          (CommRingCat.Hom.hom f))
hf₃ hf₄ :
  ∀
    (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))
    (k : (x : (↑S : Type u)) → J) (f₁ : (x : (↑S : Type u)) → i ⟶ k x) (f₂ : (x : (↑S : Type u)) → j ⟶ k x)
    (h :
      ∀ (x : (↑S : Type u)),
        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 x)))
          ((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₁ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((a.hom' : (a : (↑S : Type u)) → (↑(F.obj i) : Type u)) x : (↑(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 x)))
          ((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₂ x)) :
                (a : (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget CommRingCat).obj (k x)))
              ((b.hom' : (a : (↑S : Type u)) → (↑(F.obj j) : Type u)) x : (↑(F.obj j) : 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 x)))),
    let J' :=
      { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun (x : ↥hf.finset) ↦ Sum.inl (),
        snd := fun (x : ↥hf.finset) ↦ Sum.inr () : MulticospanShape.{0, u} };
    let D : MulticospanIndex.{0, u, vJ, uJ} J' J :=
      { left := Sum.elim (fun (x : Unit) ↦ i) fun (x : Unit) ↦ j, right := fun (x : J'.R) ↦ k (↑x : (↑S : Type u)),
        fst := fun (x : J'.R) ↦ f₁ (↑x : (↑S : Type u)), snd := fun (x : J'.R) ↦ f₂ (↑x : (↑S : Type u)) };
    ∀ (c' : Cocone D.multicospan),
      ∀ x ∈ hf.finset,
        Eq (α := (↑(F.obj c'.pt) : Type u))
          ((CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) :
                (a : (↑S : Type u)) → (↑(F.obj c'.pt) : Type u))
              x :
            (↑(F.obj c'.pt) : Type u))
          ((CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ())))) :
                (a : (↑S : Type u)) → (↑(F.obj c'.pt) : Type u))
              x :
            (↑(F.obj c'.pt) : Type u))
⊢ ∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk

Tactic:
classical
  have hc' := isColimitOfPreserves (forget _) hc
  choose k f₁ f₂ h using fun x : S ↦
    (Types.FilteredColimit.isColimit_eq_iff _ hc').mp congr(($hab).hom x)
  let J' : MulticospanShape := ⟨Unit ⊕ Unit, hf.finset, fun _ ↦ .inl .unit, fun _ ↦ .inr .unit⟩
  let D : MulticospanIndex J' J :=
  { left := Sum.elim (fun _ ↦ i) (fun _ ↦ j)
    right x := k x.1
    fst x := f₁ x
    snd x := f₂ x }
  obtain ⟨c'⟩ := IsFiltered.cocone_nonempty D.multicospan
  refine ⟨c'.pt, c'.ι.app (.left (.inl .unit)), c'.ι.app (.left (.inr .unit)), ?_⟩
  ext1
  apply hf.ext
  · rw [← CommRingCat.hom_comp, ← CommRingCat.hom_comp, reassoc_of% ha, reassoc_of% hb]
    simp [← α.naturality]
  · intro x hx
    rw [← c'.w (.fst (by exact ⟨x, hx⟩)), ← c'.w (.snd (by exact ⟨x, hx⟩))]
    have (x : _) : F.map (f₁ x) (a x) = F.map (f₂ x) (b x) := h x
    simp [D, this]

Premises used: RingHom.EssFiniteType.ext, CommRingCat.hom_comp, CategoryTheory.NatTrans.naturality