awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)
⊢ HasColimit (pair K L ⋙ eval C c i)

Tactic:
exact hasColimit_of_iso e

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
⊢ HasBinaryBiproduct K L

Tactic:
HasBinaryBiproduct.of_hasBinaryProduct _ _

Premises used: CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ PreservesBinaryBiproduct K L (eval C c i)

Tactic:
preservesBinaryBiproduct_of_preservesBinaryProduct _

Premises used: CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ Eq (α := K.X i ⟶ (K ⊞ L).X i)
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X i) (L.X i)) biprod.inl (Iso.inv (K.biprodXIso L i)) :
      K.X i ⟶ (K ⊞ L).X i)
    (Hom.f biprod.inl i : K.X i ⟶ (K ⊞ L).X i)

Tactic:
simp [biprodXIso]

Premises used: HomologicalComplex.biprodXIso
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ Eq (α := L.X i ⟶ (K ⊞ L).X i)
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X i) (L.X i)) biprod.inr (Iso.inv (K.biprodXIso L i)) :
      L.X i ⟶ (K ⊞ L).X i)
    (Hom.f biprod.inr i : L.X i ⟶ (K ⊞ L).X i)

Tactic:
simp [biprodXIso]

Premises used: HomologicalComplex.biprodXIso
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ Eq (α := (K ⊞ L).X i ⟶ K.X i)
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X i) (L.X i)) (Iso.hom (K.biprodXIso L i)) biprod.fst :
      (K ⊞ L).X i ⟶ K.X i)
    (Hom.f biprod.fst i : (K ⊞ L).X i ⟶ K.X i)

Tactic:
simp [biprodXIso]

Premises used: HomologicalComplex.biprodXIso
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ Eq (α := (K ⊞ L).X i ⟶ L.X i)
    (CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X i) (L.X i)) (Iso.hom (K.biprodXIso L i)) biprod.snd :
      (K ⊞ L).X i ⟶ L.X i)
    (Hom.f biprod.snd i : (K ⊞ L).X i ⟶ L.X i)

Tactic:
simp [biprodXIso]

Premises used: HomologicalComplex.biprodXIso
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.fst) i = 𝟙 (K.X i)
rw₁ : Hom.f (𝟙 K) i = 𝟙 (K.X i)
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) (𝟙 (K.X i))
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.fst i) = 𝟙 (K.X i)

Tactic:
rw [← comp_f, biprod.inl_fst, id_f]

Premises used: HomologicalComplex.id_f, CategoryTheory.Limits.biprod.inl_fst, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.snd) i) 0
rw₁ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (Hom.f 0 i) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) 0 0
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.snd i)) 0

Tactic:
rw [← comp_f, biprod.inl_snd, zero_f]

Premises used: CategoryTheory.Limits.biprod.inl_snd, HomologicalComplex.comp_f, HomologicalComplex.zero_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.fst) i) 0
rw₁ : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (Hom.f 0 i) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) 0 0
⊢ Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.fst i)) 0

Tactic:
rw [← comp_f, biprod.inr_fst, zero_f]

Premises used: CategoryTheory.Limits.biprod.inr_fst, HomologicalComplex.comp_f, HomologicalComplex.zero_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.snd) i = 𝟙 (L.X i)
rw₁ : Hom.f (𝟙 L) i = 𝟙 (L.X i)
rw₂ rw₃ : Eq.{v_1 + 1} (α := L.X i ⟶ L.X i) (𝟙 (L.X i)) (𝟙 (L.X i))
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.snd i) = 𝟙 (L.X i)

Tactic:
rw [← comp_f, biprod.inr_snd, id_f]

Premises used: HomologicalComplex.id_f, HomologicalComplex.comp_f, CategoryTheory.Limits.biprod.inr_snd
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ HAdd.hAdd (α := (K ⊞ L).X i ⟶ (K ⊞ L).X i)
      (CategoryStruct.comp (Y := K.X i) (Hom.f biprod.fst i) (Hom.f biprod.inl i))
      (CategoryStruct.comp (Y := L.X i) (Hom.f biprod.snd i) (Hom.f biprod.inr i)) =
    𝟙 ((K ⊞ L).X i)

Tactic:
simp [← comp_f, ← add_f_apply]

Premises used: HomologicalComplex.add_f_apply, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f : (K ⊞ L).X i ⟶ A
⊢ Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ f) ∧
    Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ f)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
refine :
  Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g) ∧
      Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g) →
    ∀ (h₁ : Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g))
      (h₂ : Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)), f = g
⊢ f = g ↔
    Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g) ∧
      Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)

Tactic:
refine ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
h :
  Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g) ∧
    Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
h₁ : Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g)
h₂ : Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
rw : 𝟙 ((K ⊞ L).X i) ≫ f = 𝟙 ((K ⊞ L).X i) ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi (𝟙 _)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
h :
  Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g) ∧
    Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
h₁ : Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g)
h₂ : Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
⊢ 𝟙 ((K ⊞ L).X i) ≫ f = 𝟙 ((K ⊞ L).X i) ≫ g

Tactic:
simp [← biprod_total_f, h₁, h₂]

Premises used: HomologicalComplex.biprod_total_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
h₁ : Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g)
h₂ : Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
⊢ f = g

Tactic:
simp [biprodX_ext_from_iff, h₁, h₂]

