awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
φ : X₁ ⟶ X₂
inst_4 : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
rw :
  Eq (α := X₁.obj j ⟶ colimit X₂) ((colimit.cocone X₁).ι.app j ≫ colimMap φ)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
rw₁ :
  Eq (α := X₁.obj j ⟶ colimit X₂) (CategoryStruct.comp (Y := (colimit.cocone X₁).pt) (colimit.ι X₁ j) (colimMap φ))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
rw₂ :
  Eq (α := X₁.obj j ⟶ colimit X₂) (φ.app j ≫ colimit.ι X₂ j)
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
rw₃ :
  Eq (α := X₁.obj j ⟶ colimit X₂) (φ.app j ≫ colimit.ι X₂ j)
    (φ.app j ≫ c₂.ι.app j ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))
rw₄ : φ.app j ≫ colimit.ι X₂ j = φ.app j ≫ (colimit.cocone X₂).ι.app j
rw₅ rw₆ : Eq (α := X₁.obj j ⟶ colimit X₂) (φ.app j ≫ colimit.ι X₂ j) (φ.app j ≫ colimit.ι X₂ j)
⊢ Eq (α := X₁.obj j ⟶ colimit X₂)
    (c₁.ι.app j ≫
      CategoryStruct.comp (Y := colimit X₁) (Iso.hom (hc₁.coconePointUniqueUpToIso (colimit.isColimit X₁)))
        (colimMap φ))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)))

Tactic:
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
        colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
        IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

Premises used: CategoryTheory.Limits.colimit.cocone_ι, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X₁ X₂ : Functor.{v', v, u', u} J C
φ : X₁ ⟶ X₂
inst_2 : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
rw : φ.app j ≫ c₂.ι.app j ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂
rw₁ : c₁.ι.app j ≫ f ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂
rw₂ : c₁.ι.app j ≫ f ≫ g₂ = φ.app j ≫ c₂.ι.app j ≫ g₂
rw₃ rw₄ : φ.app j ≫ c₂.ι.app j ≫ g₂ = φ.app j ≫ c₂.ι.app j ≫ g₂
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂

Tactic:
rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : Functor.{v', v, u', u} J C
inst_2 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst_3 : IsFiltered.{v', u'} J
j₀ : J
inst_4 : HasColimitsOfShape (Under.{v', u'} j₀) C
inst_5 : Functor.PreservesMonomorphisms (C := Under.{v', u'} j₀ ⥤ C) colim
x x_1 : Under.{v', u'} j₀
g : x ⟶ x_1
dsimp : 𝟙 (X.obj j₀) ≫ X.map x_1.hom = X.map x.hom ≫ X.map (Under.Hom.right g)
⊢ Functor.map (Functor.obj (Functor.const (Under.{v', u'} j₀)) (X.obj j₀)) g ≫ X.map x_1.hom =
    X.map x.hom ≫ (Under.forget j₀ ⋙ X).map g

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : Functor.{v', v, u', u} J C
inst_2 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst_3 : IsFiltered.{v', u'} J
j₀ : J
inst_4 : HasColimitsOfShape (Under.{v', u'} j₀) C
inst_5 : Functor.PreservesMonomorphisms (C := Under.{v', u'} j₀ ⥤ C) colim
x x_1 : Under.{v', u'} j₀
g : x ⟶ x_1
⊢ 𝟙 (X.obj j₀) ≫ X.map x_1.hom = X.map x.hom ≫ X.map (Under.Hom.right g)

Tactic:
simp only [Category.id_comp, ← X.map_comp, Under.w]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Under.w, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : Functor.{v', v, u', u} J C
inst_2 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst_3 : IsFiltered.{v', u'} J
j₀ : J
inst_4 : HasColimitsOfShape (Under.{v', u'} j₀) C
inst_5 : Functor.PreservesMonomorphisms (C := Under.{v', u'} j₀ ⥤ C) colim
f : Functor.obj (Functor.const (Under.{v', u'} j₀)) (X.obj j₀) ⟶ Under.forget j₀ ⋙ X :=
  { app := fun (j : Under.{v', u'} j₀) ↦ X.map j.hom, naturality := ⋯ }
⊢ Mono f

Tactic:
have := NatTrans.mono_of_mono_app f
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
X : Functor.{v', v, u', u} J C
inst_2 : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst_3 : IsFiltered.{v', u'} J
j₀ : J
inst_4 : HasColimitsOfShape (Under.{v', u'} j₀) C
inst_5 : Functor.PreservesMonomorphisms (C := Under.{v', u'} j₀ ⥤ C) colim
f : Functor.obj (Functor.const (Under.{v', u'} j₀)) (X.obj j₀) ⟶ Under.forget j₀ ⋙ X :=
  { app := fun (j : Under.{v', u'} j₀) ↦ X.map j.hom, naturality := ⋯ }
this : Mono f
⊢ Mono (c.ι.app j₀)

