awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 • 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
have 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
Tactic: rw [h.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 •
      (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
have 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
Tactic: dsimp [fromNext, toPrev]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ h.hom i j ≫ g.f j = 0
have rw : Eq (α := C.X i ⟶ E.X j) (0 ≫ g.f j) 0
Tactic: rw [h.zero i j w, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ h.hom i j ≫ g.f j = 0
have rw₁ : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
Tactic: rw [h.zero i j w, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ (e ≫ g).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
have rw : e.f i ≫ g.f i =
  HAdd.hAdd (α := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
    (f ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp,
    comp_f, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
rw :
  e.f i ≫ g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
⊢ (e ≫ g).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
have rw₁ : (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) ≫
    g.f i =
  HAdd.hAdd (α := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
    (f ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp,
    comp_f, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
rw :
  e.f i ≫ g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
rw₁ :
  (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) ≫
      g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
⊢ (e ≫ g).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
have rw₂ : (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) ≫
    g.f i =
  HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j : C.X i ⟶ E.X i) +
    (f ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp,
    comp_f, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
rw :
  e.f i ≫ g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
rw₁ :
  (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) ≫
      g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
rw₂ :
  (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) ≫
      g.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j :
          C.X i ⟶ E.X i) +
      (f ≫ g).f i
⊢ (e ≫ g).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ h.hom i j ≫ g.f j) +
      (f ≫ g).f i
have rw₃ : (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) ≫
    g.f i =
  HAdd.hAdd (α := C.X i ⟶ E.X i) (β := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom ≫ g.f i : C.X i ⟶ E.X i) +
    (f ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp,
    comp_f, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ e.f i ≫ h.hom i j = 0
have rw : Eq (α := C.X i ⟶ E.X j) (e.f i ≫ 0) 0
Tactic: rw [h.zero i j w, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ e.f i ≫ h.hom i j = 0
have rw₁ : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
Tactic: rw [h.zero i j w, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ (e ≫ f).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
have rw : e.f i ≫ f.f i =
  HAdd.hAdd (α := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
    (e ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_left, prevD_comp_left, comp_f,
    Preadditive.comp_add, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
rw :
  e.f i ≫ f.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
⊢ (e ≫ f).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
have rw₁ : e.f i ≫
    (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
      g.f i) =
  HAdd.hAdd (α := C.X i ⟶ E.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
    (e ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_left, prevD_comp_left, comp_f,
    Preadditive.comp_add, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
rw :
  e.f i ≫ f.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₁ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
⊢ (e ≫ f).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
have rw₂ : e.f i ≫
    (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
      g.f i) =
  HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
    (e ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_left, prevD_comp_left, comp_f,
    Preadditive.comp_add, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
rw :
  e.f i ≫ f.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₁ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₂ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
⊢ (e ≫ f).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
have rw₃ : e.f i ≫
    (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
      g.f i) =
  HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
      (e.f i ≫ (prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom) +
    (e ≫ g).f i
Tactic: rw [comp_f, h.comm i, dNext_comp_left, prevD_comp_left, comp_f,
    Preadditive.comp_add, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
rw :
  e.f i ≫ f.f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₁ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₂ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
rw₃ :
  e.f i ≫
      (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
          ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
          ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
        g.f i) =
    HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
        (e.f i ≫ (prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom) +
      (e ≫ g).f i
⊢ (e ≫ f).f i =
    HAdd.hAdd (α := C.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ e.f i ≫ h.hom i j) +
      (e ≫ g).f i
have rw₄ : e.f i ≫
    (HAdd.hAdd (α := D.X i ⟶ E.X i) (β := D.X i ⟶ E.X i)
        ((dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i)
        ((prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom : D.X i ⟶ E.X i) +
      g.f i) =
  HAdd.hAdd (α := C.X i ⟶ E.X i) (e.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom)
      (e.f i ≫ (prevD i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) h.hom) +
    e.f i ≫ g.f i
Tactic: rw [comp_f, h.comm i, dNext_comp_left, prevD_comp_left, comp_f,
    Preadditive.comp_add, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (hypothesis)
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
⊢ 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)
have 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)
Tactic: have eq1 : prevD i hom ≫ D.d i j = 0 := by
      simp only [prevD, AddMonoidHom.mk'_apply, assoc, d_comp_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (hypothesis)
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)
⊢ 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)
have 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
Tactic: have eq2 : C.d i j ≫ dNext j hom = 0 := by
      simp only [dNext, AddMonoidHom.mk'_apply, d_comp_d_assoc, zero_comp]