-- 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) (b : T₁.obj₂ ⟶ T₂.obj₂)
    (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂) :
    ∃ (a : T₁.obj₁ ⟶ T₂.obj₁), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧
      T₁.mor₃ ≫ a⟦(1 : ℤ)⟧' = c ≫ T₂.mor₃

Proof state:
case intro.intro.refine_1.a
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : (shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = a ≫ (shiftFunctor C 1).map T₂.mor₁
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)

Tactic:
simpa only [Functor.map_comp, Functor.map_preimage] using ha₂

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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃

Tactic:
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
  (rot_of_distTriang _ hT₁) (rot_of_distTriang _ hT₂) b c comm

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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃

Proof state:
case intro.intro.refine_2
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a) = c ≫ T₂.mor₃

Tactic:
simpa only [Functor.map_preimage] using ha₁

Result:
no goals

Proof state:
case intro.intro.refine_1.a
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : (-(shiftFunctor C 1).map T₁.mor₁) ≫ (shiftFunctor C 1).map b = a ≫ (-(shiftFunctor C 1).map T₂.mor₁)
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)

Tactic:
rw [neg_comp, comp_neg, neg_inj] at ha₂

Result:
case intro.intro.refine_1.a
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : (shiftFunctor C 1).map T₁.mor₁ ≫ (shiftFunctor C 1).map b = a ≫ (shiftFunctor C 1).map T₂.mor₁
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage 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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃

Tactic:
refine ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩

Result:
case intro.intro.refine_1
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ T₁.mor₁ ≫ b = (shiftFunctor C 1).preimage a ≫ T₂.mor₁

case intro.intro.refine_2
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a) = c ≫ T₂.mor₃

Proof state:
case intro.intro.refine_1
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ T₁.mor₁ ≫ b = (shiftFunctor C 1).preimage a ≫ T₂.mor₁

Tactic:
apply (shiftFunctor C (1 : ℤ)).map_injective

Result:
case intro.intro.refine_1.a
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
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)