awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
mp :
  Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 →
    Nonempty (Homotopy (𝟙 C) 0)
mpr :
  Nonempty (Homotopy (𝟙 C) 0) →
    Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0 ↔
    Nonempty (Homotopy (𝟙 C) 0)

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
h : Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C)
    (CategoryTheory.Functor.map (quotient V c) (𝟙 C)) (CategoryTheory.Functor.map (quotient V c) 0)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
h : Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0
⊢ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
exact ⟨(homotopyOfEq _ _ (by simp [h]))⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_2} V c
h : Homotopy (𝟙 C) 0
⊢ Eq (α := Functor.obj (quotient V c) C ⟶ Functor.obj (quotient V c) C) (𝟙 (Functor.obj (quotient V c) C)) 0

Tactic:
simpa using (eq_of_homotopy _ _ h)

Premises used: HomotopyCategory.eq_of_homotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : CategoryWithHomology.{v, u} V
i : ι
K L : HomologicalComplex.{v, u, u_2} V c
f g : K ⟶ L
h : Homotopy f g
⊢ Eq (α :=
    Functor.obj (HomologicalComplex.homologyFunctor V c i) K ⟶ Functor.obj (HomologicalComplex.homologyFunctor V c i) L)
    (CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor V c i) f)
    (CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor V c i) g)

Tactic:
h.homologyMap_eq i

Premises used: Homotopy.homologyMap_eq, CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : CategoryWithHomology.{v, u} V
i : ι
K L : HomologicalComplex.{v, u, u_2} V c
f g : K ⟶ L
h : Homotopy f g
⊢ Eq (α :=
    Functor.obj (HomologicalComplex.homologyFunctor V c i) K ⟶ Functor.obj (HomologicalComplex.homologyFunctor V c i) L)
    (CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor V c i) f)
    (CategoryTheory.Functor.map (HomologicalComplex.homologyFunctor V c i) g)

Tactic:
exact h.homologyMap_eq i

Premises used: Homotopy.homologyMap_eq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : CategoryWithHomology.{v, u} V
i : ι
⊢ Functor.Additive (C := HomologicalComplex.{v, u, u_2} V c) (quotient V c ⋙ homologyFunctor V c i)

Tactic:
have := Functor.additive_of_iso (homologyFunctorFactors V c i).symm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : CategoryWithHomology.{v, u} V
i : ι
this : Functor.Additive (C := HomologicalComplex.{v, u, u_2} V c) (quotient V c ⋙ homologyFunctor V c i)
⊢ Functor.Additive (C := HomotopyCategory.{v, u, u_2} V c) (homologyFunctor V c i)

Tactic:
Functor.additive_of_full_essSurj_comp (quotient V c) _

Premises used: HomotopyCategory.quotient, CategoryTheory.Functor.additive_of_full_essSurj_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c : ComplexShape ι
inst_3 : CategoryWithHomology.{v, u} V
i : ι
this : Functor.Additive (C := HomologicalComplex.{v, u, u_2} V c) (quotient V c ⋙ homologyFunctor V c i)
⊢ Functor.Additive (C := HomotopyCategory.{v, u, u_2} V c) (homologyFunctor V c i)

Tactic:
exact Functor.additive_of_full_essSurj_comp (quotient V c) _

Premises used: HomotopyCategory.quotient, CategoryTheory.Functor.additive_of_full_essSurj_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_3
inst_2 : Category.{v_1, u_3} W
inst_3 : Preadditive.{v_1, u_3} W
F : Functor.{v, v_1, u, u_3} V W
inst_4 : F.Additive
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_2} V c
f : K ⟶ L
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_3, u_2} W c)
      (obj (F.mapHomotopyCategory c) (obj (HomotopyCategory.quotient V c) K))
      (obj (F.mapHomotopyCategory c) (obj (HomotopyCategory.quotient V c) L)))
    (map (F.mapHomotopyCategory c) (map (HomotopyCategory.quotient V c) f))
    (map (HomotopyCategory.quotient W c) (map (F.mapHomologicalComplex c) f))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c_1 : ComplexShape ι
