awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
hij : ¬c.Rel i j
neg :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
neg₁ :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op 0) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
neg₂ :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) 0 (Iso.inv (K.cyclesOpIso i)) : op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
neg₃ neg₄ : Eq.{v_1 + 1} (α := op (K.X j) ⟶ K.op.cycles i) 0 0
⊢ Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (K.op.toCycles j i : K.op.X j ⟶ K.op.cycles i)

Tactic:
rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]

Premises used: HomologicalComplex.op, HomologicalComplex.fromOpcycles_eq_zero, HomologicalComplex.toCycles_eq_zero, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := (Functor.obj (opFunctor V c) (op L)).homology i ⟶ op (K.homology i))
    (homologyMap (CategoryTheory.Functor.map (opFunctor V c) φ.op) i ≫ Iso.hom (K.homologyOp i))
    (CategoryStruct.comp (Y := op (L.homology i)) (Iso.hom (L.homologyOp i)) (Quiver.Hom.op (homologyMap φ i)))

Tactic:
ShortComplex.homologyOpIso_hom_naturality ((shortComplexFunctor V c i).map φ)

Premises used: CategoryTheory.ShortComplex.homologyOpIso_hom_naturality, Quiver.Hom.op, ComplexShape.prev, HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.opMap, ComplexShape.next, HomologicalComplex.homologyMap, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := (Functor.obj (opFunctor V c) (op L)).opcycles i ⟶ op (K.cycles i))
    (opcyclesMap (CategoryTheory.Functor.map (opFunctor V c) φ.op) i ≫ Iso.hom (K.opcyclesOpIso i))
    (CategoryStruct.comp (Y := op (L.cycles i)) (Iso.hom (L.opcyclesOpIso i)) (Quiver.Hom.op (cyclesMap φ i)))

Tactic:
ShortComplex.opcyclesOpIso_hom_naturality ((shortComplexFunctor V c i).map φ)

Premises used: Quiver.Hom.op, HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, CategoryTheory.ShortComplex.opcyclesOpIso_hom_naturality, ComplexShape.prev, HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.opMap, HomologicalComplex.cyclesMap, ComplexShape.next, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := op (L.cycles i) ⟶ K.op.opcycles i)
    (CategoryStruct.comp (Y := op (K.cycles i)) (Quiver.Hom.op (cyclesMap φ i)) (Iso.inv (K.opcyclesOpIso i)) :
      op (L.cycles i) ⟶ K.op.opcycles i)
    (Iso.inv (L.opcyclesOpIso i) ≫ opcyclesMap (CategoryTheory.Functor.map (opFunctor V c) φ.op) i :
      op (L.cycles i) ⟶ (Functor.obj (opFunctor V c) (op K)).opcycles i)

Tactic:
ShortComplex.opcyclesOpIso_inv_naturality ((shortComplexFunctor V c i).map φ)

Premises used: Quiver.Hom.op, HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, ComplexShape.prev, HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.opcyclesOpIso_inv_naturality, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.opMap, HomologicalComplex.cyclesMap, ComplexShape.next, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := (Functor.obj (opFunctor V c) (op L)).cycles i ⟶ op (K.opcycles i))
    (cyclesMap (CategoryTheory.Functor.map (opFunctor V c) φ.op) i ≫ Iso.hom (K.cyclesOpIso i))
    (CategoryStruct.comp (Y := op (L.opcycles i)) (Iso.hom (L.cyclesOpIso i)) (Quiver.Hom.op (opcyclesMap φ i)))

Tactic:
ShortComplex.cyclesOpIso_hom_naturality ((shortComplexFunctor V c i).map φ)

Premises used: Quiver.Hom.op, CategoryTheory.ShortComplex.cyclesOpIso_hom_naturality, HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, ComplexShape.prev, HomologicalComplex.shortComplexFunctor, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.opMap, HomologicalComplex.cyclesMap, ComplexShape.next, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K L : HomologicalComplex.{v_1, u_2, u_1} V c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := op (L.opcycles i) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (opcyclesMap φ i)) (Iso.inv (K.cyclesOpIso i)) :
      op (L.opcycles i) ⟶ K.op.cycles i)
    (Iso.inv (L.cyclesOpIso i) ≫ cyclesMap (CategoryTheory.Functor.map (opFunctor V c) φ.op) i :
      op (L.opcycles i) ⟶ (Functor.obj (opFunctor V c) (op K)).cycles i)

Tactic:
ShortComplex.cyclesOpIso_inv_naturality ((shortComplexFunctor V c i).map φ)

Premises used: Quiver.Hom.op, HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, ComplexShape.prev, HomologicalComplex.shortComplexFunctor, CategoryTheory.ShortComplex.cyclesOpIso_inv_naturality, CategoryTheory.Functor.map, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.opMap, HomologicalComplex.cyclesMap, ComplexShape.next, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
dsimp :
  φ₁.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop
