awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
rw : ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((cylinder K).X i)
⊢ IsStrictlyGE (cylinder K) (n - 1)

Tactic:
rw [CochainComplex.isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
dsimp : IsZero.{v_1, u_1} (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) i)
⊢ IsZero.{v_1, u_1} ((cylinder K).X i)

Tactic:
dsimp [cylinder]

Premises used: HomologicalComplex.cylinder
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) i)

Tactic:
homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ ?_)

Premises used: HomologicalComplex.homotopyCofiber.isZero_X
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
refine_1 : IsZero.{v_1, u_1} ((K ⊞ K).X i)
refine_2 : ∀ (j : ℤ) (hj : (ComplexShape.up ℤ).Rel i j), IsZero.{v_1, u_1} (K.X j)
⊢ IsZero.{v_1, u_1} (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) i)

Tactic:
refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ ?_)

Premises used: HomologicalComplex.homotopyCofiber.isZero_X
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((K ⊞ K).X i)

Tactic:
IsZero.of_iso ?_ ((HomologicalComplex.eval C (.up ℤ) i).mapBiprod _ _)

Premises used: HomologicalComplex.eval, Int, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Functor.mapBiprod, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
refine_1 :
  IsZero.{v_1, u_1}
    (biprod.{v_1, u_1} (Functor.obj (eval C (ComplexShape.up ℤ) i) K) (Functor.obj (eval C (ComplexShape.up ℤ) i) K))
⊢ IsZero.{v_1, u_1} ((K ⊞ K).X i)

Tactic:
refine IsZero.of_iso ?_ ((HomologicalComplex.eval C (.up ℤ) i).mapBiprod _ _)

Premises used: HomologicalComplex.eval, Int, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Functor.mapBiprod, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1}
    (biprod.{v_1, u_1} (Functor.obj (eval C (ComplexShape.up ℤ) i) K) (Functor.obj (eval C (ComplexShape.up ℤ) i) K))

Tactic:
simpa using K.isZero_of_isStrictlyGE n i

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : i + 1 = j
⊢ j < n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : i + 1 = j
⊢ IsZero.{v_1, u_1} (K.X j)

Tactic:
exact K.isZero_of_isStrictlyGE n _ (by lia)

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : CochainComplex.plus C K
obtain : ∀ (n : ℤ) (hn : K.IsStrictlyGE n), CochainComplex.plus C (pathObject K)
⊢ CochainComplex.plus C (pathObject K)

Tactic:
obtain ⟨n, hn⟩ := hK
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ CochainComplex.plus C (pathObject K)

Tactic:
⟨n - 1, ?_⟩

Premises used: HSub.hSub, Exists.intro, CochainComplex.plus, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
refine : IsStrictlyGE (pathObject K) (n - 1)
⊢ CochainComplex.plus C (pathObject K)

Tactic:
refine ⟨n - 1, ?_⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
rw : ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((pathObject K).X i)
⊢ IsStrictlyGE (pathObject K) (n - 1)

Tactic:
rw [CochainComplex.isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} ((pathObject K).X i)

Tactic:
pathObject.isZero_X _ _ (K.isZero_of_isStrictlyGE n i)
    (fun j hj ↦ ?_)

Premises used: HomologicalComplex.pathObject.isZero_X, CochainComplex.isZero_of_isStrictlyGE
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
refine : ∀ (j : ℤ) (hj : (ComplexShape.up ℤ).Rel j i), IsZero.{v_1, u_1} (K.X j)
⊢ IsZero.{v_1, u_1} ((pathObject K).X i)

Tactic:
refine pathObject.isZero_X _ _ (K.isZero_of_isStrictlyGE n i)
    (fun j hj ↦ ?_)

Premises used: HomologicalComplex.pathObject.isZero_X, CochainComplex.isZero_of_isStrictlyGE
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : j + 1 = i
⊢ IsZero.{v_1, u_1} (K.X j)

Tactic:
K.isZero_of_isStrictlyGE n j

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : j + 1 = i
⊢ IsZero.{v_1, u_1} (K.X j)

Tactic:
exact K.isZero_of_isStrictlyGE n j

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
rw : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} ((mappingCone f).X i)
⊢ (mappingCone f).IsStrictlyGE n

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ i < n

