awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
zero :
  Eq (α := C.X 0 ⟶ D.X 0)
    (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next 0)) (C.d 0 ((ComplexShape.down ℕ).next 0))
      (f ((ComplexShape.down ℕ).next 0) 0))
    (CategoryStruct.comp (Y := C.X (HSub.hSub (α := ℕ) 0 1)) (C.d 0 (HSub.hSub (α := ℕ) 0 1))
      (f (HSub.hSub (α := ℕ) 0 1) 0))
succ :
  ∀ (n : ℕ),
    Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
      (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next (n + 1)))
        (C.d (n + 1) ((ComplexShape.down ℕ).next (n + 1))) (f ((ComplexShape.down ℕ).next (n + 1)) (n + 1)))
      (CategoryStruct.comp (Y := C.X (n + 1 - 1)) (C.d (n + 1) (n + 1 - 1)) (f (n + 1 - 1) (n + 1)))
⊢ CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next i)) (C.d i ((ComplexShape.down ℕ).next i))
      (f ((ComplexShape.down ℕ).next i) i) =
    CategoryStruct.comp (Y := C.X (i - 1)) (C.d i (i - 1)) (f (i - 1) i)

Tactic:
cases i
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ Eq (α := C.X 0 ⟶ D.X 0)
    (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next 0)) (C.d 0 ((ComplexShape.down ℕ).next 0))
      (f ((ComplexShape.down ℕ).next 0) 0))
    (CategoryStruct.comp (Y := C.X (HSub.hSub (α := ℕ) 0 1)) (C.d 0 (HSub.hSub (α := ℕ) 0 1))
      (f (HSub.hSub (α := ℕ) 0 1) 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n : ℕ
succ succ₁ succ₂ : (ComplexShape.down ℕ).next (n + 1) = n + 1 - 1
⊢ Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
    (CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next (n + 1)))
      (C.d (n + 1) ((ComplexShape.down ℕ).next (n + 1))) (f ((ComplexShape.down ℕ).next (n + 1)) (n + 1)))
    (CategoryStruct.comp (Y := C.X (n + 1 - 1)) (C.d (n + 1) (n + 1 - 1)) (f (n + 1 - 1) (n + 1)))

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n + 1 - 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
dsimp :
  CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev i)) (f i ((ComplexShape.up ℕ).prev i))
      (D.d ((ComplexShape.up ℕ).prev i) i) =
    CategoryStruct.comp (Y := D.X (i - 1)) (f i (i - 1)) (D.d (i - 1) i)
⊢ (prevD i : (a : (i j : ℕ) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f =
    CategoryStruct.comp (Y := D.X (i - 1)) (f i (i - 1)) (D.d (i - 1) i)

Tactic:
dsimp [prevD]

Premises used: prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
zero :
  Eq (α := C.X 0 ⟶ D.X 0)
    (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev 0)) (f 0 ((ComplexShape.up ℕ).prev 0))
      (D.d ((ComplexShape.up ℕ).prev 0) 0))
    (CategoryStruct.comp (Y := D.X (HSub.hSub (α := ℕ) 0 1)) (f 0 (HSub.hSub (α := ℕ) 0 1))
      (D.d (HSub.hSub (α := ℕ) 0 1) 0))
succ :
  ∀ (n : ℕ),
    Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
      (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev (n + 1))) (f (n + 1) ((ComplexShape.up ℕ).prev (n + 1)))
        (D.d ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)))
      (CategoryStruct.comp (Y := D.X (n + 1 - 1)) (f (n + 1) (n + 1 - 1)) (D.d (n + 1 - 1) (n + 1)))
⊢ CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev i)) (f i ((ComplexShape.up ℕ).prev i))
      (D.d ((ComplexShape.up ℕ).prev i) i) =
    CategoryStruct.comp (Y := D.X (i - 1)) (f i (i - 1)) (D.d (i - 1) i)

Tactic:
cases i
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ Eq (α := C.X 0 ⟶ D.X 0)
    (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev 0)) (f 0 ((ComplexShape.up ℕ).prev 0))
      (D.d ((ComplexShape.up ℕ).prev 0) 0))
    (CategoryStruct.comp (Y := D.X (HSub.hSub (α := ℕ) 0 1)) (f 0 (HSub.hSub (α := ℕ) 0 1))
      (D.d (HSub.hSub (α := ℕ) 0 1) 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n : ℕ
succ succ₁ succ₂ : (ComplexShape.up ℕ).prev (n + 1) = n + 1 - 1
⊢ Eq (α := C.X (n + 1) ⟶ D.X (n + 1))
    (CategoryStruct.comp (Y := D.X ((ComplexShape.up ℕ).prev (n + 1))) (f (n + 1) ((ComplexShape.up ℕ).prev (n + 1)))
      (D.d ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)))
    (CategoryStruct.comp (Y := D.X (n + 1 - 1)) (f (n + 1) (n + 1 - 1)) (D.d (n + 1 - 1) (n + 1)))

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
n : ℕ
⊢ (ComplexShape.up ℕ).prev (n + 1) = n + 1 - 1

Tactic:
simp
-- 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_1 : ι
h : Homotopy f g
i : ι
⊢ (f - g).f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) fun (i j : ι) ↦ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) fun (i j : ι) ↦ h.hom i j) +
      Hom.f 0 i