Premises used: HomologicalComplex.biprodX_ext_from_iff
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f : A ⟶ (K ⊞ L).X i
⊢ Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (f ≫ Hom.f biprod.fst i) ∧
    Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (f ≫ Hom.f biprod.snd i)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
refine :
  Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i) ∧
      Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i) →
    ∀ (h₁ : Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i))
      (h₂ : Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)), f = g
⊢ f = g ↔
    Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i) ∧
      Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)

Tactic:
refine ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
h :
  Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i) ∧
    Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
h₁ : Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i)
h₂ : Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
rw : f ≫ 𝟙 ((K ⊞ L).X i) = g ≫ 𝟙 ((K ⊞ L).X i)
⊢ f = g

Tactic:
rw [← cancel_mono (𝟙 _)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.cancel_mono
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
h :
  Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i) ∧
    Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
h₁ : Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i)
h₂ : Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
⊢ f ≫ 𝟙 ((K ⊞ L).X i) = g ≫ 𝟙 ((K ⊞ L).X i)

Tactic:
simp [← biprod_total_f, reassoc_of% h₁, reassoc_of% h₂]

Premises used: HomologicalComplex.biprod_total_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
h₁ : Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i)
h₂ : Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
⊢ f = g

Tactic:
simp [biprodX_ext_to_iff, h₁, h₂]

Premises used: HomologicalComplex.biprodX_ext_to_iff
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : K ⟶ M
β : L ⟶ M
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) biprod.inl (biprod.desc α β)).f i = α.f i
rw₁ rw₂ : α.f i = α.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f (biprod.desc α β) i) = α.f i

Tactic:
rw [← comp_f, biprod.inl_desc]

Premises used: HomologicalComplex.comp_f, CategoryTheory.Limits.biprod.inl_desc
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : K ⟶ M
β : L ⟶ M
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) biprod.inr (biprod.desc α β)).f i = β.f i
rw₁ rw₂ : β.f i = β.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f (biprod.desc α β) i) = β.f i

Tactic:
rw [← comp_f, biprod.inr_desc]

Premises used: CategoryTheory.Limits.biprod.inr_desc, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : M ⟶ K
β : M ⟶ L
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) (biprod.lift α β) biprod.fst).f i = α.f i
rw₁ rw₂ : α.f i = α.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f (biprod.lift α β) i) (Hom.f biprod.fst i) = α.f i

Tactic:
rw [← comp_f, biprod.lift_fst]

Premises used: CategoryTheory.Limits.biprod.lift_fst, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : M ⟶ K
β : M ⟶ L
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) (biprod.lift α β) biprod.snd).f i = β.f i
rw₁ rw₂ : β.f i = β.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f (biprod.lift α β) i) (Hom.f biprod.snd i) = β.f i

Tactic:
rw [← comp_f, biprod.lift_snd]

Premises used: CategoryTheory.Limits.biprod.lift_snd, HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
apply :
  ∀ (j : J),
    Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
      (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
          ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' : t.pt.X i ⟶ s.pt.X i')
          (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
            Functor.obj.{v_2, v_1, u_3, u_1}
                (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
              (F ⋙ eval C c i').obj j) :
        t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
      (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
          (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) : t.pt.X i ⟶ s.pt.X i')
          (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
            Functor.obj.{v_2, v_1, u_3, u_1}
                (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
              (F ⋙ eval C c i').obj j) :
        t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
⊢ Eq (α := t.pt.X i ⟶ s.pt.X i') ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' : t.pt.X i ⟶ s.pt.X i')
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) : t.pt.X i ⟶ s.pt.X i')

Tactic:
apply IsLimit.hom_ext (hs i')

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
⊢ ∀ (k : ι) (j : J),
    Eq (α := Cone.pt (F := F ⋙ eval C c k) (Functor.mapCone (eval C c k) t) ⟶ (F ⋙ eval C c k).obj j)
      ((hs k).lift (Functor.mapCone (eval C c k) t) ≫ NatTrans.app (Cone.π (Functor.mapCone (eval C c k) s)) j)
      (NatTrans.app (Cone.π (Functor.mapCone (eval C c k) t)) j)

Tactic:
have eq := fun k => (hs k).fac ((eval C c k).mapCone t)
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift (Functor.mapCone (eval C c k) t) ≫ (s.π.app j).f k = (t.π.app j).f k
simp :
  Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) ≫ (s.π.app j).f i' :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)

Tactic:
simp only [Functor.mapCone_π_app, eval_map, assoc]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.eval_map, CategoryTheory.Functor.mapCone_π_app
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift (Functor.mapCone (eval C c k) t) ≫ (s.π.app j).f k = (t.π.app j).f k
rw : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
rw₁ : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ (s.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
rw₂ : (t.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
rw₃ rw₄ : t.pt.d i i' ≫ (t.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) ≫ (s.π.app j).f i' :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)

Tactic:
rw [eq i', ← Hom.comm, reassoc_of% (eq i), Hom.comm]

Premises used: HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
j : J
h :
  ∀ (i : ι),
    Hom.f ({ f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ } ≫ s.π.app j) i =
      (t.π.app j).f i
⊢ { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ } ≫ s.π.app j = t.π.app j

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
j : J
i : ι
⊢ Hom.f ({ f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ } ≫ s.π.app j) i =
    (t.π.app j).f i

Tactic:
apply (hs i).fac

Premises used: CategoryTheory.Limits.IsLimit.fac