awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_1 :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) ((colimit.cocone S.X₁).ι.app j ≫ colimMap S.f)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₁ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₁).pt) (colimit.ι S.X₁ j) (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
⊢ Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (c₁.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₁) (Iso.hom (hc₁.coconePointUniqueUpToIso (colimit.isColimit S.X₁)))
        (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
have refine_1₂ : Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j)
  (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_1 :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) ((colimit.cocone S.X₁).ι.app j ≫ colimMap S.f)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₁ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₁).pt) (colimit.ι S.X₁ j) (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₂ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
⊢ Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (c₁.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₁) (Iso.hom (hc₁.coconePointUniqueUpToIso (colimit.isColimit S.X₁)))
        (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
have refine_1₃ : Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j)
  (S.f.app j ≫ c₂.ι.app j ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_1 :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) ((colimit.cocone S.X₁).ι.app j ≫ colimMap S.f)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₁ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₁).pt) (colimit.ι S.X₁ j) (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₂ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₃ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j)
    (S.f.app j ≫ c₂.ι.app j ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
⊢ Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (c₁.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₁) (Iso.hom (hc₁.coconePointUniqueUpToIso (colimit.isColimit S.X₁)))
        (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
have refine_1₄ : S.f.app j ≫ colimit.ι S.X₂ j = S.f.app j ≫ (colimit.cocone S.X₂).ι.app j
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_1 :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) ((colimit.cocone S.X₁).ι.app j ≫ colimMap S.f)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₁ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₁).pt) (colimit.ι S.X₁ j) (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₂ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₃ :
  Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j)
    (S.f.app j ≫ c₂.ι.app j ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_1₄ : S.f.app j ≫ colimit.ι S.X₂ j = S.f.app j ≫ (colimit.cocone S.X₂).ι.app j
⊢ Eq (α := S.X₁.obj j ⟶ colimit S.X₂)
    (c₁.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₁) (Iso.hom (hc₁.coconePointUniqueUpToIso (colimit.isColimit S.X₁)))
        (colimMap S.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
have refine_1₅ : Eq (α := S.X₁.obj j ⟶ colimit S.X₂) (S.f.app j ≫ colimit.ι S.X₂ j) (S.f.app j ≫ colimit.ι S.X₂ j)
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ Eq (α := S.X₂.obj j ⟶ ShortComplex.X₃ (S.map colim))
    (c₂.ι.app j ≫
      CategoryStruct.comp (Y := ShortComplex.X₂ (S.map colim))
        (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂))) (ShortComplex.g (S.map colim)))
    (c₂.ι.app j ≫
      (mapShortComplex S hc₁ c₂ c₃ f g hf hg).g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
have refine_2 : Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
  (c₂.ι.app j ≫
    CategoryStruct.comp (Y := colimit S.X₂) (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
      (colimMap S.g))
  (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (c₂.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₂) (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
        (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
have refine_2 : Eq (α := S.X₂.obj j ⟶ colimit S.X₃) ((colimit.cocone S.X₂).ι.app j ≫ colimMap S.g)
  (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_2 :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) ((colimit.cocone S.X₂).ι.app j ≫ colimMap S.g)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
⊢ Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (c₂.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₂) (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
        (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
have refine_2₁ : Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
  (CategoryStruct.comp (Y := (colimit.cocone S.X₂).pt) (colimit.ι S.X₂ j) (colimMap S.g))
  (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_2 :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) ((colimit.cocone S.X₂).ι.app j ≫ colimMap S.g)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₁ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₂).pt) (colimit.ι S.X₂ j) (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
⊢ Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (c₂.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₂) (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
        (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
have refine_2₂ : Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j)
  (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_2 :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) ((colimit.cocone S.X₂).ι.app j ≫ colimMap S.g)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₁ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₂).pt) (colimit.ι S.X₂ j) (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₂ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
⊢ Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (c₂.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₂) (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
        (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
have refine_2₃ : Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j)
  (S.g.app j ≫ c₃.ι.app j ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_2 :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) ((colimit.cocone S.X₂).ι.app j ≫ colimMap S.g)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₁ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₂).pt) (colimit.ι S.X₂ j) (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₂ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₃ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j)
    (S.g.app j ≫ c₃.ι.app j ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
⊢ Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (c₂.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₂) (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
        (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
have refine_2₄ : S.g.app j ≫ colimit.ι S.X₃ j = S.g.app j ≫ (colimit.cocone S.X₃).ι.app j
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : HasExactColimitsOfShape.{v, v', u, u'} J C
inst_4 : HasZeroMorphisms.{v, u} C
S : ShortComplex (Functor.{v', v, u', u} J C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
refine_2 :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) ((colimit.cocone S.X₂).ι.app j ≫ colimMap S.g)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₁ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (CategoryStruct.comp (Y := (colimit.cocone S.X₂).pt) (colimit.ι S.X₂ j) (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₂ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j)
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₃ :
  Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j)
    (S.g.app j ≫ c₃.ι.app j ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
refine_2₄ : S.g.app j ≫ colimit.ι S.X₃ j = S.g.app j ≫ (colimit.cocone S.X₃).ι.app j
⊢ Eq (α := S.X₂.obj j ⟶ colimit S.X₃)
    (c₂.ι.app j ≫
      CategoryStruct.comp (Y := colimit S.X₂) (Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
        (colimMap S.g))
    (c₂.ι.app j ≫ g ≫ Iso.hom (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)))
have refine_2₅ : Eq (α := S.X₂.obj j ⟶ colimit S.X₃) (S.g.app j ≫ colimit.ι S.X₃ j) (S.g.app j ≫ colimit.ι S.X₃ j)
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : Functor.PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
X₁ X₂ : Functor.{v', v, u', u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : functorCategory (monomorphisms C) J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ monomorphisms C φ
have this : ∀ (j : J), Mono (f.app j)
Tactic: have (j : J) : Mono (f.app j) := hf _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : HasColimitsOfShape.{v', u', v, u} J C
inst_3 : Functor.PreservesMonomorphisms (C := Functor.{v', v, u', u} J C) colim
X₁ X₂ : Functor.{v', v, u', u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : functorCategory (monomorphisms C) J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : ∀ (j : J), Mono (f.app j)
⊢ monomorphisms C φ
have this₁ : Mono f
Tactic: have := NatTrans.mono_of_mono_app f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (goal)
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
⊢ IsColimit (F := pullback c.ι (Functor.map (Functor.const J) f))
    { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }
have suffices : IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) f))) (Y :=
  colimit.{w', w, v, u} (Functor.obj (Functor.const J) X))
  (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) f)))
Tactic: suffices IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f))) from
    Cocone.isColimitOfIsIsoColimMapι _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
⊢ IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) f))) (Y :=
    colimit.{w', w, v, u} (Functor.obj (Functor.const J) X))
    (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) f)))
