awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x :
  (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
⊢ 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
        x *
      0 =
    0
have obtain : ∀ (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),
  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) *
      0 =
    0
Tactic: obtain ⟨j, x⟩ := x
Cleared hypotheses: x
-- 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
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₁
j₂ : J
y :
  ((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₃ : J
z :
  ((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₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [CategoryTheory.Functor.map_id]
-- 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 y : (↑(R.{v, u} F) : Type (max u v))
⊢ ZeroHom.toFun (↑(descAddMonoidHom t) : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))) (x * y) =
    ZeroHom.toFun (↑(descAddMonoidHom t) : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))) x *
      ZeroHom.toFun (↑(descAddMonoidHom t) : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))) y
have change : (descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) (x * y) =
  HMul.hMul (α := (↑t.pt : Type (max u v))) (β := (↑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)))
    ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) y : (↑t.pt : Type (max u v)))
Tactic: change descAddMonoidHom t (x * y) =
          descAddMonoidHom t x * descAddMonoidHom t y
-- 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
j : J
⊢ (colimitCocone.{v, u} F).ι.app j ≫
      ofHom
        (let __src : (↑(R.{v, u} F) : Type (max v u)) →+ (↑t.pt : Type (max u v)) := descAddMonoidHom t;
        { toFun := (↑__src : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))).toFun, map_one' := ⋯,
          map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) =
    t.ι.app j
have hf : ∀ (x : (↑(F.obj j) : Type (max u v))),
  Eq (α := (↑t.pt : Type (max u v)))
    ((Hom.hom
            ((colimitCocone.{v, u} F).ι.app j ≫
              ofHom
                (let __src : (↑(R.{v, u} F) : Type (max v u)) →+ (↑t.pt : Type (max u v)) := descAddMonoidHom t;
                { toFun := (↑__src : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))).toFun, map_one' := sorry,
                  map_mul' := sorry, map_zero' := sorry, map_add' := sorry })) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v)))
        x :
      (↑t.pt : Type (max u v)))
    ((Hom.hom (t.ι.app j) : (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v))) x :
      (↑t.pt : Type (max u v)))
Tactic: ext x
-- 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
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inl : IsEmpty J → Nontrivial.{v} (↑c.pt : Type v)
Tactic: cases isEmpty_or_nonempty J
-- 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)
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inr : Nonempty J → Nontrivial.{v} (↑c.pt : Type v)
Tactic: cases isEmpty_or_nonempty J
-- 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
h : Nonempty J
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inr : ∀ (i : J), Nontrivial.{v} (↑c.pt : Type v)
Tactic: have i := ‹Nonempty J›.some
-- 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
h : Nonempty J
i : J
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inr : ∀
  (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
Tactic: refine ⟨c.ι.app i 0, c.ι.app i 1, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (hypothesis)
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
h_1 : 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
have this : IsFiltered J
Tactic: have : IsFiltered J := ⟨⟩
-- 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
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inl : IsEmpty J → 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)
-- 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)
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inr : Nonempty J → 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)
-- 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)
⊢ Nontrivial.{v} (↑c.pt : Type v)
have inr₂ : Nonempty J → ∀ (i : J), 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)
-- 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)
⊢ 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))),
    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)
-- 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
⊢ 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), 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)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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 : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk
have choose : ∀ (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)))),
  ∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk
Tactic: choose k f₁ f₂ h using fun x : S ↦
    (Types.FilteredColimit.isColimit_eq_iff _ hc').mp congr(($hab).hom x)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
⊢ ∃ (k : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk
have have : ∀
  (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 : J) (hik : i ⟶ k) (hjk : j ⟶ k), a ≫ F.map hik = b ≫ F.map hjk
Tactic: classical
  have hc' := isColimitOfPreserves (forget _) hc
  choose k f₁ f₂ h using fun x : S ↦
    (Types.FilteredColimit.isColimit_eq_iff _ hc').mp congr(($hab).hom x)
  let J' : MulticospanShape := ⟨Unit ⊕ Unit, hf.finset, fun _ ↦ .inl .unit, fun _ ↦ .inr .unit⟩
  let D : MulticospanIndex J' J :=
  { left := Sum.elim (fun _ ↦ i) (fun _ ↦ j)
    right x := k x.1
    fst x := f₁ x
    snd x := f₂ x }
  obtain ⟨c'⟩ := IsFiltered.cocone_nonempty D.multicospan
  refine ⟨c'.pt, c'.ι.app (.left (.inl .unit)), c'.ι.app (.left (.inr .unit)), ?_⟩
  ext1
  apply hf.ext
  · rw [← CommRingCat.hom_comp, ← CommRingCat.hom_comp, reassoc_of% ha, reassoc_of% hb]
    simp [← α.naturality]
  · intro x hx
    rw [← c'.w (.fst (by exact ⟨x, hx⟩)), ← c'.w (.snd (by exact ⟨x, hx⟩))]
    have (x : _) : F.map (f₁ x) (a x) = F.map (f₂ x) (b x) := h x
    simp [D, this]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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).FinitePresentation
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
have have : ∀
  (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)),
  ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
Tactic: have hc' := isColimitOfPreserves (forget _) hc