W : Type u_3
inst_3 : Category.{v_1, u_3} W
inst_4 : Preadditive.{v_1, u_3} W
F G : Functor.{v, v_1, u, u_3} V W
inst_5 : F.Additive
inst_6 : G.Additive
α : F ⟶ G
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_2} V c
f_1 :
  Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c) (Quotient.mk (r := homotopic V c) C)
    (Quotient.mk (r := homotopic V c) D)
f : C ⟶ D
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_3, u_2} W c)
      (Functor.obj (F.mapHomotopyCategory c) (Quotient.mk (r := homotopic V c) C))
      (Functor.obj (G.mapHomotopyCategory c) (Quotient.mk (r := homotopic V c) D)))
    (Functor.map (F.mapHomotopyCategory c) (Quot.mk (HomRel.CompClosure (homotopic V c)) f) ≫
      Functor.map (HomotopyCategory.quotient W c)
        (app (mapHomologicalComplex α c) (Quotient.as (r := homotopic V c) (Quotient.mk (r := homotopic V c) D))))
    (Functor.map (HomotopyCategory.quotient W c)
        (app (mapHomologicalComplex α c) (Quotient.as (r := homotopic V c) (Quotient.mk (r := homotopic V c) C))) ≫
      Functor.map (G.mapHomotopyCategory c) (Quot.mk (HomRel.CompClosure (homotopic V c)) f))

Tactic:
simp only [HomotopyCategory.quot_mk_eq_quotient_map, Functor.mapHomotopyCategory_map,
      ← Functor.map_comp, NatTrans.naturality]

Premises used: HomotopyCategory.quot_mk_eq_quotient_map, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.mapHomotopyCategory_map, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_3
inst_2 : Category.{v_1, u_3} W
inst_3 : Preadditive.{v_1, u_3} W
c : ComplexShape ι
F : Functor.{v, v_1, u, u_3} V W
inst_4 : F.Additive
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c ⥤ HomotopyCategory.{v_1, u_3, u_2} W c) (F.mapHomotopyCategory c)
      (F.mapHomotopyCategory c))
    (mapHomotopyCategory (𝟙 F) c) (𝟙 (F.mapHomotopyCategory c))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c ⥤ HomotopyCategory.{v_1, u_3, u_2} W c) (F.mapHomotopyCategory c)
      (F.mapHomotopyCategory c))
    (mapHomotopyCategory (𝟙 F) c) (𝟙 (F.mapHomotopyCategory c))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
ι : Type u_2
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_3
inst_2 : Category.{v_1, u_3} W
inst_3 : Preadditive.{v_1, u_3} W
c : ComplexShape ι
F G H : Functor.{v, v_1, u, u_3} V W
inst_4 : F.Additive
inst_5 : G.Additive
inst_6 : H.Additive
α : F ⟶ G
β : G ⟶ H
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c ⥤ HomotopyCategory.{v_1, u_3, u_2} W c) (F.mapHomotopyCategory c)
      (H.mapHomotopyCategory c))
    (mapHomotopyCategory (α ≫ β) c)
    (CategoryStruct.comp (Y := G.mapHomotopyCategory c) (mapHomotopyCategory α c) (mapHomotopyCategory β c))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, u_2} V c ⥤ HomotopyCategory.{v_1, u_3, u_2} W c) (F.mapHomotopyCategory c)
      (H.mapHomotopyCategory c))
    (mapHomotopyCategory (α ≫ β) c)
    (CategoryStruct.comp (Y := G.mapHomotopyCategory c) (mapHomotopyCategory α c) (mapHomotopyCategory β c))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c_1 : ComplexShape ι
W : Type u_3
inst_3 : Category.{v_1, u_3} W
inst_4 : Preadditive.{v_1, u_3} W
F : Functor.{v, v_1, u, u_3} V W
inst_5 : F.Additive
c : ComplexShape ι
⊢ Functor.Additive (C := HomotopyCategory.{v, u, u_2} V c) (D := HomotopyCategory.{v_1, u_3, u_2} W c)
    (F.mapHomotopyCategory c)

Tactic:
have := Functor.additive_of_iso (F.mapHomotopyCategoryFactors c).symm
  (HomotopyCategory.quotient V c).additive_of_full_essSurj_comp (F.mapHomotopyCategory c)

