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
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₂
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₃

Tactic:
⟨_, ?_,
      ⟨Triangle.π₃.mapIso (isoTriangleOfIso₁₂ T _ hT (mappingCone_triangleh_distinguished f)
        (Iso.refl _) (Iso.refl _) ?_)⟩⟩

Premises used: CategoryTheory.Pretriangulated.Triangle.π₃, CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂, HomotopyCategory.mappingCone_triangleh_distinguished, CategoryTheory.Iso.refl, Nonempty.intro, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.Functor.mapIso
-- 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₂
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₁
refine_1 : plus C (Functor.obj Triangle.π₃ (CochainComplex.mappingCone.triangleh f))
refine_2 :
  T.mor₁ ≫ Iso.hom (Iso.refl T.obj₂) = Iso.hom (Iso.refl T.obj₁) ≫ (CochainComplex.mappingCone.triangleh f).mor₁
⊢ ObjectProperty.isoClosure (plus C) T.obj₃

Tactic:
refine ⟨_, ?_,
      ⟨Triangle.π₃.mapIso (isoTriangleOfIso₁₂ T _ hT (mappingCone_triangleh_distinguished f)
        (Iso.refl _) (Iso.refl _) ?_)⟩⟩
-- 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₂
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₁
refine_1 : CochainComplex.plus C (CochainComplex.mappingCone f)
⊢ plus C (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone f))

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
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₂
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₁
⊢ min (n₁ - 1) n₂ < n₁

Tactic:
simp
-- 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₂
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₁
⊢ min (n₁ - 1) n₂ ≤ n₂

Tactic:
simp
-- 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₂
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₁
⊢ CochainComplex.plus C (CochainComplex.mappingCone f)

Tactic:
exact ⟨min (n₁ - 1) n₂, CochainComplex.isStrictlyGE_mappingCone f n₁ n₂ _
        (by simp) (by simp)⟩
-- 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₂
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₁
⊢ T.mor₁ ≫ Iso.hom (Iso.refl T.obj₂) = Iso.hom (Iso.refl T.obj₁) ≫ (CochainComplex.mappingCone.triangleh f).mor₁

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
A : Type u_2
inst : Category.{v_2, u_2} A
inst_1 : Abelian.{v_2, u_2} A
K L : Plus.{v_2, u_2} A
f : K ⟶ L
⊢ quasiIso A f ↔ HomotopyCategory.quasiIso A (ComplexShape.up ℤ) f.hom

Tactic:
Iff.rfl

Premises used: CategoryTheory.MorphismProperty.inverseImage, Iff.rfl, HomotopyCategory.quasiIso, HomotopyCategory.Plus.quasiIso
-- 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
a : ℤ
h :
  ∀ ⦃X Y : Plus.{v_2, u_2} A⦄ (f : X ⟶ Y),
    MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔ quasiIso A f
⊢ Eq (α := MorphismProperty (Plus.{v_2, u_2} A))
    (MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a)) (quasiIso A)

Tactic:
ext X Y f
-- 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
a : ℤ
X Y : Plus.{v_2, u_2} A
f : X ⟶ Y
h :
  MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔
    HomotopyCategory.quasiIso A (ComplexShape.up ℤ) (X :=
      Functor.obj (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) (X.obj (P := plus A)))
      (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) f.hom)
⊢ MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔ quasiIso A f

Tactic:
simp only [quasiIso_iff, ← MorphismProperty.IsCompatibleWithShift.iff
      (HomotopyCategory.quasiIso _ _) f.hom a]

Premises used: HomotopyCategory.quasiIso, CategoryTheory.InducedCategory.Hom.hom, HomotopyCategory.Plus.quasiIso_iff, CategoryTheory.MorphismProperty.IsCompatibleWithShift.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
a : ℤ
X Y : Plus.{v_2, u_2} A
f : X ⟶ Y
⊢ MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔
    HomotopyCategory.quasiIso A (ComplexShape.up ℤ) (X :=
      Functor.obj (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) (X.obj (P := plus A)))
      (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) f.hom)

