-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (goal)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
r : R
H : ∃ (j' : J), ∀ (j : J) (x : j' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0
x :
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (colimit F)
hx : r • x = 0
obtain :
  ∀ (j : J)
    (x :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (F.obj j))
    (hx :
      HSMul.hSMul (β :=
          ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
            ModuleCat.carrier) (colimit F))
          r
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
                  (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
                (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
              x :
            (↑(colimit F) : Type (max t w))) =
        0),
    Eq (α :=
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
          x :
        (↑(colimit F) : Type (max t w)))
      (0 :
        ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
          ModuleCat.carrier) (colimit F))
⊢ x = 0
have obtain₁ : ∀ (j : J)
  (x :
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (F.obj j))
  (hx :
    Eq (α :=
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
      ((ModuleCat.Hom.hom (colimit.ι F j) : (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
          (r • x) :
        (↑(colimit F) : Type (max t w)))
      (0 :
        ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
          ModuleCat.carrier) (colimit F))),
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
Tactic: classical
  obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep F x
  rw [← map_smul (colimit.ι F j).hom] at hx
  obtain ⟨j', i, h⟩ := Concrete.colimit_rep_eq_zero (hx := hx)
  obtain ⟨j'', H⟩ := H
  simpa [elementwise_of% (colimit.w F), map_zero] using congr(colimit.ι F _
    $(H (IsFiltered.sup {j, j', j''} { ⟨j, j', by simp, by simp, i⟩ })
      (IsFiltered.toSup _ _ <| by simp)
      (F.map (IsFiltered.toSup _ _ <| by simp) x)
      (by rw [← IsFiltered.toSup_commutes (f := i) (mY := by simp) (mf := by simp), F.map_comp,
        ModuleCat.comp_apply, ← map_smul, ← map_smul, h, map_zero])))
Cleared hypotheses: x, hx