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 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
⊢ 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 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)
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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)
⊢ 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 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)
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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)
⊢ 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 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
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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
⊢ 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 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
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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
⊢ 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 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
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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
⊢ 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 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
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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
⊢ 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 rw₆ : (C.d i j ≫ hom j i) ≫ D.d i j = 0 + C.d i j ≫ hom j i ≫ D.d i j
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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
⊢ 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 rw₇ : (C.d i j ≫ hom j i) ≫ D.d i j = C.d i j ≫ hom j i ≫ D.d i j
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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 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
⊢ 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 rw₈ : C.d i j ≫ hom j i ≫ D.d i j = C.d i j ≫ hom j i ≫ D.d i j
Tactic: rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2,
      add_zero, zero_add, assoc]
-- 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
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
⊢ nullHomotopicMap hom ≫ g = nullHomotopicMap fun (i j : ι) ↦ hom i j ≫ g.f j
have h : ∀ (n : ι), (nullHomotopicMap hom ≫ g).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ hom i j ≫ g.f j) n
Tactic: ext n
-- 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
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
n : ι
⊢ (nullHomotopicMap hom ≫ g).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ hom i j ≫ g.f j) n
have h : (C.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ D.dTo n) ≫ g.f n =
  C.dFrom n ≫ hom (c.next n) n ≫ g.f n + (hom n (c.prev n) ≫ g.f (c.prev n)) ≫ E.dTo n
Tactic: dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
-- 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
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
⊢ nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j
have rw : Eq (α := C ⟶ E) (nullHomotopicMap fun (i j : ι) ↦ (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) ≫ g.f j)
  (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j)
Tactic: rw [nullHomotopicMap', nullHomotopicMap_comp]