-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
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
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
⊢ Nontrivial.{v} (↑c.pt : Type v)

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)

Premises used: isEmpty_or_nonempty