Tactic:
(HomotopyCategory.quasiIso _ _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso ((ι A).commShiftIso a) (Arrow.mk f))

Premises used: CategoryTheory.MorphismProperty.inverseImage, HomotopyCategory.quasiIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, HomotopyCategory.Plus.quasiIso, HomotopyCategory.Plus.ι, CategoryTheory.Arrow.isoOfNatIso, CategoryTheory.Arrow.mk, CategoryTheory.Functor.CommShift.commShiftIso
-- 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
a : ℤ
X Y : Plus.{v_2, u_2} A
f : X ⟶ Y
⊢ MorphismProperty.inverseImage (quasiIso A) (shiftFunctor (Plus.{v_2, u_2} A) a) f ↔
    HomotopyCategory.quasiIso A (ComplexShape.up ℤ) (X :=
      Functor.obj (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) (X.obj (P := plus A)))
      (CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_2, u_2, 0} A (ComplexShape.up ℤ)) a) f.hom)

Tactic:
exact (HomotopyCategory.quasiIso _ _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso ((ι A).commShiftIso a) (Arrow.mk f))

Premises used: HomotopyCategory.quasiIso, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, HomotopyCategory.Plus.ι, CategoryTheory.Arrow.isoOfNatIso, CategoryTheory.Arrow.mk, CategoryTheory.Functor.CommShift.commShiftIso
-- 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
⊢ MorphismProperty.RespectsIso (C := Plus.{v_2, u_2} A)
    (MorphismProperty.inverseImage (HomotopyCategory.quasiIso A (ComplexShape.up ℤ)) (ι A))

Tactic:
infer_instance
-- 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
K : CochainComplex.{v_1, u_1, 0} C ℤ
h : CochainComplex.plus C K
⊢ plus C
    (Functor.obj (CochainComplex.Plus.ι C ⋙ HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K h))

Tactic:
simpa [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
K : Plus.{v_1, u_1} C
obtain :
  ∀ (L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ))
    (hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)),
    ∃ (a : CochainComplex.Plus.{v_1, u_1} C), Functor.obj (quotient C) a = K
⊢ ∃ (a : CochainComplex.Plus.{v_1, u_1} C), Functor.obj (quotient C) a = K

Tactic:
obtain ⟨L, hL⟩ := HomotopyCategory.quotient_obj_surjective K.obj

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, HomotopyCategory.quotient_obj_surjective
-- 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 : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
obj :
  (Functor.obj (quotient C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)).obj (P := plus C) =
    K.obj (P := plus C)
⊢ Functor.obj (quotient C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) = K

Tactic:
ext
-- 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 : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
⊢ (Functor.obj (quotient C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)).obj (P := plus C) =
    K.obj (P := plus C)

Tactic:
hL
-- 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 : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
⊢ (Functor.obj (quotient C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)).obj (P := plus C) =
    K.obj (P := plus C)

Tactic:
exact hL
-- 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 : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
refine : CochainComplex.plus C L
⊢ ∃ (a : CochainComplex.Plus.{v_1, u_1} C), Functor.obj (quotient C) a = K

Tactic:
refine ⟨⟨L, ?_⟩, by ext; exact hL⟩
-- 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 : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
rw : plus C (K.obj (P := plus C))
⊢ CochainComplex.plus C L

Tactic:
rw [← HomotopyCategory.plus_quotient_obj_iff, hL]

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
K : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
⊢ plus C (K.obj (P := plus C))

Tactic:
K.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- 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 : Plus.{v_1, u_1} C
L : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
hL : Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L = K.obj (P := plus C)
⊢ plus C (K.obj (P := plus C))

Tactic:
exact K.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- 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
K : Plus.{v_1, u_1} C
obtain : ∀ (L : CochainComplex.Plus.{v_1, u_1} C), Functor.essImage (quotient C) (Functor.obj (quotient C) L)
⊢ Functor.essImage (quotient C) K

Tactic:
obtain ⟨L, rfl⟩ := quotient_obj_surjective K

