awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.BifunctorShift
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
d p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = d
⊢ Eq (α :=
    (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁).X p)).obj (K₂.X q) ⟶
      X (mapBifunctor K₁ L₂ F (ComplexShape.up ℤ)) (d + n))
    (CategoryStruct.comp (Y :=
      X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) K₂ F (ComplexShape.up ℤ)) d)
      (ιMapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) K₂ F (ComplexShape.up ℤ) p q d h)
      (CategoryStruct.comp (Y := X (mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)) (d + n))
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) n)) K₁) d)
        (Hom.f (mapBifunctorMap (𝟙 K₁) g F (ComplexShape.up ℤ)) (d + n))))
    (CategoryStruct.comp (Y :=
      X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) K₂ F (ComplexShape.up ℤ)) d)
      (ιMapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) K₂ F (ComplexShape.up ℤ) p q d h)
      (CategoryStruct.comp (Y :=
        X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) L₂ F (ComplexShape.up ℤ)) d)
        (Hom.f
          (mapBifunctorMap (𝟙 (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁)) g F (ComplexShape.up ℤ)) d)
        (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) L₂) n)) K₁) d)))

Tactic:
simp [commShiftIso_map₂CochainComplex_flip_hom_app,
      CochainComplex.ι_mapBifunctorShift₁Iso_hom_f _ _ _ _ _ _ _ _ (p + n) (d + n) rfl rfl,
      CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc _ _ _ _ _ _ _ _ (p + n) (d + n) rfl rfl]

Premises used: CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app, HAdd.hAdd, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, rfl, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x x_1 : ℤ
⊢ Eq (α := ℤ) ((fun (n : ℤ) ↦ -n) x) ((fun (n : ℤ) ↦ -n) x_1) → x = x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ ∀ {i₁ i₂ : ℤ} (h : (up ℤ).Rel i₁ i₂), (down ℤ).Rel (-i₁) (-i₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ ∀ (i₁ i₂ : ℤ) (h : -i₂ + 1 = -i₁), i₁ + 1 = i₂

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ ∀ {i₁ i₂ : ℤ} (h : i₂ + 1 = i₁), -i₁ + 1 = -i₂

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ ∀ (i₁ i₂ : ℤ) (h : -i₁ + 1 = -i₂), i₂ + 1 = i₁

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ n = ComplexShape.embeddingUpIntDownInt.f (ComplexShape.embeddingDownIntUpInt.f n)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ ComplexShape.embeddingDownIntUpInt.f (ComplexShape.embeddingUpIntDownInt.f n) = n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q : ℤ
hpq : ¬(ComplexShape.up ℤ).Rel q p
a : ¬(ComplexShape.up ℤ).Rel (-p) (-q)
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X p ⟶
      (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X q)
    (Quiver.Hom.op (h.hom (-q) (-p))) 0

Tactic:
rw [h.zero, op_zero]

Premises used: Homotopy.zero, CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q : ℤ
hpq : ¬q + 1 = p
⊢ ¬-p + 1 = -q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (-(n + 1)) (-n)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
e_a :
  Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := L.X (-(n + 1))) (h.hom (-n) (-(n + 1))) (L.d (-(n + 1)) (-n))))
    (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op ((prevD (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) h.hom) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))

Tactic:
rw [prevD_eq _ (j' := - (n + 1)) (by simp)]

Premises used: prevD_eq
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
e_a :
  Eq.{v_1 + 1} (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := L.X (-(n + 1))) (h.hom (-n) (-(n + 1))) (L.d (-(n + 1)) (-n))) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := L.X (-(n + 1))) (h.hom (-n) (-(n + 1))) (L.d (-(n + 1)) (-n))))
    (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))

Tactic:
symm
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (ComplexShape.up ℤ).Rel n (n + 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ Eq.{v_1 + 1} (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := L.X (-(n + 1))) (h.hom (-n) (-(n + 1))) (L.d (-(n + 1)) (-n))) :
      op (L.X (-n)) ⟶ op (K.X (-n)))

Tactic:
exact dNext_eq _ (i' := n + 1) (by simp)

Premises used: dNext_eq
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ -n + 1 = -(n - 1)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
e_a :
  Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1))) (h.hom (-(n - 1)) (-n))))
    (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op ((dNext (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) h.hom) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))

Tactic:
rw [dNext_eq _ (i' := - (n - 1)) (by dsimp; lia)]

Premises used: dNext_eq
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
e_a :
  Eq.{v_1 + 1} (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1))) (h.hom (-(n - 1)) (-n))) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1))) (h.hom (-(n - 1)) (-n))))
    (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
            (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
            (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
          ((i j : ℤ) →
              ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
            (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
        (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
      fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))

Tactic:
symm
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ Eq.{v_1 + 1} (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (((prevD.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op (CategoryStruct.comp (Y := K.X (-(n - 1))) (K.d (-n) (-(n - 1))) (h.hom (-(n - 1)) (-n))) :
      op (L.X (-n)) ⟶ op (K.X (-n)))

Tactic:
exact prevD_eq _ (j' := n - 1) (by simp)

Premises used: prevD_eq
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q p' q' : ℤ
hp : autoParam (p + p' = 0) homotopyOp_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyOp_hom_eq._auto_2
⊢ p' = -p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q p' q' : ℤ
hp : autoParam (p + p' = 0) homotopyOp_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyOp_hom_eq._auto_2
⊢ -q = q'

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q p' q' : ℤ
hp : p + p' = 0
hq : q + q' = 0
⊢ p' = -p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q p' q' : ℤ
hp : p + p' = 0
hq : q + q' = 0
obtain :
  ∀ (hp : p + -p = 0),
    (homotopyOp h).hom p q =
      (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫
        Quiver.Hom.op (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ (h.hom q' p').op ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op

Tactic:
obtain rfl : p' = -p := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
⊢ q' = -q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
obtain :
  ∀ (hq : q + -q = 0),
    (homotopyOp h).hom p q =
      (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫
        Quiver.Hom.op (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ Quiver.Hom.op (h.hom q' (-p)) ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op

Tactic:
obtain rfl : q' = -q := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q : ℤ
hp : p + -p = 0
hq : q + -q = 0
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫
      Quiver.Hom.op (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op

Tactic:
simp [homotopyOp]

Premises used: CochainComplex.homotopyOp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
p q : ℤ
⊢ p = ComplexShape.embeddingUpIntDownInt.f (-p)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
p q : ℤ
⊢ ComplexShape.embeddingUpIntDownInt.f (-q) = q

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
p q : ℤ
hpq : ¬(ComplexShape.up ℤ).Rel q p
a : ¬(ComplexShape.up ℤ).Rel (-p) (-q)
⊢ (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ Quiver.Hom.unop (h.hom (-q) (-p)) ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom = 0

Tactic:
rw [h.zero, unop_zero, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, Homotopy.zero, CategoryTheory.Limits.unop_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
p q : ℤ
hpq : ¬q + 1 = p
⊢ ¬-p + 1 = -q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.CochainComplexOpposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h :
  Homotopy.{v_1, u_1, 0} (ι := ℤ) (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L)) (D :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) f.op)
    (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) g.op)
n p q p' q' : ℤ
hp : p = p'
hq : q = q'
⊢ ComplexShape.embeddingUpIntDownInt.f p' = ComplexShape.embeddingUpIntDownInt.f p

Tactic:
simpa using hp.symm

Premises used: Eq.symm