awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK :
  ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
refine_2 :
  Eq.{max 1 (v_1 + 1)} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    0 (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
refine_2₁ refine_2₂ :
  Eq.{max 1 (v_1 + 1)} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    0 0
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)

Tactic:
rw [hK ((HomotopyCategory.quotient _ _).map f) hL, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map, HomotopyCategory.quotient
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 rwa rwa₁ rwa₂ rwa₃ : K.IsKProjective
⊢ ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)

Tactic:
rwa [← isKProjective_iff_leftOrthogonal]

Premises used: CochainComplex.isKProjective_iff_leftOrthogonal
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : K.IsKProjective
n : ℤ
rw :
  ∀
    (hK :
      ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
    (n : ℤ),
    ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K))
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).IsKProjective

Tactic:
rw [isKProjective_iff_leftOrthogonal] at hK ⊢

Premises used: CochainComplex.isKProjective_iff_leftOrthogonal
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK :
  ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
n : ℤ
⊢ ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K))

Tactic:
ObjectProperty.prop_of_iso _
    (((HomotopyCategory.quotient C (.up ℤ)).commShiftIso n).symm.app K)
    ((HomotopyCategory.subcategoryAcyclic C).leftOrthogonal.le_shift n _ hK)

Premises used: CategoryTheory.ObjectProperty.prop_of_iso, Int, CategoryTheory.Iso.symm, HomotopyCategory.subcategoryAcyclic, HomotopyCategory.quotient, CategoryTheory.Iso.app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.ObjectProperty.leftOrthogonal, ComplexShape.up, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK :
  ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
n : ℤ
⊢ ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K))

Tactic:
exact ObjectProperty.prop_of_iso _
    (((HomotopyCategory.quotient C (.up ℤ)).commShiftIso n).symm.app K)
    ((HomotopyCategory.subcategoryAcyclic C).leftOrthogonal.le_shift n _ hK)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).IsKProjective ↔ K.IsKProjective

Tactic:
⟨fun _ ↦ isKProjective_of_iso (show K⟦n⟧⟦-n⟧ ≅ K from (shiftEquiv _ n).unitIso.symm.app K),
    fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Equivalence.unitIso, inferInstance, Int, CategoryTheory.shiftEquiv, CochainComplex, Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CochainComplex.isKProjective_of_iso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : IsKInjective.{v_1, u_1} (C := Cᵒᵖ) (Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ Eq.{max 1 (v_1 + 1)} (α :=
    Functor.obj (Equivalence.functor (opEquivalence C)) (op L) ⟶
      Functor.obj (Equivalence.functor (opEquivalence C)) (op K))
    0 (CategoryTheory.Functor.map (Equivalence.functor (opEquivalence C)) (Quiver.Hom.op 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
n : ℤ
dsimp : Injective.{v_1, u_1} (op (K.X (-n)))
⊢ Injective.{v_1, u_1} (L.X n)

Tactic:
dsimp [L]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
n : ℤ
⊢ Injective.{v_1, u_1} (op (K.X (-n)))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
⊢ ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)

Tactic:
have (n : ℤ) : Injective (L.X n) := by
    dsimp [L]
    infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
rw : ∀ (i : ℤ), autoParam (i < -d) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (L.X i)
⊢ L.IsStrictlyGE (-d)

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
i : ℤ
hi : autoParam (i < -d) isStrictlyGE_iff._auto_1
⊢ d < -i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
i : ℤ
hi : autoParam (i < -d) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (L.X i)

Tactic:
exact (K.isZero_of_isStrictlyLE d _ (by dsimp; lia)).op

Premises used: CategoryTheory.Limits.IsZero.op, CochainComplex.isZero_of_isStrictlyLE
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
⊢ L.IsStrictlyGE (-d)

Tactic:
have : L.IsStrictlyGE (-d) := by
    rw [isStrictlyGE_iff]
    intro i hi
    exact (K.isZero_of_isStrictlyLE d _ (by dsimp; lia)).op
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this_1 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
this : L.IsStrictlyGE (-d)
⊢ K.IsKProjective

Tactic:
isKProjective_of_op (isKInjective_of_injective L (-d))

Premises used: CochainComplex.isKInjective_of_injective, CochainComplex.isKProjective_of_op, Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this_1 : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
this : L.IsStrictlyGE (-d)
⊢ K.IsKProjective

Tactic:
exact isKProjective_of_op (isKInjective_of_injective L (-d))

Premises used: CochainComplex.isKInjective_of_injective, CochainComplex.isKProjective_of_op, Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : ∀ (n : ℕ), Projective.{v_1, u_1} (K.X n)
⊢ IsKProjective (HomologicalComplex.extend K ComplexShape.embeddingDownNat)

Tactic:
CochainComplex.isKProjective_of_projective _ 0

Premises used: CochainComplex.isKProjective_of_projective, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
⊢ HAdd.hAdd (α := ℤ) 1 (-1) = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p : ℤ
⊢ p + -1 = p + -1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p : ℤ
⊢ p + -1 + 1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p : ℤ
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p ⋯) (Hom.f (fst φ) p) = 𝟙 (K.X p)

Tactic:
simp [inl, fst, Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia),
    Cochain.leftShift_v (n := 1) _ _ _ _ _ p _ (p + -1) (by lia)]

