awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- 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 ℤ))
hT₁ :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)))) (distinguishedTriangles C)
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
obtain :
  ∀ (K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ) (φ₁ : K₁ ⟶ L₁) (e₁ : T₁ ≅ triangleh φ₁),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
        T₁.mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              a =
          c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

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₁ 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₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
obtain :
  ∀ (K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ) (φ₂ : K₂ ⟶ L₂) (e₂ : T₂ ≅ triangleh φ₂),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
        T₁.mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              a =
          c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

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₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
⊢ ∃ (a' : Functor.obj (quotient C (ComplexShape.up ℤ)) K₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) K₂),
    a' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
obtain :
  ∀ (a' : Functor.obj (quotient C (ComplexShape.up ℤ)) K₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) K₂)
    (ha' : a' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
        T₁.mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              a =
          c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

Tactic:
obtain ⟨a', ha'⟩ : ∃ (a' : (quotient _ _).obj K₁ ⟶ (quotient _ _).obj K₂),
    a' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁ := ⟨_, rfl⟩

Premises used: HomotopyCategory.quotient, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a' : Functor.obj (quotient C (ComplexShape.up ℤ)) K₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) K₂
ha' : a' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
⊢ ∃ (b' : Functor.obj (quotient C (ComplexShape.up ℤ)) L₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) L₂),
    b' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a' : Functor.obj (quotient C (ComplexShape.up ℤ)) K₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) K₂
ha' : a' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
obtain :
  ∀ (b' : Functor.obj (quotient C (ComplexShape.up ℤ)) L₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) L₂)
    (hb' : b' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
        T₁.mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              a =
          c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

Tactic:
obtain ⟨b', hb'⟩ : ∃ (b' : (quotient _ _).obj L₁ ⟶ (quotient _ _).obj L₂),
    b' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂ := ⟨_, rfl⟩

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, HomotopyCategory.quotient, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a' : Functor.obj (quotient C (ComplexShape.up ℤ)) K₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) K₂
ha' : a' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b' : Functor.obj (quotient C (ComplexShape.up ℤ)) L₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) L₂
hb' : b' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
obtain :
  ∀ (a'' : K₁ ⟶ K₂)
    (ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
        T₁.mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              a =
          c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

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

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
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
b' : Functor.obj (quotient C (ComplexShape.up ℤ)) L₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) L₂
hb' : b' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
obtain :
  ∀ (b'' : L₁ ⟶ L₂)
    (hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
        T₁.mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              a =
          c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

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

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
T₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
⊢ (triangleh φ₁).mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁

Tactic:
have comm₁₁ := e₁.inv.comm₁
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
comm₁₁ : (triangleh φ₁).mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
⊢ T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ (triangleh φ₂).mor₁

Tactic:
have comm₁₂ := e₂.hom.comm₁
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
comm₁₁ : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) φ₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁₂ : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) φ₂
⊢ Eq (α := Functor.obj (quotient C (ComplexShape.up ℤ)) K₁ ⟶ Functor.obj (quotient C (ComplexShape.up ℤ)) L₂)
    (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (φ₁ ≫ b''))
    (CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (a'' ≫ φ₂))

Tactic:
simp only [Functor.map_comp, ha', hb', reassoc_of% comm₁₁,
      reassoc_of% fac, comm₁₂, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_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₁ T₂ : Triangle (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
have :
  ∀ (H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
        T₁.mor₃ ≫
            CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
              a =
          c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

Tactic:
have H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂) := homotopyOfEq _ _ (by
    have comm₁₁ := e₁.inv.comm₁
    have comm₁₂ := e₂.hom.comm₁
    dsimp at comm₁₁ comm₁₂
    simp only [Functor.map_comp, ha', hb', reassoc_of% comm₁₁,
      reassoc_of% fac, comm₁₂, assoc])
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
⊢ T₁.mor₂ ≫ γ.hom₃ = γ.hom₂ ≫ T₂.mor₂

Tactic:
have comm₂ := γ.comm₂
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ : T₁.mor₂ ≫ γ.hom₃ = γ.hom₂ ≫ T₂.mor₂
⊢ T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        γ.hom₁ =
    γ.hom₃ ≫ T₂.mor₃

Tactic:
have comm₃ := γ.comm₃
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂

Tactic:
simp only [ha', hb'] at comm₂ comm₃
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
comm₄ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
⊢ T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃

Tactic:
simp only [ha', hb'] at comm₂ comm₃
-- 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 ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
        (e₁.hom.hom₁ ≫ (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁) ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ CategoryTheory.Functor.map (quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫
      T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧
      T₁.mor₃ ≫
          CategoryTheory.Functor.map (shiftFunctor (HomotopyCategory.{v_1, u_1, 0} C (ComplexShape.up ℤ)) (A := ℤ) 1)
            a =
        c ≫ T₂.mor₃

Tactic:
⟨γ.hom₃, ?_, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Pretriangulated.TriangleMorphism.hom₃