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 : 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₂)))
⊢ 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₂)))
have rw₃ : Eq (α := X₁.obj j ⟶ colimit X₂) (φ.app j ≫ colimit.ι X₂ j)
  (φ.app j ≫ c₂.ι.app j ≫ 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_ι]
-- 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 : 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₂)))
⊢ 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₂)))
have rw₄ : φ.app j ≫ colimit.ι X₂ j = φ.app j ≫ (colimit.cocone 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 : 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
⊢ 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₂)))
have rw₅ : Eq (α := X₁.obj j ⟶ colimit X₂) (φ.app j ≫ colimit.ι X₂ j) (φ.app j ≫ colimit.ι 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
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
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂
have rw : φ.app j ≫ c₂.ι.app j ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂
Tactic: rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]
-- 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
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₂
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂
have rw₁ : c₁.ι.app j ≫ f ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂
Tactic: rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]
-- 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
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₂
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂
have rw₂ : c₁.ι.app j ≫ f ≫ g₂ = φ.app j ≫ c₂.ι.app j ≫ g₂
Tactic: rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]
-- 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
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₂
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂
have rw₃ : φ.app j ≫ c₂.ι.app j ≫ g₂ = φ.app j ≫ c₂.ι.app j ≫ g₂
Tactic: rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]
-- 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
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
⊢ 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
have dsimp : 𝟙 (X.obj j₀) ≫ X.map x_1.hom = X.map x.hom ≫ X.map (Under.Hom.right g)
Tactic: dsimp
-- 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
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 (c.ι.app j₀)
have this : Mono f
Tactic: have := NatTrans.mono_of_mono_app f
-- 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
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
have rw : S.f.app j ≫ c₂.ι.app j ≫ 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]
-- 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
rw : S.f.app j ≫ c₂.ι.app j ≫ g = c₁.ι.app j ≫ 0
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
have rw₁ : S.f.app j ≫ S.g.app j ≫ c₃.ι.app j = c₁.ι.app j ≫ 0
Tactic: rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]
-- 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
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
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
have rw₂ : S.f.app j ≫ S.g.app j ≫ c₃.ι.app j = 0
Tactic: rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]
-- 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
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
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
have rw₃ : (S.f ≫ S.g).app j ≫ c₃.ι.app j = 0
Tactic: rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]
-- 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
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
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
have rw₄ : Eq (α := S.X₁.obj j ⟶ c₃.pt) (NatTrans.app 0 j ≫ c₃.ι.app j) 0
Tactic: rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]
-- 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
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
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
have rw₅ : Eq (α := S.X₁.obj j ⟶ c₃.pt) (0 ≫ c₃.ι.app j) 0
Tactic: rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]
-- 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
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
⊢ c₁.ι.app j ≫ f ≫ g = c₁.ι.app j ≫ 0
have rw₆ : Eq.{v + 1} (α := S.X₁.obj j ⟶ c₃.pt) 0 0
Tactic: rw [reassoc_of% (hf j), hg j, comp_zero, ← NatTrans.comp_app_assoc, S.zero,
      zero_app, zero_comp]
-- 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
⊢ (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact
have refine : mapShortComplex S hc₁ c₂ c₃ f g hf hg ≅ S.map colim
Tactic: refine (ShortComplex.exact_iff_of_iso ?_).2 (hS.map colim)
-- 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
⊢ mapShortComplex S hc₁ c₂ c₃ f g hf hg ≅ S.map colim
have 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₂)))
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 ↦ ?_))
-- 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
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₂)))
⊢ mapShortComplex S hc₁ c₂ c₃ f g hf hg ≅ S.map colim
have 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₃)))
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 ↦ ?_))
-- 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.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₂)))
have 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₂)))
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.f))
    (c₁.ι.app j ≫ f ≫ Iso.hom (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)))
have 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₂)))
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₂)))
⊢ 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₂)
  (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₂)))
Tactic: rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]