awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))

Tactic:
simp [ι₀]

Premises used: HomologicalComplex.cylinder.ι₀
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))

Tactic:
simp only [inr_biprodXIso_inv_assoc, biprod_inr_snd_f_assoc, comp_sub,
        biprod_inr_desc_f_assoc, id_f, id_comp, ι₀, comp_f, this,
        sub_f_apply, sub_comp, homotopyCofiber_X, homotopyCofiber.inr_f]

Premises used: HomologicalComplex.biprod_inr_snd_f_assoc, HomologicalComplex.homotopyCofiber_X, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, HomologicalComplex.cylinder.ι₀, HomologicalComplex.comp_f, HomologicalComplex.inr_biprodXIso_inv_assoc, HomologicalComplex.biprod_inr_desc_f_assoc, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp, HomologicalComplex.homotopyCofiber.inr_f, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ¬∃ (k : ι), c.Rel j k
⊢ ∀ (x : ι), ¬c.Rel j x

Tactic:
simp only [not_exists] at hj

Premises used: not_exists
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
neg :
  Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
simp only [assoc, Homotopy.nullHomotopicMap'_f_of_not_rel_left hij hj, homotopyCofiber_X,
      homotopyCofiber_d, homotopyCofiber.inlX_d' _ _ _ _ (hj _), homotopyCofiber.inrX_sndX_assoc,
      comp_sub, inrX_π_assoc, comp_id, ι₀, comp_f, homotopyCofiber.inr_f]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.homotopyCofiber.inrX_sndX_assoc, HomologicalComplex.homotopyCofiber_X, HomologicalComplex.cylinder.ι₀, CategoryTheory.Category.comp_id, HomologicalComplex.cylinder.inrX_π_assoc, HomologicalComplex.comp_f, Homotopy.nullHomotopicMap'_f_of_not_rel_left, HomologicalComplex.homotopyCofiber.inlX_d', HomologicalComplex.homotopyCofiber_d, CategoryTheory.Preadditive.comp_sub, HomologicalComplex.homotopyCofiber.inr_f
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
neg :
  Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
⊢ Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)

Tactic:
rw [← cancel_epi (biprodXIso K K j).inv]

Premises used: HomologicalComplex.biprodXIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
neg :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
neg₁ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
⊢ Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f biprod.inl j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
h : ∀ (i : ι), Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
⊢ nullHomotopicMap K = π K ≫ ι₀ K - 𝟙 K.cylinder

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i : ι
pos : ∀ (hi : c.Rel i (c.next i)), Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
neg : ∀ (hi : ¬c.Rel i (c.next i)), Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
⊢ Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
by_cases hi : c.Rel i (c.next i)

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
homotopyCofiber.ext_from_X (biprod.lift (𝟙 K) (-𝟙 K)) (c.next i) i hi
      (inlX_nullHomotopy_f _ _ _ _) (inrX_nullHomotopy_f _ hc _)