Premises used: HomotopyCategory.Plus.quotient_obj_surjective, 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
L : CochainComplex.Plus.{v_1, u_1} C
⊢ Functor.essImage (quotient C) (Functor.obj (quotient C) L)

Tactic:
⟨L, ⟨Iso.refl _⟩⟩

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.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
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
L : CochainComplex.Plus.{v_1, u_1} C
⊢ Functor.essImage (quotient C) (Functor.obj (quotient C) L)

Tactic:
exact ⟨L, ⟨Iso.refl _⟩⟩
-- 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
⊢ Functor.Full (C := CochainComplex.Plus.{v_1, u_1} C)
    (ObjectProperty.lift (plus C) (CochainComplex.Plus.ι C ⋙ HomotopyCategory.quotient C (ComplexShape.up ℤ)) ⋯)

Tactic:
infer_instance
-- 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
x x_1 : CochainComplex.Plus.{v_1, u_1} C
f : x ⟶ x_1
hf : MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) f
⊢ IsIso (X := Functor.obj (quotient C) x) (CategoryTheory.Functor.map (quotient C) f)

Tactic:
simpa [← isIso_iff_of_reflects_iso _ (HomotopyCategory.Plus.ι C),
        ← inverseImage_quotient_isomorphisms] using hf

Premises used: CategoryTheory.isIso_iff_of_reflects_iso, HomotopyCategory.Plus.ι, HomotopyCategory.inverseImage_quotient_isomorphisms
-- 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
K L : CochainComplex.Plus.{v_1, u_1} C
f₀ f₁ : K ⟶ L
hf :
  Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L) (CategoryTheory.Functor.map (quotient C) f₀)
    (CategoryTheory.Functor.map (quotient C) f₁)
obtain :
  ∀ (f₀ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C))
    (hf :
      Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
        (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
        (CategoryTheory.Functor.map (quotient C) f₁)),
    ∃ (P : Precylinder K) (x : P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀) f₁),
      MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
⊢ ∃ (P : Precylinder K) (x : P.LeftHomotopy f₀ f₁),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π

Tactic:
obtain ⟨f₀, rfl⟩ := ObjectProperty.homMk_surjective f₀

Premises used: CategoryTheory.ObjectProperty.homMk_surjective, 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
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.Plus.{v_1, u_1} C
f₁ : K ⟶ L
f₀ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C)
hf :
  Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
    (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
    (CategoryTheory.Functor.map (quotient C) f₁)
obtain :
  ∀ (f₁ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C))
    (hf :
      Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
        (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
        (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₁))),
    ∃ (P : Precylinder K) (x :
      P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀)
        (ObjectProperty.homMk (P := CochainComplex.plus C) f₁)),
      MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
⊢ ∃ (P : Precylinder K) (x : P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀) f₁),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π

Tactic:
obtain ⟨f₁, rfl⟩ := ObjectProperty.homMk_surjective f₁

Premises used: CategoryTheory.ObjectProperty.homMk_surjective, 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
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.Plus.{v_1, u_1} C
f₀ f₁ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C)
hf :
  Eq (α := Functor.obj (quotient C) K ⟶ Functor.obj (quotient C) L)
    (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₀))
    (CategoryTheory.Functor.map (quotient C) (ObjectProperty.homMk (P := CochainComplex.plus C) f₁))
replace :
  ∀ (hf : Homotopy f₀ f₁),
    ∃ (P : Precylinder K) (x :
      P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀)
        (ObjectProperty.homMk (P := CochainComplex.plus C) f₁)),
      MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π
⊢ ∃ (P : Precylinder K) (x :
    P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀)
      (ObjectProperty.homMk (P := CochainComplex.plus C) f₁)),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π

Tactic:
replace hf := homotopyOfEq f₀ f₁ ((HomotopyCategory.Plus.ι _).congr_map hf)
-- 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
K L : CochainComplex.Plus.{v_1, u_1} C
f₀ f₁ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C)
hf : Homotopy f₀ f₁
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
simp