awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : G.Additive
refine_2 :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
      (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
    (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L) ≫
      inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
refine_2₁ refine_2₂ :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
      (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
    (inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ))
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
      (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
      (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (CategoryStruct.comp (Y := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) (mappingCone φ))
        (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) (inr φ))
        (Iso.hom (mapHomologicalComplexIso φ G)) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
        (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))
    (𝟙 (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L) ≫
        inr (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ) :
      Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (ComplexShape.up ℤ))
        (Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) L)
        (mappingCone (F := Functor.obj (G.mapHomologicalComplex (ComplexShape.up ℤ)) K)
          (CategoryTheory.Functor.map (G.mapHomologicalComplex (ComplexShape.up ℤ)) φ)))

Tactic:
rw [map_inr, id_comp]

Premises used: CochainComplex.mappingCone.map_inr, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
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 C)
    T₁
T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
obtain :
  ∀ (X Y : CochainComplex.{v_1, u_1, 0} C ℤ) (f : X ⟶ Y) (e' : T₁ ≅ CochainComplex.mappingCone.triangleh f),
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) T₂
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₂

Tactic:
obtain ⟨X, Y, f, ⟨e'⟩⟩ := hT₁
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
f : X ⟶ Y
e' : T₁ ≅ CochainComplex.mappingCone.triangleh f
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₂

Tactic:
⟨X, Y, f, ⟨e ≪≫ e'⟩⟩

Premises used: Set.Mem, setOf, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
X Y : CochainComplex.{v_1, u_1, 0} C ℤ
f : X ⟶ Y
e' : T₁ ≅ CochainComplex.mappingCone.triangleh f
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₂

Tactic:
exact ⟨X, Y, f, ⟨e ≪≫ e'⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
obtain :
  ∀ (X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)),
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C)
      (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (contractibleTriangle X)

Tactic:
obtain ⟨X⟩ := X
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))

Tactic:
⟨_, _, 𝟙 X, ⟨?_⟩⟩

Premises used: Set.Mem, setOf, CategoryTheory.CategoryStruct.id, Nonempty.intro, Exists.intro, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
refine :
  contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X) ≅
    CochainComplex.mappingCone.triangleh (𝟙 X)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))

Tactic:
refine ⟨_, _, 𝟙 X, ⟨?_⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
⊢ IsZero (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone (𝟙 X)))

Tactic:
have h := (isZero_quotient_obj_iff _).2 ⟨CochainComplex.mappingCone.homotopyToZeroOfId X⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
h : IsZero (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone (𝟙 X)))
⊢ Triangle.mor₁ (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)) ≫
      Iso.hom
        (Iso.refl
          (Triangle.obj₂
            (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)))) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₁
            (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)))) ≫
      (CochainComplex.mappingCone.triangleh (𝟙 X)).mor₁

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
h : IsZero (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone (𝟙 X)))
dsimp :
  Eq (α :=
    0 ⟶
      Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) X))
    (0 ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (𝟙 (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)))
    (Iso.inv h.isoZero ≫
      CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone.triangle (𝟙 X)).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) X)
⊢ Eq (α :=
    Triangle.obj₃ (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)) ⟶
      Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (CochainComplex.mappingCone.triangleh (𝟙 X)).obj₁)
    (Triangle.mor₃ (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)) ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Iso.hom
          (Iso.refl
            (Triangle.obj₁
              (contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X))))))
    (Iso.hom (Iso.symm h.isoZero) ≫ (CochainComplex.mappingCone.triangleh (𝟙 X)).mor₃)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
h : IsZero (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone (𝟙 X)))
⊢ Eq (α :=
    0 ⟶
      Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (Functor.obj (quotient C (ComplexShape.up ℤ)) X))
    (0 ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (𝟙 (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X)))
    (Iso.inv h.isoZero ≫
      CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone.triangle (𝟙 X)).mor₃ ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1)) X)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
inst_3 : HasZeroObject.{v_1, u_1} C
X : HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.up ℤ)
h : IsZero (Functor.obj (quotient C (ComplexShape.up ℤ)) (CochainComplex.mappingCone (𝟙 X)))
⊢ contractibleTriangle (CategoryTheory.Quotient.mk (r := homotopic C (ComplexShape.up ℤ)) X) ≅
    CochainComplex.mappingCone.triangleh (𝟙 X)

Tactic:
exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) h.isoZero.symm
    (by simp) (h.eq_of_tgt _ _) (by dsimp; ext)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
X Y : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
obtain :
  ∀ (f : X.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ Y.as (r := homotopic C (ComplexShape.up ℤ))),
    ∃ (Z : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (g : Y ⟶ Z) (h :
      Z ⟶ Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) X),
      Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
        (distinguishedTriangles C) (Triangle.mk (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f) g h)