Tactic:
simp [h.comm]

Premises used: Homotopy.comm
-- 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_1 : ι
h : Homotopy (f - g) 0
i : ι
⊢ f.f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) fun (i j : ι) ↦ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) fun (i j : ι) ↦ h.hom i j) +
      g.f i

Tactic:
simpa [sub_eq_iff_eq_add] using h.comm i

Premises used: sub_eq_iff_eq_add, Homotopy.comm
-- 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 : ι
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬c.Rel j i
rw : (-h.hom i) j = 0
rw₁ : -h.hom i j = 0
rw₂ : Eq.{v + 1} (α := C.X i ⟶ D.X j) (-0) 0
rw₃ rw₄ : Eq.{v + 1} (α := C.X i ⟶ D.X j) 0 0
⊢ (-h.hom) i j = 0

Tactic:
rw [Pi.neg_apply, Pi.neg_apply, h.zero i j w, neg_zero]

Premises used: Homotopy.zero, neg_zero, Pi.neg_apply
-- 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 : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
rw :
  g.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) +
      f.f i
rw₁ :
  g.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) +
      f.f i
rw₂ :
  g.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) +
      (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)
rw₃ :
  g.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) +
      (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)
rw₄ :
  g.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) +
        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
rw₅ : g.f i = 0 + g.f i
rw₆ rw₇ : g.f i = g.f i
⊢ g.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) +
      f.f i

Tactic:
rw [map_neg, map_neg, h.comm, ← neg_add, ← add_assoc, neg_add_cancel, zero_add]

Premises used: add_assoc, neg_add, map_neg, zero_add, neg_add_cancel, Homotopy.comm
-- 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_1 : D ⟶ E
i_1 : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j i
rw : (h.hom i + k.hom i) j = 0
rw₁ : h.hom i j + k.hom i j = 0
rw₂ : 0 + k.hom i j = 0
rw₃ : HAdd.hAdd (α := C.X i ⟶ D.X j) 0 0 = 0
rw₄ rw₅ : Eq.{v + 1} (α := C.X i ⟶ D.X j) 0 0
⊢ (h.hom + k.hom) i j = 0

Tactic:
rw [Pi.add_apply, Pi.add_apply, h.zero i j w, k.zero i j w, zero_add]

Premises used: Homotopy.zero, zero_add, Pi.add_apply
-- 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_1 : D ⟶ E
i_1 : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i : ι
⊢ e.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 + k.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 + k.hom) : C.X i ⟶ D.X i) +
      g.f i

Tactic:
grind [Homotopy.comm]

Premises used: Homotopy.comm
-- 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 k : D ⟶ E
i_1 : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
rw : (h₁.hom i + h₂.hom i) j = 0
rw₁ : h₁.hom i j + h₂.hom i j = 0
rw₂ : 0 + h₂.hom i j = 0
rw₃ : HAdd.hAdd (α := C.X i ⟶ D.X j) 0 0 = 0
rw₄ rw₅ : Eq.{v + 1} (α := C.X i ⟶ D.X j) 0 0
⊢ (h₁.hom + h₂.hom) i j = 0

Tactic:
rw [Pi.add_apply, Pi.add_apply, h₁.zero i j hij, h₂.zero i j hij, add_zero]

Premises used: Homotopy.zero, Pi.add_apply, add_zero
-- 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 k : D ⟶ E
i_1 : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i : ι
⊢ (f₁ + 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 + 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 + h₂.hom) : C.X i ⟶ D.X i) +
      (g₁ + g₂).f i

Tactic:
grind [HomologicalComplex.add_f_apply, Homotopy.comm]

Premises used: HomologicalComplex.add_f_apply, Homotopy.comm
-- 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_1 : ι
R : Type u_2
inst_2 : Semiring R
inst_3 : Linear.{u_2, v, u} R V
h : Homotopy f g
a : R
i j : ι
hij : ¬c.Rel j i
rw : HSMul.hSMul (β := C.X i ⟶ D.X j) a 0 = 0
rw₁ rw₂ : Eq.{v + 1} (α := C.X i ⟶ D.X j) 0 0
⊢ a • h.hom i j = 0

Tactic:
rw [h.zero i j hij, smul_zero]