Tactic:
exact colim.map_mono' f (isColimitConstCocone _ _)
    ((Functor.Final.isColimitWhiskerEquiv _ _).symm hc) (c.ι.app j₀) (by cat_disch)

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.isColimitConstCocone, CategoryTheory.Limits.colim.map_mono', CategoryTheory.Functor.Final.isColimitWhiskerEquiv, Equiv.symm, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
dsimp : c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
rw : S.f.app j ≫ c₂.ι.app j ≫ g = c₁.ι.app j ≫ 0
rw₁ : S.f.app j ≫ S.g.app j ≫ c₃.ι.app j = c₁.ι.app j ≫ 0
rw₂ : S.f.app j ≫ S.g.app j ≫ c₃.ι.app j = 0
rw₃ : (S.f ≫ S.g).app j ≫ c₃.ι.app j = 0
rw₄ : Eq (α := S.X₁.obj j ⟶ c₃.pt) (NatTrans.app 0 j ≫ c₃.ι.app j) 0
rw₅ : Eq (α := S.X₁.obj j ⟶ c₃.pt) (0 ≫ c₃.ι.app j) 0
rw₆ rw₇ : Eq.{v + 1} (α := S.X₁.obj j ⟶ c₃.pt) 0 0
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0

Tactic:
rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]

Premises used: CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.zero, CategoryTheory.Limits.zero_app, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
⊢ (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact

Tactic:
(ShortComplex.exact_iff_of_iso ?_).2 (hS.map colim)

Premises used: Iff.mpr, CategoryTheory.Limits.colim, CategoryTheory.ShortComplex.exact_iff_of_iso, CategoryTheory.ShortComplex.Exact.map
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
refine : mapShortComplex S hc₁ c₂ c₃ f g hf hg ≅ S.map colim
⊢ (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact

Tactic:
refine (ShortComplex.exact_iff_of_iso ?_).2 (hS.map colim)

Premises used: Iff.mpr, CategoryTheory.Limits.colim, CategoryTheory.ShortComplex.exact_iff_of_iso, CategoryTheory.ShortComplex.Exact.map
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
refine_1 :
  ∀ (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.f (S.map colim)))
      (c₁.ι.app j ≫
        (mapShortComplex S hc₁ c₂ c₃ f g hf hg).f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
refine_2 :
  ∀ (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₃)))
⊢ mapShortComplex S hc₁ c₂ c₃ f g hf hg ≅ S.map colim

Tactic:
refine ShortComplex.isoMk
    (IsColimit.coconePointUniqueUpToIso hc₁ (colimit.isColimit _))
    (IsColimit.coconePointUniqueUpToIso hc₂ (colimit.isColimit _))
    (IsColimit.coconePointUniqueUpToIso hc₃ (colimit.isColimit _))
    (hc₁.hom_ext (fun j ↦ ?_)) (hc₂.hom_ext (fun j ↦ ?_))

Premises used: CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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₂)
    (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₂)))
⊢ 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.f (S.map colim)))
    (c₁.ι.app j ≫
      (mapShortComplex S hc₁ c₂ c₃ f g hf hg).f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
refine_1₅ 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)
⊢ 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₂)))

Tactic:
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

Premises used: CategoryTheory.Limits.colimit.cocone_ι, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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₃)
    (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₃)))
⊢ 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₃)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
refine_2₅ 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)
⊢ 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:
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

Premises used: CategoryTheory.Limits.colimit.cocone_ι, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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
⊢ ∀ (j : J), Mono (f.app j)

Tactic:
have (j : J) : Mono (f.app j) := hf _
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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)
⊢ Mono f

Tactic:
have := NatTrans.mono_of_mono_app f
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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_1 : ∀ (j : J), Mono (f.app j)
this : Mono f
⊢ ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j

Tactic:
simp [hφ]
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
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_1 : ∀ (j : J), Mono (f.app j)
this : Mono f
⊢ monomorphisms C φ

Tactic:
apply colim.map_mono' f hc₁ hc₂ φ (by simp [hφ])

Premises used: CategoryTheory.Limits.colim.map_mono'
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u'
inst_1 : Category.{v', u'} J_1
inst_2 : HasFilteredColimitsOfSize.{v', u', v, u} C
inst_3 : AB5OfSize.{v', u', v, u} C
J : Type u'
x : Category.{v', u'} J
h : IsFiltered.{v', u'} J
⊢ IsStableUnderColimitsOfShape.{v, u, v', u'} (monomorphisms C) J

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
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
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)))
⊢ IsColimit (F := pullback c.ι (Functor.map (Functor.const J) f))
    { pt := X, ι := pullback.snd c.ι (Functor.map (Functor.const J) f) }

Tactic:
suffices IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f))) from
    Cocone.isColimitOfIsIsoColimMapι _
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
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
⊢ 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))
-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected
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 F) (Y := colimit.{w', w, v, u} (Functor.obj (Functor.const J) c.pt)) (colimMap c.ι)

Tactic:
have := hc.isIso_colimMap_ι