Premises used: CategoryTheory.Functor.mapHomotopyCategory, CategoryTheory.Functor.additive_of_iso, CategoryTheory.Iso.symm, HomotopyCategory.quotient, CategoryTheory.Functor.additive_of_full_essSurj_comp, CategoryTheory.Functor.mapHomotopyCategoryFactors
-- Module: Mathlib.Algebra.Homology.HomotopyCategory
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
V : Type u
inst_1 : Category.{v, u} V
inst_2 : Preadditive.{v, u} V
c_1 : ComplexShape ι
W : Type u_3
inst_3 : Category.{v_1, u_3} W
inst_4 : Preadditive.{v_1, u_3} W
F : Functor.{v, v_1, u, u_3} V W
inst_5 : F.Additive
c : ComplexShape ι
inst_6 : Linear.{u_1, v, u} R V
inst_7 : Linear.{u_1, v_1, u_3} R W
inst_8 : Functor.Linear R F
⊢ Functor.Linear R (C := HomotopyCategory.{v, u, u_2} V c) (D := HomotopyCategory.{v_1, u_3, u_2} W c)
    (F.mapHomotopyCategory c)

Tactic:
have := Functor.linear_of_iso R (F.mapHomotopyCategoryFactors c).symm
  (HomotopyCategory.quotient V c).linear_of_full_essSurj_comp (F.mapHomotopyCategory c)

Premises used: CategoryTheory.Functor.mapHomotopyCategory, CategoryTheory.Iso.symm, HomotopyCategory.quotient, CategoryTheory.Functor.linear_of_full_essSurj_comp, CategoryTheory.Functor.linear_of_iso, CategoryTheory.Functor.mapHomotopyCategoryFactors
-- 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
i j : ι
hij : c.Rel i j
inst_4 : HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)
obtain :
  ∀ (hij : c.Rel i (c.next i)) [inst_5 : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)],
    X φ i = biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ X φ i = biprod.{v_1, u_1} (F.X j) (G.X i)

Tactic:
obtain rfl := c.next_eq' hij

Premises used: rfl, ComplexShape.next_eq'
-- 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
i : ι
hij : c.Rel i (c.next i)
inst_4 : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ X φ i = biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)

Tactic:
apply dif_pos hij

Premises used: dif_pos
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
pos : ∀ (h : c.Rel i (c.next i)), IsZero.{v_1, u_1} (X φ i)
neg : ∀ (h : ¬c.Rel i (c.next i)), IsZero.{v_1, u_1} (X φ i)
⊢ IsZero.{v_1, u_1} (X φ i)

Tactic:
by_cases h : 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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
⊢ HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)

Tactic:
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ h
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ IsZero.{v_1, u_1} (X φ i)

Tactic:
IsZero.of_iso ?_ (XIsoBiprod φ _ _ h)

Premises used: CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.homotopyCofiber.XIsoBiprod
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
pos : IsZero.{v_1, u_1} (biprod.{v_1, u_1} (F.X (c.next i)) (G.X i))
⊢ IsZero.{v_1, u_1} (X φ i)

Tactic:
refine IsZero.of_iso ?_ (XIsoBiprod φ _ _ h)

Premises used: CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.homotopyCofiber.XIsoBiprod
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
pos : IsZero.{v_1, u_1} (F.X (c.next i)) ∧ IsZero.{v_1, u_1} (G.X i)
⊢ IsZero.{v_1, u_1} (biprod.{v_1, u_1} (F.X (c.next i)) (G.X i))

Tactic:
simp only [biprod_isZero_iff]

Premises used: CategoryTheory.Limits.biprod_isZero_iff
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ IsZero.{v_1, u_1} (F.X (c.next i)) ∧ IsZero.{v_1, u_1} (G.X i)

Tactic:
⟨hF _ h, hG⟩

Premises used: And.intro
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : c.Rel i (c.next i)
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ IsZero.{v_1, u_1} (F.X (c.next i)) ∧ IsZero.{v_1, u_1} (G.X i)