Premises used: HomologicalComplex.homotopyCofiber.X, CategoryTheory.CategoryStruct.id, dite, CategoryTheory.Limits.biprod.lift, HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, ComplexShape.next, HomologicalComplex.homotopyCofiber.ext_from_X, Neg.neg, HomologicalComplex.cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i : ι
hi : c.Rel i (c.next i)
⊢ Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
exact homotopyCofiber.ext_from_X (biprod.lift (𝟙 K) (-𝟙 K)) (c.next i) i hi
      (inlX_nullHomotopy_f _ _ _ _) (inrX_nullHomotopy_f _ hc _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.biprod.lift, HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, ComplexShape.next, HomologicalComplex.homotopyCofiber.ext_from_X, Neg.neg, HomologicalComplex.cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
homotopyCofiber.ext_from_X' (biprod.lift (𝟙 K) (-𝟙 K)) _ hi (inrX_nullHomotopy_f _ hc _)

Premises used: HomologicalComplex.homotopyCofiber.X, CategoryTheory.CategoryStruct.id, dite, CategoryTheory.Limits.biprod.lift, HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, HomologicalComplex.homotopyCofiber.ext_from_X', Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ Hom.f (nullHomotopicMap K) i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
exact homotopyCofiber.ext_from_X' (biprod.lift (𝟙 K) (-𝟙 K)) _ hi (inrX_nullHomotopy_f _ hc _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.biprod.lift, HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, HomologicalComplex.homotopyCofiber.ext_from_X', Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
inst_4 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_5 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
⊢ CategoryStruct.comp (Y := K.cylinder) (ι₀ K) (π K) = 𝟙 K

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
inst_4 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_5 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
⊢ Eq (α := K ⟶ K.cylinder) (ι₀ K) (CategoryStruct.comp (Y := K.cylinder) (ι₁ K) (π K ≫ ι₀ K))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
inst_4 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_5 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
⊢ ι₁ K ≫ 𝟙 K.cylinder = ι₁ K

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
D : Type u_3
inst_5 : Category.{v_2, u_3} D
H : HomologicalComplex.{v_1, u_1, u_2} C c ⥤ D
hH : MorphismProperty.IsInvertedBy (homotopyEquivalences C c) H
⊢ IsIso (X := H.obj K.cylinder) (H.map (π K))

Tactic:
have : IsIso (H.map (cylinder.π K)) := hH _ ⟨homotopyEquiv K hc, rfl⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
D : Type u_3
inst_5 : Category.{v_2, u_3} D
H : HomologicalComplex.{v_1, u_1, u_2} C c ⥤ D
hH : MorphismProperty.IsInvertedBy (homotopyEquivalences C c) H
this : IsIso (X := H.obj K.cylinder) (H.map (π K))
⊢ Eq (α := H.obj K ⟶ H.obj K.cylinder) (H.map (ι₀ K)) (H.map (ι₁ K))

Tactic:
simp only [← cancel_mono (H.map (cylinder.π K)), ← H.map_comp, ι₀_π, H.map_id, ι₁_π]

Premises used: HomologicalComplex.cylinder.ι₁_π, CategoryTheory.cancel_mono, HomologicalComplex.cylinder.ι₀_π, CategoryTheory.Functor.map, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, HomologicalComplex.cylinder.π
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ φ₁ : F ⟶ G
h : Homotopy φ₀ φ₁
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (F.X i) (F.X i)
inst_3 : HasHomotopyCofiber (G := F ⊞ F) (biprod.lift (𝟙 F) (-𝟙 F))
D : Type u_3
inst_4 : Category.{v_2, u_3} D
H : HomologicalComplex.{v_1, u_1, u_2} C c ⥤ D
hH : MorphismProperty.IsInvertedBy (homotopyEquivalences C c) H
⊢ H.map φ₀ = H.map φ₁

Tactic:
simp only [← cylinder.ι₀_desc _ _ h, ← cylinder.ι₁_desc _ _ h, H.map_comp,
    cylinder.map_ι₀_eq_map_ι₁ _ hc _ hH]

Premises used: HomologicalComplex.cylinder.ι₀_desc, CategoryTheory.Functor.map_comp, HomologicalComplex.cylinder.map_ι₀_eq_map_ι₁, HomologicalComplex.cylinder.ι₁_desc
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ φ₁ : F ⟶ G
h : Homotopy φ₀ φ₁
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (F.X i) (F.X i)
inst_3 : HasHomotopyCofiber (G := F ⊞ F) (biprod.lift (𝟙 F) (-𝟙 F))
D : Type u_3
inst_4 : Category.{v_2, u_3} D
H : HomologicalComplex.{v_1, u_1, u_2} C c ⥤ D
hH : MorphismProperty.IsInvertedBy (homotopyEquivalences C c) H
⊢ H.map φ₀ = H.map φ₁

Tactic:
classical
  simp only [← cylinder.ι₀_desc _ _ h, ← cylinder.ι₁_desc _ _ h, H.map_comp,
    cylinder.map_ι₀_eq_map_ι₁ _ hc _ hH]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : DecidableRel c.Rel
inst_3 : HasHomotopyFiber φ
inst_4 : DecidableRel c.Rel
i j : α
hij : c.symm.Rel i j
⊢ HasBinaryBiproduct.{v_1, u_1} (G.X j) (F.X i)

Tactic:
have := HasHomotopyFiber.hasBinaryBiproduct φ j i hij
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : DecidableRel c.Rel
inst_3 : HasHomotopyFiber φ
inst_4 : DecidableRel c.Rel
i j : α
hij : c.symm.Rel i j
this : HasBinaryBiproduct.{v_1, u_1} (G.X j) (F.X i)
dsimp : HasBinaryBiproduct.{v_1, u_1} (op (G.X j)) (op (F.X i))
⊢ HasBinaryBiproduct.{v_1, u_1} ((Functor.obj (opFunctor C c) (op G)).X j) ((Functor.obj (opFunctor C c) (op F)).X i)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyFiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : DecidableRel c.Rel
inst_3 : HasHomotopyFiber φ
inst_4 : DecidableRel c.Rel
i j : α
hij : c.symm.Rel i j
this : HasBinaryBiproduct.{v_1, u_1} (G.X j) (F.X i)
⊢ HasBinaryBiproduct.{v_1, u_1} (op (G.X j)) (op (F.X i))

Tactic:
infer_instance