have hpull : IsPullback (P := Functor.obj colim (pullback c.ι (Functor.map (Functor.const J) f)))
  (Functor.map colim (pullback.fst c.ι (Functor.map (Functor.const J) f)))
  (Functor.map colim (pullback.snd c.ι (Functor.map (Functor.const J) f))) (Functor.map colim c.ι)
  (Functor.map colim (Functor.map (Functor.const J) f))
Tactic: have hpull := colim.map_isPullback (IsPullback.of_hasPullback c.ι ((Functor.const J).map f))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected (hypothesis)
Goal:
J : Type w
inst : Category.{w', w} J
inst_1 : IsConnected.{w', w} J
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : HasColimitsOfShape.{w', w, v, u} J C
inst_5 : HasExactColimitsOfShape.{v, w', u, w} J C
F : Functor.{w', v, w, u} J C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
hpull :
  IsPullback (P := colimit (pullback c.ι (Functor.map (Functor.const J) f))) (X := colimit F) (Y :=
    colimit.{w', w, v, u} (Functor.obj (Functor.const J) X)) (Z :=
    colimit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt))
    (colimMap (pullback.fst c.ι (Functor.map (Functor.const J) f)))
    (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) f))) (colimMap c.ι)
    (colimMap (Functor.map (Functor.const J) f))
⊢ IsIso (X := colimit (pullback c.ι (Functor.map (Functor.const J) f))) (Y :=
    colimit.{w', w, v, u} (Functor.obj (Functor.const J) X))
    (colimMap (pullback.snd c.ι (Functor.map (Functor.const J) f)))
have this : IsIso (X := colimit F) (Y := colimit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (colimMap c.ι)
Tactic: have := hc.isIso_colimMap_ι