Tactic:
exact ⟨hF _ h, hG⟩
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : ¬c.Rel i (c.next i)
⊢ IsZero.{v_1, u_1} (X φ i)

Tactic:
hG.of_iso (XIso φ i h)

Premises used: CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.homotopyCofiber.XIso
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hG : IsZero.{v_1, u_1} (G.X i)
hF : ∀ (j : ι), c.Rel i j → IsZero.{v_1, u_1} (F.X j)
h : ¬c.Rel i (c.next i)
⊢ IsZero.{v_1, u_1} (X φ i)

Tactic:
exact hG.of_iso (XIso φ i h)

Premises used: CategoryTheory.Limits.IsZero.of_iso, HomologicalComplex.homotopyCofiber.XIso
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
dsimp :
  Eq.{v_1 + 1} (α := G.X i ⟶ G.X i)
    (CategoryStruct.comp (Y := X φ i)
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi))
      else Iso.inv (XIso φ i hi))
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd
      else Iso.hom (XIso φ i hi)))
    (𝟙 (G.X i))
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i) (sndX φ i) = 𝟙 (G.X i)

Tactic:
dsimp [sndX, inrX]

Premises used: HomologicalComplex.homotopyCofiber.inrX, HomologicalComplex.homotopyCofiber.sndX
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
pos :
  ∀ (hi : c.Rel i (c.next i)),
    CategoryStruct.comp (Y := X φ i)
        (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi)))
        (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd) =
      𝟙 (G.X i)
neg :
  ∀ (hi : ¬c.Rel i (c.next i)),
    CategoryStruct.comp (Y := X φ i) (Iso.inv (XIso φ i hi)) (Iso.hom (XIso φ i hi)) = 𝟙 (G.X i)
⊢ Eq.{v_1 + 1} (α := G.X i ⟶ G.X i)
    (CategoryStruct.comp (Y := X φ i)
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi))
      else Iso.inv (XIso φ i hi))
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd
      else Iso.hom (XIso φ i hi)))
    (𝟙 (G.X i))

Tactic:
split_ifs with hi
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : c.Rel i (c.next i)
⊢ CategoryStruct.comp (Y := X φ i)
      (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
        (Iso.inv (XIsoBiprod φ i (c.next i) hi)))
      (CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
        biprod.snd) =
    𝟙 (G.X i)

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 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
⊢ CategoryStruct.comp (Y := X φ i) (Iso.inv (XIso φ i hi)) (Iso.hom (XIso φ i hi)) = 𝟙 (G.X i)

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 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
dsimp :
  Eq.{v_1 + 1} (α := X φ i ⟶ X φ i)
    (CategoryStruct.comp (Y := G.X i)
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd
      else Iso.hom (XIso φ i hi))
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi))
      else Iso.inv (XIso φ i hi)))
    (𝟙 (X φ i))
⊢ sndX φ i ≫ inrX φ i = 𝟙 (X φ i)

Tactic:
dsimp [sndX, inrX]

Premises used: HomologicalComplex.homotopyCofiber.inrX, HomologicalComplex.homotopyCofiber.sndX
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
⊢ Eq.{v_1 + 1} (α := X φ i ⟶ X φ i)
    (CategoryStruct.comp (Y := G.X i)
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (Iso.hom (XIsoBiprod φ i (c.next i) hi))
          biprod.snd
      else Iso.hom (XIso φ i hi))
      (if hi : c.Rel i (c.next i) then
        CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) biprod.inr
          (Iso.inv (XIsoBiprod φ i (c.next i) hi))
      else Iso.inv (XIso φ i hi)))
    (𝟙 (X φ i))

Tactic:
simp only [dif_neg hi, Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id, dif_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 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ i j hij) (fstX φ j i hij) = 𝟙 (F.X i)

Tactic:
simp [inlX, fstX]

Premises used: HomologicalComplex.homotopyCofiber.fstX, HomologicalComplex.homotopyCofiber.inlX
-- 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
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
obtain : ∀ (hij : c.Rel j (c.next j)), CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hij) (sndX φ j) = 0
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ i j hij) (sndX φ j) = 0

Tactic:
obtain rfl := c.next_eq' hij

Premises used: rfl, ComplexShape.next_eq'