-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
x : (↑(R.{v, u} F) : Type (max v u))
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((descMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) x : (↑t.pt : Type (max u v)))
    ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) x : (↑t.pt : Type (max u v)))
have mk : ∀ (j : J)
  (x :
    ((F ⋙
            forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
              carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
              MonCat.carrier)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).obj
      j),
  Eq (α := (↑t.pt : Type (max u v)))
    ((descMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v)))
        (Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x)) :
      (↑t.pt : Type (max u v)))
    ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v)))
        (Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x)) :
      (↑t.pt : Type (max u v)))
Tactic: obtain ⟨j, x⟩ := x