-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
inl : IsEmpty J → Nontrivial.{v} (↑c.pt : Type v)
inr inr₁ : Nonempty J → Nontrivial.{v} (↑c.pt : Type v)
inr₂ : Nonempty J → ∀ (i : J), Nontrivial.{v} (↑c.pt : Type v)
inr₃ :
  Nonempty J →
    ∀ (i : J)
      (h :
        Eq (α := (↑c.pt : Type v))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                  (c.ι.app i) :
                (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
              0 :
            (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                  (c.ι.app i) :
                (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
              1 :
            (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))),
      False
inr₄ :
  Nonempty J →
    ∀ (i : J)
      (h :
        Eq (α := (↑c.pt : Type v))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                  (c.ι.app i) :
                (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
              0 :
            (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                  (c.ι.app i) :
                (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
              1 :
            (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v)))
      (this : IsFiltered J), False
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inr₅ : Nonempty J →
  ∀ (i : J)
    (h :
      Eq (α := (↑c.pt : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                (c.ι.app i) :
              (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
            0 :
          (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                (c.ι.app i) :
              (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
            1 :
          (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v)))
    (this : IsFiltered J) (k : J) (f : i ⟶ k)
    (e :
      Eq (α :=
        (fun (X : Type v) ↦ X)
          ((F ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                  carrier)).obj
            k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                      carrier)).map
                f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj k))
          0)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F ⋙
                    forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                      carrier)).map
                f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj k))
          1)),
    False
Tactic: classical
  cases isEmpty_or_nonempty J
  · exact ((isColimitEquivIsInitialOfIsEmpty _ _ hc).to (.of (ULift ℤ))).hom.domain_nontrivial
  have i := ‹Nonempty J›.some
  refine ⟨c.ι.app i 0, c.ι.app i 1, fun h ↦ ?_⟩
  have : IsFiltered J := ⟨⟩
  obtain ⟨k, f, e⟩ :=
    (Types.FilteredColimit.isColimit_eq_iff' (isColimitOfPreserves (forget _) hc) _ _).mp h
  exact zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)