Premises used: CochainComplex.mappingCocone.inl, CochainComplex.mappingCocone.fst, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ q = p + -1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
obtain :
  ∀ (hpq : p + -1 = p + -1),
    CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p ⋯) (Cochain.v (snd φ) p (p + -1) hpq) = 0
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p ⋯) (Cochain.v (snd φ) p q hpq) = 0

Tactic:
obtain rfl : q = p + -1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p : ℤ
hpq : p + -1 = p + -1
⊢ p + -1 = p + -1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p : ℤ
hpq : p + -1 = p + -1
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p ⋯) (Cochain.v (snd φ) p (p + -1) hpq) = 0

Tactic:
simp [inl, snd, Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia),
    Cochain.leftShift_v _ _ _ _ _ _ hpq]

Premises used: CochainComplex.mappingCocone.snd, CochainComplex.mappingCocone.inl, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X q) (Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) p q hpq)
      (Hom.f (fst φ) q) =
    0

Tactic:
simp [inr, fst, Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero p),
    Cochain.leftShift_v _ _ _ _ _ _ _ _ hpq]

Premises used: CochainComplex.mappingCocone.inr, CochainComplex.mappingCocone.fst, CochainComplex.HomComplex.Cochain.leftShift_v, add_zero, CochainComplex.HomComplex.Cochain.rightShift_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X q) (Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) p q hpq)
      (Cochain.v (snd φ) q p ⋯) =
    𝟙 (L.X p)

Tactic:
simp [inr, snd, Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero p),
    Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero p),
    Int.negOnePow_even 2 ⟨1, rfl⟩]

Premises used: CochainComplex.mappingCocone.snd, CochainComplex.mappingCocone.inr, CochainComplex.HomComplex.Cochain.leftShift_v, Exists.intro, Int.negOnePow_even, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ q + 1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
obtain :
  ∀ (hpq : p + -1 = p + -1),
    HAdd.hAdd (α := (mappingCocone φ).X p ⟶ (mappingCocone φ).X p) (Hom.f (fst φ) p ≫ Cochain.v (inl φ) p p ⋯)
        (Cochain.v (snd φ) p (p + -1) hpq ≫ Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) (p + -1) p ⋯) =
      𝟙 ((mappingCocone φ).X p)
⊢ HAdd.hAdd (α := (mappingCocone φ).X p ⟶ (mappingCocone φ).X p) (Hom.f (fst φ) p ≫ Cochain.v (inl φ) p p ⋯)
      (Cochain.v (snd φ) p q hpq ≫ Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) q p ⋯) =
    𝟙 ((mappingCocone φ).X p)

Tactic:
obtain rfl : q = p + -1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p : ℤ
hpq : p + -1 = p + -1
⊢ p + -1 + 1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
p : ℤ
hpq : p + -1 = p + -1
⊢ HAdd.hAdd (α := (mappingCocone φ).X p ⟶ (mappingCocone φ).X p) (Hom.f (fst φ) p ≫ Cochain.v (inl φ) p p ⋯)
      (Cochain.v (snd φ) p (p + -1) hpq ≫ Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) (p + -1) p ⋯) =
    𝟙 ((mappingCocone φ).X p)

Tactic:
simp [fst, inl, snd, inr, mappingCocone,
    Cochain.leftShift_v (n := 1) _ _ _ _ _ p _ (p + -1) (by lia),
    Cochain.rightShift_v _ _ _ _ _ _ _ _ hpq,
    Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Int.negOnePow_even 2 ⟨1, rfl⟩,
    mappingCone.id_X φ (p + -1) p (by lia)]

Premises used: CochainComplex.mappingCocone.snd, CochainComplex.mappingCone.id_X, CochainComplex.mappingCocone.inr, CochainComplex.mappingCocone.inl, CochainComplex.mappingCocone, CochainComplex.mappingCocone.fst, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, Exists.intro, Int.negOnePow_even, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Neg.neg, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
⊢ n + -1 = m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + m = q
⊢ p + -1 = p + -1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + m = q
⊢ n + -1 = m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + m = q
⊢ p + -1 + n = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + m = q
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p ⋯) (Cochain.v (descCochain φ α β h) p q hpq) =
    α.v p q hpq

Tactic:
simp [inl, descCochain, mappingCocone,
    Cochain.rightShift_v (n := -1) _ _ _ _ p _ _ (p + -1) (by lia), smul_smul,
    Cochain.leftShift_v (n := n) _ (-1) m (by lia) _ _ hpq (p + -1) (by lia)]

Premises used: CochainComplex.mappingCocone.descCochain, smul_smul, CochainComplex.mappingCocone.inl, CochainComplex.mappingCocone, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Neg.neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + 1 = q
r : ℤ
hr : q + m = r
⊢ p + n = r

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + 1 = q
r : ℤ
hr : q + m = r
⊢ p = q + -1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + 1 = q
r : ℤ
hr : q + m = r
obtain :
  ∀ (hpq : q + -1 + 1 = q),
    CategoryStruct.comp (Y := (mappingCocone φ).X q)
        (Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) (q + -1) q hpq) (Cochain.v (descCochain φ α β h) q r hr) =
      β.v (q + -1) r ⋯
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X q) (Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) p q hpq)
      (Cochain.v (descCochain φ α β h) q r hr) =
    β.v p r ⋯

Tactic:
obtain rfl : p = q + -1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
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 ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
q r : ℤ
hr : q + m = r
hpq : q + -1 + 1 = q
⊢ q + -1 + n = r

Tactic:
lia