-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
/-- A commutative square involving the morphisms `mor₃` of two distinguished triangles
can be extended as morphism of triangles -/
lemma complete_distinguished_triangle_morphism₂ (T₁ T₂ : Triangle C)
    (hT₁ : T₁ ∈ distTriang C) (hT₂ : T₂ ∈ distTriang C) (a : T₁.obj₁ ⟶ T₂.obj₁)
    (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : T₁.mor₃ ≫ a⟦(1 : ℤ)⟧' = c ≫ T₂.mor₃) :
    ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂

Tactic:
rw [← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃), assoc, assoc, ← ha₂]

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ T₁.mor₂ ≫ c ≫ (shiftEquiv C 1).counitIso.inv.app T₂.obj₃ =
    (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ T₁.invRotate.mor₁ ≫ a = (shiftFunctor C (-1)).map c ≫ T₂.invRotate.mor₁

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ (-(shiftFunctor C (-1)).map T₁.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₁.obj₁) ≫ a =
    (shiftFunctor C (-1)).map c ≫
      (-(shiftFunctor C (-1)).map T₂.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₂.obj₁)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ (-(shiftFunctor C (-1)).map T₁.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₁.obj₁) ≫ a =
    (shiftFunctor C (-1)).map c ≫
      (-(shiftFunctor C (-1)).map T₂.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T₂.obj₁)

Tactic:
simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm,
  Functor.map_comp, shift_shift_neg', Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Tactic:
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
  (inv_rot_of_distTriang _ hT₁) (inv_rot_of_distTriang _ hT₂) (c⟦(-1 : ℤ)⟧') a (by
  dsimp
  simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm,
    Functor.map_comp, shift_shift_neg', Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id])

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ T₂.invRotate.mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a✝ ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) = a ≫ T₂.invRotate.mor₃
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂

Tactic:
dsimp only [Triangle.invRotate, Triangle.mk] at ha₂

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ T₁.mor₂ ≫ c = a ≫ T₂.mor₂

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a✝ : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a✝ = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a✝ ≫ T₂.invRotate.mor₂
ha₂ :
  (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c) =
    a ≫ T₂.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₂.3
⊢ T₁.mor₂ ≫ c ≫ (shiftEquiv C 1).counitIso.inv.app T₂.obj₃ =
    (T₁.mor₂ ≫ (shiftEquiv C 1).counitIso.inv.app T₁.3) ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map c)

Tactic:
simp only [shiftEquiv'_counitIso, shift_neg_shift', assoc, Iso.inv_hom_id_app_assoc]

Result:
no goals