⊢ Quiver.Hom.unop (Hom.f (CategoryTheory.Functor.map (opFunctor V c) φ₁.op) n) =
    (HAdd.hAdd (α :=
          (Functor.obj (opFunctor V c) (Opposite.op G)).X n ⟶ (Functor.obj (opFunctor V c) (Opposite.op F)).X n)
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := Functor.obj (opFunctor V c) (Opposite.op G)) (D :=
                  Functor.obj (opFunctor V c) (Opposite.op F)) n :
                ((i j : ι) →
                    (Functor.obj (opFunctor V c) (Opposite.op G)).X i ⟶
                      (Functor.obj (opFunctor V c) (Opposite.op F)).X j) →+
                  ((Functor.obj (opFunctor V c) (Opposite.op G)).X n ⟶
                    (Functor.obj (opFunctor V c) (Opposite.op F)).X n)) :
              (a : (i j : ι) → ((opFunctor V c).obj (Opposite.op G)).X i ⟶ ((opFunctor V c).obj (Opposite.op F)).X j) →
                ((opFunctor V c).obj (Opposite.op G)).X n ⟶ ((opFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := Functor.obj (opFunctor V c) (Opposite.op G)) (D :=
                  Functor.obj (opFunctor V c) (Opposite.op F)) n :
                ((i j : ι) →
                    (Functor.obj (opFunctor V c) (Opposite.op G)).X i ⟶
                      (Functor.obj (opFunctor V c) (Opposite.op F)).X j) →+
                  ((Functor.obj (opFunctor V c) (Opposite.op G)).X n ⟶
                    (Functor.obj (opFunctor V c) (Opposite.op F)).X n)) :
              (a : (i j : ι) → ((opFunctor V c).obj (Opposite.op G)).X i ⟶ ((opFunctor V c).obj (Opposite.op F)).X j) →
                ((opFunctor V c).obj (Opposite.op G)).X n ⟶ ((opFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).op) +
        Hom.f (CategoryTheory.Functor.map (opFunctor V c) φ₂.op) n).unop

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
rw :
  HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        ((dNext n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n)
        ((prevD n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop
⊢ φ₁.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop

Tactic:
rw [h.comm n]

Premises used: Homotopy.comm
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
nth_rw :
  HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        ((prevD n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n)
        ((dNext n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop
⊢ HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        ((dNext n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n)
        ((prevD n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop

Tactic:
nth_rw 2 [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        ((prevD n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n)
        ((dNext n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy.{v_1, u_1, u_2} (ι := ι) (V := Vᵒᵖ) (c := c) (C := F) (D := G) φ₁ φ₂
n : ι
dsimp :
  φ₁.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op
⊢ Quiver.Hom.op (Hom.f (CategoryTheory.Functor.map (unopFunctor V c) φ₁.op) n) =
    (HAdd.hAdd (α :=
          (Functor.obj (unopFunctor V c) (Opposite.op G)).X n ⟶ (Functor.obj (unopFunctor V c) (Opposite.op F)).X n)
          ((dNext n :
              (a :
                  (i j : ι) →
                    ((unopFunctor V c).obj (Opposite.op G)).X i ⟶ ((unopFunctor V c).obj (Opposite.op F)).X j) →
                ((unopFunctor V c).obj (Opposite.op G)).X n ⟶ ((unopFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).unop)
          ((prevD n :
              (a :
                  (i j : ι) →
                    ((unopFunctor V c).obj (Opposite.op G)).X i ⟶ ((unopFunctor V c).obj (Opposite.op F)).X j) →
                ((unopFunctor V c).obj (Opposite.op G)).X n ⟶ ((unopFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).unop) +
        Hom.f (CategoryTheory.Functor.map (unopFunctor V c) φ₂.op) n).op

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy.{v_1, u_1, u_2} (ι := ι) (V := Vᵒᵖ) (c := c) (C := F) (D := G) φ₁ φ₂
n : ι
rw :
  HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op
⊢ φ₁.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op

Tactic:
rw [h.comm n]

Premises used: Homotopy.comm
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy.{v_1, u_1, u_2} (ι := ι) (V := Vᵒᵖ) (c := c) (C := F) (D := G) φ₁ φ₂
n : ι
nth_rw :
  HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n)
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op
⊢ HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op

Tactic:
nth_rw 2 [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Homology.Opposite
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy.{v_1, u_1, u_2} (ι := ι) (V := Vᵒᵖ) (c := c) (C := F) (D := G) φ₁ φ₂
n : ι
⊢ HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n)
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op

Tactic:
rfl