awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 (α := (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ (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
have 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
Tactic: rw [L.shape _ _ h, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ (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
have neg₁ : Eq.{v_1 + 1} (α := K.X (c.prev i) ⟶ L.X i) 0 0
Tactic: rw [L.shape _ _ h, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ ((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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ ((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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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
have 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
Tactic: rw [K.shape _ _ h, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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
have neg₁ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X (c.next i)) 0 0
Tactic: rw [K.shape _ _ h, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ 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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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) =
    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)
have 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)
Tactic: rw [ho.comm (c.prev i)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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)
have 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)
Tactic: dsimp [dFrom, dTo, fromNext, toPrev]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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)
have 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)
Tactic: rw [congr_arg (fun j => d K (c.prev i) j ≫ ho.hom j (c.prev i)) (c.next_eq' h)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ ShortComplex.Hom.τ₃ (CategoryTheory.Functor.map (shortComplexFunctor C c i) f) =
    (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)) +
        ho.hom (c.next i) i ≫ (Functor.obj (shortComplexFunctor C c i) L).g +
      ShortComplex.Hom.τ₃ (CategoryTheory.Functor.map (shortComplexFunctor C c i) g)
have dsimp : f.f (c.next i) =
  (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)) +
      ho.hom (c.next i) i ≫ L.d i (c.next i) +
    g.f (c.next i)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ f.f (c.next i) =
    (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)) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
have pos : ∀ (h : c.Rel i (c.next i)),
  f.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (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)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)
Tactic: split_ifs with h