awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f_1 g_1 : C ⟶ D
h_1 k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
f g : C ⟶ D
h : Homotopy f g
i : ι
H :
  f.f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) +
      g.f i
dsimp :
  F.map (f.f i) =
    CategoryStruct.comp (Y := F.obj (C.X (c.next i))) (F.map (C.d i (c.next i))) (F.map (h.hom (c.next i) i)) +
        CategoryStruct.comp (Y := F.obj (D.X (c.prev i))) (F.map (h.hom i (c.prev i))) (F.map (D.d (c.prev i) i)) +
      F.map (g.f i)
⊢ Hom.f (map (F.mapHomologicalComplex c) f) i =
    HAdd.hAdd (α := X (obj (F.mapHomologicalComplex c) C) i ⟶ X (obj (F.mapHomologicalComplex c) D) i)
        ((dNext i :
            (a : (i j : ι) → ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X j) →
              ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X i)
          fun (i j : ι) ↦ F.map (h.hom i j))
        ((prevD i :
            (a : (i j : ι) → ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X j) →
              ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X i)
          fun (i j : ι) ↦ F.map (h.hom i j)) +
      Hom.f (map (F.mapHomologicalComplex c) g) i

Tactic:
dsimp [dNext, prevD] at H ⊢

Premises used: dNext, prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f_1 g_1 : C ⟶ D
h_1 k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
f g : C ⟶ D
h : Homotopy f g
i : ι
H :
  f.f i =
    CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (h.hom (c.next i) i) +
        CategoryStruct.comp (Y := D.X (c.prev i)) (h.hom i (c.prev i)) (D.d (c.prev i) i) +
      g.f i
⊢ F.map (f.f i) =
    CategoryStruct.comp (Y := F.obj (C.X (c.next i))) (F.map (C.d i (c.next i))) (F.map (h.hom (c.next i) i)) +
        CategoryStruct.comp (Y := F.obj (D.X (c.prev i))) (F.map (h.hom i (c.prev i))) (F.map (D.d (c.prev i) i)) +
      F.map (g.f i)

Tactic:
simp [H]
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h_1 k : D ⟶ E
i : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
h : HomotopyEquiv C D
rw :
  Homotopy (C := obj (F.mapHomologicalComplex c) C) (map (F.mapHomologicalComplex c) (h.hom ≫ h.inv))
    (map (F.mapHomologicalComplex c) (𝟙 C))
⊢ Homotopy (C := obj (F.mapHomologicalComplex c) C)
    (map (F.mapHomologicalComplex c) h.hom ≫ map (F.mapHomologicalComplex c) h.inv)
    (𝟙 (obj (F.mapHomologicalComplex c) C))

Tactic:
rw [← (F.mapHomologicalComplex c).map_comp, ← (F.mapHomologicalComplex c).map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapHomologicalComplex
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h_1 k : D ⟶ E
i : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
h : HomotopyEquiv C D
⊢ Homotopy (C := obj (F.mapHomologicalComplex c) C) (map (F.mapHomologicalComplex c) (h.hom ≫ h.inv))
    (map (F.mapHomologicalComplex c) (𝟙 C))

Tactic:
exact F.mapHomotopy h.homotopyHomInvId

Premises used: CategoryTheory.Functor.mapHomotopy, HomotopyEquiv.homotopyHomInvId
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h_1 k : D ⟶ E
i : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
h : HomotopyEquiv C D
rw :
  Homotopy (C := obj (F.mapHomologicalComplex c) D) (map (F.mapHomologicalComplex c) (h.inv ≫ h.hom))
    (map (F.mapHomologicalComplex c) (𝟙 D))
⊢ Homotopy (C := obj (F.mapHomologicalComplex c) D)
    (map (F.mapHomologicalComplex c) h.inv ≫ map (F.mapHomologicalComplex c) h.hom)
    (𝟙 (obj (F.mapHomologicalComplex c) D))

Tactic:
rw [← (F.mapHomologicalComplex c).map_comp, ← (F.mapHomologicalComplex c).map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.mapHomologicalComplex
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h_1 k : D ⟶ E
i : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
h : HomotopyEquiv C D
⊢ Homotopy (C := obj (F.mapHomologicalComplex c) D) (map (F.mapHomologicalComplex c) (h.inv ≫ h.hom))
    (map (F.mapHomologicalComplex c) (𝟙 D))

Tactic:
exact F.mapHomotopy h.homotopyInvHomId

Premises used: CategoryTheory.Functor.mapHomotopy, HomotopyEquiv.homotopyInvHomId
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
pos :
  ∀ (h : c.Rel (c.prev i) i),
    Eq (α := (Functor.obj (shortComplexFunctor C c i) K).X₁ ⟶ (Functor.obj (shortComplexFunctor C c i) L).X₂)
      (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i)) ≫
        (Functor.obj (shortComplexFunctor C c i) L).f)
      0