Tactic:
simp at hi
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
i : ℤ
hi : i < n
simp : IsZero.{v_1, u_1} (K.X (i + 1)) ∧ IsZero.{v_1, u_1} (L.X i)
⊢ IsZero.{v_1, u_1} ((mappingCone f).X i)

Tactic:
simp only [mappingCone.isZero_X_iff]

Premises used: CochainComplex.mappingCone.isZero_X_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
i : ℤ
hi : i < n
⊢ IsZero.{v_1, u_1} (K.X (i + 1)) ∧ IsZero.{v_1, u_1} (L.X i)

Tactic:
⟨K.isZero_of_isStrictlyGE n₁ _, L.isZero_of_isStrictlyGE n₂ _⟩

Premises used: CochainComplex.isZero_of_isStrictlyGE, And.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst_3 : K.IsStrictlyGE n₁
inst_4 : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
i : ℤ
hi : i < n
⊢ IsZero.{v_1, u_1} (K.X (i + 1)) ∧ IsZero.{v_1, u_1} (L.X i)

Tactic:
exact ⟨K.isZero_of_isStrictlyGE n₁ _, L.isZero_of_isStrictlyGE n₂ _⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
⊢ plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) ↔ CochainComplex.plus C K

Tactic:
⟨?_, fun h ↦ ⟨_, h⟩⟩

Premises used: CategoryTheory.ObjectProperty.strictMap.mk, Iff.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
refine : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) → CochainComplex.plus C K
⊢ plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) ↔ CochainComplex.plus C K

Tactic:
refine ⟨?_, fun h ↦ ⟨_, h⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
simp :
  (∃ (X : CochainComplex.{v_1, u_1, 0} C ℤ),
      CochainComplex.plus C X ∧
        Functor.obj (quotient C (ComplexShape.up ℤ)) X = Functor.obj (quotient C (ComplexShape.up ℤ)) K) →
    CochainComplex.plus C K
⊢ plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) → CochainComplex.plus C K

Tactic:
simp only [plus, ObjectProperty.strictMap_iff]

Premises used: CategoryTheory.ObjectProperty.strictMap_iff, HomotopyCategory.plus
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
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 ℤ
h : CochainComplex.plus C L
hL : Functor.obj (quotient C (ComplexShape.up ℤ)) L = Functor.obj (quotient C (ComplexShape.up ℤ)) K
⊢ L = K

Tactic:
congr_arg Quotient.as hL

Premises used: congr_arg, CategoryTheory.Quotient.as
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
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 ℤ
h : CochainComplex.plus C L
hL : Functor.obj (quotient C (ComplexShape.up ℤ)) L = Functor.obj (quotient C (ComplexShape.up ℤ)) K
obtain :
  ∀ (hL : Functor.obj (quotient C (ComplexShape.up ℤ)) L = Functor.obj (quotient C (ComplexShape.up ℤ)) L),
    CochainComplex.plus C L
⊢ CochainComplex.plus C K

Tactic:
obtain rfl : L = K := congr_arg Quotient.as hL

Premises used: congr_arg, CategoryTheory.Quotient.as, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : CochainComplex.plus C L
hL : Functor.obj (quotient C (ComplexShape.up ℤ)) L = Functor.obj (quotient C (ComplexShape.up ℤ)) L
⊢ CochainComplex.plus C L

Tactic:
h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
L : CochainComplex.{v_1, u_1, 0} C ℤ
h : CochainComplex.plus C L
hL : Functor.obj (quotient C (ComplexShape.up ℤ)) L = Functor.obj (quotient C (ComplexShape.up ℤ)) L
⊢ CochainComplex.plus C L

Tactic:
exact h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
simp : CochainComplex.plus.{v_1, u_1} C 0
⊢ plus.{v_1, u_1} C (Functor.obj (quotient C (ComplexShape.up ℤ)) 0)

Tactic:
simp only [plus_quotient_obj_iff]

Premises used: HomotopyCategory.plus_quotient_obj_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
⊢ CochainComplex.plus.{v_1, u_1} C 0

Tactic:
⟨0, inferInstance⟩

Premises used: inferInstance, Exists.intro, CochainComplex.plus, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
⊢ CochainComplex.plus.{v_1, u_1} C 0

Tactic:
exact ⟨0, inferInstance⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hK : plus C K
obtain :
  ∀ (K : CochainComplex.{v_1, u_1, 0} C ℤ) (hK : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K)),
    ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