Premises used: smul_zero, Homotopy.zero
-- 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_1 : ι
R : Type u_2
inst_2 : Semiring R
inst_3 : Linear.{u_2, v, u} R V
h : Homotopy f g
a : R
i : ι
dsimp :
  a • f.f i =
    (C.dFrom i ≫ (fromNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.xNext i ⟶ D.X i) fun (i j : ι) ↦ a • h.hom i j) +
        ((toPrev i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.xPrev i) fun (i j : ι) ↦ a • h.hom i j) ≫ D.dTo i +
      a • g.f i
⊢ (a • f).f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) fun (i j : ι) ↦ a • h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) fun (i j : ι) ↦ a • h.hom i j) +
      (a • g).f i

Tactic:
dsimp
-- 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_1 : ι
R : Type u_2
inst_2 : Semiring R
inst_3 : Linear.{u_2, v, u} R V
h : Homotopy f g
a : R
i : ι
rw :
  a •
      (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) =
    (C.dFrom i ≫ (fromNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.xNext i ⟶ D.X i) fun (i j : ι) ↦ a • h.hom i j) +
        ((toPrev i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.xPrev i) fun (i j : ι) ↦ a • h.hom i j) ≫ D.dTo i +
      a • g.f i
⊢ a • f.f i =
    (C.dFrom i ≫ (fromNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.xNext i ⟶ D.X i) fun (i j : ι) ↦ a • h.hom i j) +
        ((toPrev i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.xPrev i) fun (i j : ι) ↦ a • h.hom i j) ≫ D.dTo i +
      a • g.f i

Tactic:
rw [h.comm]

Premises used: Homotopy.comm
-- 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_1 : ι
R : Type u_2
inst_2 : Semiring R
inst_3 : Linear.{u_2, v, u} R V
h : Homotopy f g
a : R
i : ι
dsimp :
  a • (C.dFrom i ≫ h.hom (c.next i) i + h.hom i (c.prev i) ≫ D.dTo i + g.f i) =
    C.dFrom i ≫ HSMul.hSMul (β := C.X (c.next i) ⟶ D.X i) a (h.hom (c.next i) i) +
        HSMul.hSMul (β := C.X i ⟶ D.X (c.prev i)) a (h.hom i (c.prev i)) ≫ D.dTo i +
      a • g.f i
⊢ a •
      (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) =
    (C.dFrom i ≫ (fromNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.xNext i ⟶ D.X i) fun (i j : ι) ↦ a • h.hom i j) +
        ((toPrev i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.xPrev i) fun (i j : ι) ↦ a • h.hom i j) ≫ D.dTo i +
      a • g.f i

Tactic:
dsimp [fromNext, toPrev]

Premises used: fromNext, toPrev
-- 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_1 : ι
R : Type u_2
inst_2 : Semiring R
inst_3 : Linear.{u_2, v, u} R V
h : Homotopy f g
a : R
i : ι
⊢ a • (C.dFrom i ≫ h.hom (c.next i) i + h.hom i (c.prev i) ≫ D.dTo i + g.f i) =
    C.dFrom i ≫ HSMul.hSMul (β := C.X (c.next i) ⟶ D.X i) a (h.hom (c.next i) i) +
        HSMul.hSMul (β := C.X i ⟶ D.X (c.prev i)) a (h.hom i (c.prev i)) ≫ D.dTo i +
      a • g.f i

Tactic:
simp only [smul_add, Linear.comp_smul, Linear.smul_comp]

Premises used: CategoryTheory.Linear.comp_smul, smul_add, CategoryTheory.Linear.smul_comp
-- 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 : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i j : ι
w : ¬c.Rel j i
rw : Eq (α := C.X i ⟶ E.X j) (0 ≫ g.f j) 0
rw₁ rw₂ : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
⊢ h.hom i j ≫ g.f j = 0

Tactic:
rw [h.zero i j w, zero_comp]

Premises used: Homotopy.zero, CategoryTheory.Limits.zero_comp
-- 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 : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i j : ι
w : ¬c.Rel j i
rw : Eq (α := C.X i ⟶ E.X j) (e.f i ≫ 0) 0
rw₁ rw₂ : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
⊢ e.f i ≫ h.hom i j = 0

Tactic:
rw [h.zero i j w, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, Homotopy.zero
-- 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 k : D ⟶ E
i_1 : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X j)
    ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom ≫ D.d i j : C.X i ⟶ D.X j) (0 : C.X i ⟶ D.X j)

Tactic:
simp only [prevD, AddMonoidHom.mk'_apply, assoc, d_comp_d, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, HomologicalComplex.d_comp_d, AddMonoidHom.mk'_apply, 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 g : C ⟶ D
h k : D ⟶ E
i_1 : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X j)
    ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom ≫ D.d i j : C.X i ⟶ D.X j) (0 : C.X i ⟶ D.X j)