neg :
  ∀ (h : ¬c.Rel (c.prev i) i),
    (HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
          K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫
        (Functor.obj (shortComplexFunctor C c i) L).f =
      0
⊢ (if c.Rel (c.prev i) i then
        CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))
      else
        HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
          K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫
      (Functor.obj (shortComplexFunctor C c i) L).f =
    0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel (c.prev i) i
pos :
  Eq (α := K.X (c.prev i) ⟶ L.X i)
    (CategoryStruct.comp (Y := L.X (c.prev i))
      (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
        (L.d (c.prev (c.prev i)) (c.prev i)))
      (L.d (c.prev i) i))
    0
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c i) K).X₁ ⟶ (Functor.obj (shortComplexFunctor C c i) L).X₂)
    (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
        (L.d (c.prev (c.prev i)) (c.prev i)) ≫
      (Functor.obj (shortComplexFunctor C c i) L).f)
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel (c.prev i) i
⊢ Eq (α := K.X (c.prev i) ⟶ L.X i)
    (CategoryStruct.comp (Y := L.X (c.prev i))
      (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
        (L.d (c.prev (c.prev i)) (c.prev i)))
      (L.d (c.prev i) i))
    0

Tactic:
simp only [assoc, d_comp_d, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, HomologicalComplex.d_comp_d
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel (c.prev i) i
neg :
  (HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
        K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫
      L.d (c.prev i) i =
    0
⊢ (HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
        K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫
      (Functor.obj (shortComplexFunctor C c i) L).f =
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel (c.prev i) i
neg :
  Eq (α := K.X (c.prev i) ⟶ L.X i)
    ((HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
        K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫
      0)
    0
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.X (c.prev i) ⟶ L.X i) 0 0
⊢ (HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
        K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫
      L.d (c.prev i) i =
    0

Tactic:
rw [L.shape _ _ h, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
pos :
  ∀ (h : c.Rel i (c.next i)),
    Eq (α := (Functor.obj (shortComplexFunctor C c i) K).X₂ ⟶ (Functor.obj (shortComplexFunctor C c i) L).X₃)
      ((Functor.obj (shortComplexFunctor C c i) K).g ≫
        CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
      0
neg :
  ∀ (h : ¬c.Rel i (c.next i)),
    (Functor.obj (shortComplexFunctor C c i) K).g ≫
        (HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
          ho.hom (c.next i) i ≫ L.d i (c.next i)) =
      0
⊢ ((Functor.obj (shortComplexFunctor C c i) K).g ≫
      if c.Rel i (c.next i) then
        CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i))
      else
        HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
          ho.hom (c.next i) i ≫ L.d i (c.next i)) =
    0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c i) K).X₂ ⟶ (Functor.obj (shortComplexFunctor C c i) L).X₃)
    ((Functor.obj (shortComplexFunctor C c i) K).g ≫
      CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
        (ho.hom (c.next (c.next i)) (c.next i)))
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
neg :
  K.d i (c.next i) ≫
      (HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
        ho.hom (c.next i) i ≫ L.d i (c.next i)) =
    0
⊢ (Functor.obj (shortComplexFunctor C c i) K).g ≫
      (HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
        ho.hom (c.next i) i ≫ L.d i (c.next i)) =
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
neg :
  Eq (α := K.X i ⟶ L.X (c.next i))
    (0 ≫
      (HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
        ho.hom (c.next i) i ≫ L.d i (c.next i)))
    0
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X (c.next i)) 0 0
⊢ K.d i (c.next i) ≫
      (HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
        ho.hom (c.next i) i ≫ L.d i (c.next i)) =
    0