⊢ ObjectProperty.shift (plus C) n K

Tactic:
obtain ⟨K : CochainComplex _ _, rfl⟩ := K.quotient_obj_surjective

Premises used: HomotopyCategory.quotient_obj_surjective, CochainComplex, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
⊢ CochainComplex.plus C K

Tactic:
simp only [plus_quotient_obj_iff] at hK

Premises used: HomotopyCategory.plus_quotient_obj_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : CochainComplex.plus C K
obtain : ∀ (q : ℤ), K.IsStrictlyGE q → ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)
⊢ ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)

Tactic:
obtain ⟨q, _⟩ := hK
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
q : ℤ
h : K.IsStrictlyGE q
rw : CochainComplex.plus C (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) n) K)
⊢ ObjectProperty.shift (plus C) n (Functor.obj (quotient C (ComplexShape.up ℤ)) K)

Tactic:
rw [ObjectProperty.prop_shift_iff, shift_quotient_obj,
          plus_quotient_obj_iff]

Premises used: CategoryTheory.ObjectProperty.prop_shift_iff, HomotopyCategory.plus_quotient_obj_iff, HomotopyCategory.shift_quotient_obj
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
q : ℤ
h : K.IsStrictlyGE q
⊢ n + (q - n) = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
n : ℤ
K : CochainComplex.{v_1, u_1, 0} C ℤ
q : ℤ
h : K.IsStrictlyGE q
⊢ CochainComplex.plus C (Functor.obj (shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)) n) K)

Tactic:
exact ⟨q - n, K.isStrictlyGE_shift q n (q - n) (by lia)⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
rwa rwa₁ rwa₂ rwa₃ :
  plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))))
⊢ CochainComplex.plus C (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ)))

Tactic:
rwa [← plus_quotient_obj_iff]

Premises used: HomotopyCategory.plus_quotient_obj_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
obtain :
  ∀ (n₁ : ℤ),
    CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁ →
      ObjectProperty.isoClosure (plus C) T.obj₃
⊢ ObjectProperty.isoClosure (plus C) T.obj₃

Tactic:
obtain ⟨n₁, _⟩ : (CochainComplex.plus C) T.obj₁.as := by
      rwa [← plus_quotient_obj_iff]

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.Quotient.as, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
rwa rwa₁ rwa₂ rwa₃ :
  plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))))
⊢ CochainComplex.plus C (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ)))

Tactic:
rwa [← plus_quotient_obj_iff]

Premises used: HomotopyCategory.plus_quotient_obj_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
obtain :
  ∀ (n₂ : ℤ),
    CochainComplex.IsStrictlyGE (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))) n₂ →
      ObjectProperty.isoClosure (plus C) T.obj₃
⊢ ObjectProperty.isoClosure (plus C) T.obj₃

Tactic:
obtain ⟨n₂, _⟩ : (CochainComplex.plus C) T.obj₂.as := by
      rwa [← plus_quotient_obj_iff]

Premises used: CategoryTheory.Quotient.as, CategoryTheory.Pretriangulated.Triangle.obj₂, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
hT :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
    (@distinguishedTriangles _ _ ⋯ _ (instPreadditive C (ComplexShape.up ℤ)) ⋯ _) T
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h : CochainComplex.IsStrictlyGE (T.obj₁.as (r := homotopic C (ComplexShape.up ℤ))) n₁
n₂ : ℤ
h_1 : CochainComplex.IsStrictlyGE (T.obj₂.as (r := homotopic C (ComplexShape.up ℤ))) n₂
obtain :
  ∀ (f : T.obj₁.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ T.obj₂.as (r := homotopic C (ComplexShape.up ℤ)))
    (hf : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f = T.mor₁),
    ObjectProperty.isoClosure (plus C) T.obj₃
⊢ ObjectProperty.isoClosure (plus C) T.obj₃

Tactic:
obtain ⟨f : T.obj₁.as ⟶ T.obj₂.as, hf⟩ := (quotient _ _).map_surjective T.mor₁

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.Quotient.as, HomotopyCategory.quotient, CategoryTheory.Pretriangulated.Triangle.obj₂, CategoryTheory.Pretriangulated.Triangle.mor₁, CategoryTheory.Functor.map_surjective