⊢ ∃ (Z : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (g : Y ⟶ Z) (h :
    Z ⟶ Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) (Triangle.mk f g h)

Tactic:
obtain ⟨f, rfl⟩ := (quotient _ _).map_surjective f

Premises used: HomotopyCategory.quotient, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
X Y : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
f : X.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ Y.as (r := homotopic C (ComplexShape.up ℤ))
⊢ ∃ (Z : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (g : Y ⟶ Z) (h :
    Z ⟶ Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) (Triangle.mk (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f) g h)

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

Premises used: CategoryTheory.Iso.refl, Nonempty.intro, Exists.intro
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
X Y : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)
f : X.as (r := homotopic C (ComplexShape.up ℤ)) ⟶ Y.as (r := homotopic C (ComplexShape.up ℤ))
⊢ ∃ (Z : HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (g : Y ⟶ Z) (h :
    Z ⟶ Functor.obj (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) (Triangle.mk (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) f) g h)

Tactic:
exact ⟨_, _, _, ⟨_, _, f, ⟨Iso.refl _⟩⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
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 C)
    T
obtain :
  ∀ (K L : CochainComplex.{v_1, u_1, 0} C ℤ) (φ : K ⟶ L) (e : T ≅ CochainComplex.mappingCone.triangleh φ),
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) T.rotate
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T.rotate

Tactic:
obtain ⟨K, L, φ, ⟨e⟩⟩ := hT
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T.rotate

Tactic:
⟨_, _, _, ⟨(rotate _).mapIso e ≪≫ CochainComplex.mappingCone.rotateTrianglehIso φ⟩⟩

Premises used: Set.Mem, setOf, CochainComplex.mappingCone.rotateTrianglehIso, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Pretriangulated.rotate, CategoryTheory.Functor.mapIso, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T.rotate

Tactic:
exact ⟨_, _, _, ⟨(rotate _).mapIso e ≪≫ CochainComplex.mappingCone.rotateTrianglehIso φ⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
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 C)
    T
n : ℤ
obtain :
  ∀ (K L : CochainComplex.{v_1, u_1, 0} C ℤ) (φ : K ⟶ L) (e : T ≅ CochainComplex.mappingCone.triangleh φ),
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C)
      (Functor.obj (Triangle.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) n) T)
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (Functor.obj (Triangle.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) n) T)

Tactic:
obtain ⟨K, L, φ, ⟨e⟩⟩ := hT
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
n : ℤ
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (Functor.obj (Triangle.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) n) T)

Tactic:
⟨_, _, _, ⟨Functor.mapIso _ e ≪≫ CochainComplex.mappingCone.shiftTrianglehIso φ n⟩⟩

Premises used: Set.Mem, setOf, CochainComplex.mappingCone.shiftTrianglehIso, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Functor.mapIso, HomotopyCategory.Pretriangulated.distinguishedTriangles
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
n : ℤ
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
e : T ≅ CochainComplex.mappingCone.triangleh φ
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    (Functor.obj (Triangle.shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) n) T)

Tactic:
exact ⟨_, _, _, ⟨Functor.mapIso _ e ≪≫ CochainComplex.mappingCone.shiftTrianglehIso φ n⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
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 C)
    T
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T.invRotate

Tactic:
isomorphic_distinguished _
    (shift_distinguished_triangle _ (rotate_distinguished_triangle' _
      (rotate_distinguished_triangle' _ hT)) _) _
    ((invRotateIsoRotateRotateShiftFunctorNegOne _).app T)

Premises used: CategoryTheory.Pretriangulated.invRotateIsoRotateRotateShiftFunctorNegOne, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle', CategoryTheory.Iso.app, HomotopyCategory.Pretriangulated.isomorphic_distinguished, HomotopyCategory.Pretriangulated.shift_distinguished_triangle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
mp :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
      T →
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) T.rotate
mpr :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
      T.rotate →
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) T
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
      T ↔
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) T.rotate

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
      T →
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) T.rotate

Tactic:
rotate_distinguished_triangle' T

Premises used: HomotopyCategory.Pretriangulated.rotate_distinguished_triangle'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
T : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
      T →
    Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))))
      (distinguishedTriangles C) T.rotate

Tactic:
exact rotate_distinguished_triangle' T

Premises used: HomotopyCategory.Pretriangulated.rotate_distinguished_triangle'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
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
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 C)
    T.rotate
⊢ Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T

Tactic:
isomorphic_distinguished _ (invRotate_distinguished_triangle' T.rotate hT) _
      ((triangleRotation _).unitIso.app T)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Pretriangulated.triangleRotation, CategoryTheory.Pretriangulated.Triangle.rotate, CategoryTheory.Iso.app, HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle', HomotopyCategory.Pretriangulated.isomorphic_distinguished