awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
h₄ :
  Hom.τ₁
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₁
h₅ :
  Hom.τ₂
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₂
h₆ :
  Hom.τ₃
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₃
⊢ c.ι.app j ≫
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    s.ι.app j

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
⊢ Hom.τ₁
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₁

Tactic:
apply IsColimit.fac h₁

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
⊢ Hom.τ₂
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₂

Tactic:
apply IsColimit.fac h₂

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
⊢ Hom.τ₃
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₃

Tactic:
apply IsColimit.fac h₃

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
h₄ :
  m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
h₅ :
  m.τ₂ =
    Hom.τ₂
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
h₆ :
  m.τ₃ =
    Hom.τ₃
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
⊢ m =
    { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
      comm₂₃ := ⋯ }

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
h₁.uniq (π₁.mapCocone s) _ (fun j => π₁.congr_map (hm j))

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ShortComplex.π₁, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
exact h₁.uniq (π₁.mapCocone s) _ (fun j => π₁.congr_map (hm j))

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ShortComplex.π₁, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₂ =
    Hom.τ₂
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
h₂.uniq (π₂.mapCocone s) _ (fun j => π₂.congr_map (hm j))

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.ShortComplex.π₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₂ =
    Hom.τ₂
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
exact h₂.uniq (π₂.mapCocone s) _ (fun j => π₂.congr_map (hm j))

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.ShortComplex.π₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₃ =
    Hom.τ₃
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
h₃.uniq (π₃.mapCocone s) _ (fun j => π₃.congr_map (hm j))

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ShortComplex.π₃, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₃ =
    Hom.τ₃
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
exact h₃.uniq (π₃.mapCocone s) _ (fun j => π₃.congr_map (hm j))

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.ShortComplex.π₃, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Functor.congr_map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
j : J
⊢ colimit.ι (F ⋙ π₁) j ≫
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          j).f =
    (F.obj j).f ≫ colimit.ι (F ⋙ π₂) j

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
j : J
⊢ colimit.ι (F ⋙ π₂) j ≫
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          j).g =
    (F.obj j).g ≫ colimit.ι (F ⋙ π₃) j

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    (F.obj x).X₁ ⟶
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x_1).X₁)
    (Hom.τ₁
      (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₁
      ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        Functor.map
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f))

Tactic:
simp [← colimit.w (F ⋙ π₁) f]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ShortComplex.π₁, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    (F.obj x).X₂ ⟶
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x_1).X₂)
    (Hom.τ₂
      (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₂
      ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        Functor.map
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f))

Tactic:
simp [← colimit.w (F ⋙ π₂) f]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.w, CategoryTheory.ShortComplex.π₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    (F.obj x).X₃ ⟶
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x_1).X₃)
    (Hom.τ₃
      (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₃
      ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        Functor.map
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f))

Tactic:
simp [← colimit.w (F ⋙ π₃) f]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ShortComplex.π₃, CategoryTheory.Limits.colimit.w
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
⊢ HasColimit F

Tactic:
⟨⟨⟨_, isColimitColimitCocone _⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.ShortComplex.isColimitColimitCocone
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
⊢ PreservesColimit F π₁

Tactic:
preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F)
    (isColimitπ₁MapCoconeColimitCocone F)

Premises used: CategoryTheory.ShortComplex.isColimitπ₁MapCoconeColimitCocone, CategoryTheory.ShortComplex.isColimitColimitCocone, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
⊢ PreservesColimit F π₂

Tactic:
preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F)
    (isColimitπ₂MapCoconeColimitCocone F)

Premises used: CategoryTheory.ShortComplex.isColimitπ₂MapCoconeColimitCocone, CategoryTheory.ShortComplex.isColimitColimitCocone, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
⊢ PreservesColimit F π₃

Tactic:
preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F)
    (isColimitπ₃MapCoconeColimitCocone F)

Premises used: CategoryTheory.ShortComplex.isColimitπ₃MapCoconeColimitCocone, CategoryTheory.ShortComplex.isColimitColimitCocone, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteColimits.{v_2, u_2} C
⊢ HasFiniteColimits (ShortComplex.{v_2, u_2} C)

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteColimits.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteColimits.{v_2, u_2} C
⊢ PreservesFiniteColimits (C := ShortComplex.{v_2, u_2} C) π₁

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: CategoryTheory.Limits.PreservesFiniteColimits.mk, inferInstance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteColimits.{v_2, u_2} C
⊢ PreservesFiniteColimits (C := ShortComplex.{v_2, u_2} C) π₂

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: CategoryTheory.Limits.PreservesFiniteColimits.mk, inferInstance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteColimits.{v_2, u_2} C
⊢ PreservesFiniteColimits (C := ShortComplex.{v_2, u_2} C) π₃

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: CategoryTheory.Limits.PreservesFiniteColimits.mk, inferInstance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimitsOfShape.{0, 0, v_2, u_2} WalkingSpan C
⊢ PreservesEpimorphisms (C := ShortComplex.{v_2, u_2} C) π₁

Tactic:
CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape _

Premises used: CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimitsOfShape.{0, 0, v_2, u_2} WalkingSpan C
⊢ PreservesEpimorphisms (C := ShortComplex.{v_2, u_2} C) π₂

Tactic:
CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape _

Premises used: CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasColimitsOfShape.{0, 0, v_2, u_2} WalkingSpan C
⊢ PreservesEpimorphisms (C := ShortComplex.{v_2, u_2} C) π₃

Tactic:
CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape _

Premises used: CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
a : R
φ : S₁ ⟶ S₂
⊢ (a • φ).τ₁ = a • φ.τ₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
a : R
φ : S₁ ⟶ S₂
⊢ (a • φ).τ₂ = a • φ.τ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
a : R
φ : S₁ ⟶ S₂
⊢ (a • φ).τ₃ = a • φ.τ₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).leftHomologyMap'_eq, LeftHomologyMapData.smul_φH, γ.leftHomologyMap'_eq]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.smul
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂
⊢ cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).cyclesMap'_eq, LeftHomologyMapData.smul_φK, γ.cyclesMap'_eq]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.smul
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
a : R
inst_4 : S₁.HasLeftHomology
inst_5 : S₂.HasLeftHomology
⊢ leftHomologyMap (a • φ) = HSMul.hSMul (β := S₁.leftHomology ⟶ S₂.leftHomology) a (leftHomologyMap φ)

Tactic:
leftHomologyMap'_smul _ _ _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.leftHomologyMap'_smul