Tactic:
rw [K.shape _ _ h, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
dsimp :
  f.f (c.prev i) =
    (K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        if c.Rel (c.prev i) i then
          CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
            (L.d (c.prev (c.prev i)) (c.prev i))
        else
          HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
            K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)
⊢ ShortComplex.Hom.τ₁ (CategoryTheory.Functor.map (shortComplexFunctor C c i) f) =
    ((Functor.obj (shortComplexFunctor C c i) K).f ≫ ho.hom i (c.prev i) +
        if c.Rel (c.prev i) i then
          CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
            (L.d (c.prev (c.prev i)) (c.prev i))
        else
          HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
            K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      ShortComplex.Hom.τ₁ (CategoryTheory.Functor.map (shortComplexFunctor C c i) g)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
pos :
  ∀ (h : c.Rel (c.prev i) i),
    f.f (c.prev i) =
      HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
          (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
            (L.d (c.prev (c.prev i)) (c.prev i))) +
        g.f (c.prev i)
neg :
  ∀ (h : ¬c.Rel (c.prev i) i),
    f.f (c.prev i) =
      K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
          (HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
            K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
        g.f (c.prev i)
⊢ f.f (c.prev i) =
    (K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        if c.Rel (c.prev i) i then
          CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
            (L.d (c.prev (c.prev i)) (c.prev i))
        else
          HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
            K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel (c.prev i) i
pos :
  HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (β := K.X (c.prev i) ⟶ L.X (c.prev i))
        ((dNext (c.prev i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.prev i) ⟶ L.X (c.prev i)) ho.hom :
          K.X (c.prev i) ⟶ L.X (c.prev i))
        ((prevD (c.prev i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.prev i) ⟶ L.X (c.prev i)) ho.hom :
          K.X (c.prev i) ⟶ L.X (c.prev i)) +
      g.f (c.prev i) =
    HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
        (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i)
⊢ f.f (c.prev i) =
    HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
        (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i)

Tactic:
rw [ho.comm (c.prev i)]

Premises used: ComplexShape.prev, Homotopy.comm
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel (c.prev i) i
pos :
  HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i))
        (CategoryStruct.comp (Y := K.xNext (c.prev i)) (K.d (c.prev i) (c.next (c.prev i)))
          (ho.hom (c.next (c.prev i)) (c.prev i)))
        (CategoryStruct.comp (Y := L.xPrev (c.prev i)) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i) =
    HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
        (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i)
⊢ HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (β := K.X (c.prev i) ⟶ L.X (c.prev i))
        ((dNext (c.prev i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.prev i) ⟶ L.X (c.prev i)) ho.hom :
          K.X (c.prev i) ⟶ L.X (c.prev i))
        ((prevD (c.prev i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.prev i) ⟶ L.X (c.prev i)) ho.hom :
          K.X (c.prev i) ⟶ L.X (c.prev i)) +
      g.f (c.prev i) =
    HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
        (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i)

Tactic:
dsimp [dFrom, dTo, fromNext, toPrev]

Premises used: fromNext, HomologicalComplex.dTo, HomologicalComplex.dFrom, toPrev
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel (c.prev i) i
pos pos₁ :
  HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
        (CategoryStruct.comp (Y := L.xPrev (c.prev i)) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i) =
    HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
        (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i)
⊢ HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i))
        (CategoryStruct.comp (Y := K.xNext (c.prev i)) (K.d (c.prev i) (c.next (c.prev i)))
          (ho.hom (c.next (c.prev i)) (c.prev i)))
        (CategoryStruct.comp (Y := L.xPrev (c.prev i)) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i) =
    HAdd.hAdd (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (K.d (c.prev i) i ≫ ho.hom i (c.prev i))
        (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))) +
      g.f (c.prev i)

Tactic:
rw [congr_arg (fun j => d K (c.prev i) j ≫ ho.hom j (c.prev i)) (c.next_eq' h)]

Premises used: Homotopy.hom, ComplexShape.prev, congr_arg, CategoryTheory.CategoryStruct.comp, ComplexShape.next_eq', HomologicalComplex.d
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel (c.prev i) i
⊢ f.f (c.prev i) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        (HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
          K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)

Tactic:
abel