-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (hypothesis)
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
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)))
J' : MulticospanShape :=
  { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun (x : ↥hf.finset) ↦ Sum.inl (),
    snd := fun (x : ↥hf.finset) ↦ Sum.inr () }
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 : (↑S : Type u)
hx : x ∈ hf.finset
⊢ Eq (α := (↑(F.obj c'.pt) : Type u))
    (((CommRingCat.Hom.hom
              (a ≫
                F.map
                  (D.multicospan.map
                      (WalkingMulticospan.Hom.fst (Subtype.mk (p := fun (x : (↑S : Type u)) ↦ x ∈ hf.finset) x hx)) ≫
                    c'.ι.app
                      (WalkingMulticospan.right (Subtype.mk (p := fun (x : (↑S : Type u)) ↦ x ∈ hf.finset) x hx)))) :
            (↑S : Type u) →+* (↑(F.obj c'.pt) : Type u)) :
          (a : (↑S : Type u)) → (↑(F.obj c'.pt) : Type u))
        x :
      (↑(F.obj c'.pt) : Type u))
    (((CommRingCat.Hom.hom
              (b ≫
                F.map
                  (D.multicospan.map
                      (WalkingMulticospan.Hom.snd (Subtype.mk (p := fun (x : (↑S : Type u)) ↦ x ∈ hf.finset) x hx)) ≫
                    c'.ι.app
                      (WalkingMulticospan.right (Subtype.mk (p := fun (x : (↑S : Type u)) ↦ x ∈ hf.finset) x hx)))) :
            (↑S : Type u) →+* (↑(F.obj c'.pt) : Type u)) :
          (a : (↑S : Type u)) → (↑(F.obj c'.pt) : Type u))
        x :
      (↑(F.obj c'.pt) : Type u))
have this : ∀ (x : (↑S : Type u)),
  Eq (α := (↑(F.obj (k x)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (F.map (f₁ x)) :
          (a : (↑(F.obj i) : Type u)) → (↑(F.obj (k x)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) a :
              (a : (↑S : Type u)) → (↑(F.obj i) : Type u))
            x :
          (↑(F.obj i) : Type u)) :
      (↑(F.obj (k x)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (F.map (f₂ x)) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj (k x)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) b :
              (a : (↑S : Type u)) → (↑(F.obj j) : Type u))
            x :
          (↑(F.obj j) : Type u)) :
      (↑(F.obj (k x)) : Type u))
Tactic: have (x : _) : F.map (f₁ x) (a x) = F.map (f₂ x) (b x) := h x