Tactic:
have eq1 : prevD i hom ≫ D.d i j = 0 := by
      simp only [prevD, AddMonoidHom.mk'_apply, assoc, d_comp_d, comp_zero]
-- 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 k : D ⟶ E
i_1 : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 :
  Eq.{v + 1} (α := C.X i ⟶ D.X j)
    ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom ≫ D.d i j : C.X i ⟶ D.X j) (0 : C.X i ⟶ D.X j)
⊢ Eq (α := C.X i ⟶ D.X j) (C.d i j ≫ (dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom) 0

Tactic:
simp only [dNext, AddMonoidHom.mk'_apply, d_comp_d_assoc, zero_comp]

Premises used: HomologicalComplex.d_comp_d_assoc, dNext, AddMonoidHom.mk'_apply, CategoryTheory.Limits.zero_comp
-- 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 k : D ⟶ E
i_1 : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 :
  Eq.{v + 1} (α := C.X i ⟶ D.X j)
    ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom ≫ D.d i j : C.X i ⟶ D.X j) (0 : C.X i ⟶ D.X j)
⊢ Eq (α := C.X i ⟶ D.X j) (C.d i j ≫ (dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom) 0

Tactic:
have eq2 : C.d i j ≫ dNext j hom = 0 := by
      simp only [dNext, AddMonoidHom.mk'_apply, d_comp_d_assoc, zero_comp]
-- 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 k : D ⟶ E
i_1 : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 :
  Eq.{v + 1} (α := C.X i ⟶ D.X j)
    ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom ≫ D.d i j : C.X i ⟶ D.X j) (0 : C.X i ⟶ D.X j)
eq2 : Eq (α := C.X i ⟶ D.X j) (C.d i j ≫ (dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom) 0
rw :
  HAdd.hAdd (β := C.X i ⟶ D.X i) (C.d i j ≫ hom j i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i) ≫
      D.d i j =
    C.d i j ≫
      HAdd.hAdd (α := C.X j ⟶ D.X j) (β := C.X j ⟶ D.X j)
        ((dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom : C.X j ⟶ D.X j)
        ((prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom : C.X j ⟶ D.X j)
rw₁ :
  HAdd.hAdd (β := C.X i ⟶ D.X i) (C.d i j ≫ hom j i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i) ≫
      D.d i j =
    C.d i j ≫
      HAdd.hAdd (α := C.X j ⟶ D.X j) ((dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom : C.X j ⟶ D.X j)
        (hom j i ≫ D.d i j)
rw₂ :
  HAdd.hAdd (β := C.X i ⟶ D.X i) (C.d i j ≫ hom j i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i) ≫
      D.d i j =
    C.d i j ≫ (dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom + C.d i j ≫ hom j i ≫ D.d i j
rw₃ :
  HAdd.hAdd (β := C.X i ⟶ D.X j) ((C.d i j ≫ hom j i) ≫ D.d i j)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom ≫ D.d i j : C.X i ⟶ D.X j) =
    C.d i j ≫ (dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom + C.d i j ≫ hom j i ≫ D.d i j
rw₄ :
  (C.d i j ≫ hom j i) ≫ D.d i j + 0 =
    C.d i j ≫ (dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom + C.d i j ≫ hom j i ≫ D.d i j
rw₅ : (C.d i j ≫ hom j i) ≫ D.d i j + 0 = 0 + C.d i j ≫ hom j i ≫ D.d i j
rw₆ : (C.d i j ≫ hom j i) ≫ D.d i j = 0 + C.d i j ≫ hom j i ≫ D.d i j
rw₇ : (C.d i j ≫ hom j i) ≫ D.d i j = C.d i j ≫ hom j i ≫ D.d i j
rw₈ rw₉ : C.d i j ≫ hom j i ≫ D.d i j = C.d i j ≫ hom j i ≫ D.d i j
⊢ 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) hom : C.X i ⟶ D.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i) ≫
      D.d i j =
    C.d i j ≫
      HAdd.hAdd (α := C.X j ⟶ D.X j) (β := C.X j ⟶ D.X j)
        ((dNext j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom : C.X j ⟶ D.X j)
        ((prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) hom : C.X j ⟶ D.X j)

Tactic:
rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]

Premises used: CategoryTheory.Category.assoc, prevD_eq, zero_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, dNext_eq, add_zero
-- 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
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
h : ∀ (n : ι), (nullHomotopicMap hom ≫ g).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ hom i j ≫ g.f j) n
⊢ nullHomotopicMap hom ≫ g = nullHomotopicMap fun (i j : ι) ↦ hom i j ≫ g.f j

Tactic:
ext n