-- Mathlib/CategoryTheory/Triangulated/Functor.lean
lemma mem_mapTriangle_essImage_of_distinguished
    [F.IsTriangulated] [F.mapArrow.EssSurj] (T : Triangle D) (hT : T ∈ distTriang D) :
    ∃ (T' : Triangle C) (_ : T' ∈ distTriang C), Nonempty (F.mapTriangle.obj T' ≅ T)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ ∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)

Tactic:
obtain ⟨X, Y, f, e₁, e₂, w⟩ : ∃ (X Y : C) (f : X ⟶ Y) (e₁ : F.obj X ≅ T.obj₁)
  (e₂ : F.obj Y ≅ T.obj₂), F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁ := by
    let e := F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
    exact ⟨_, _, _, Arrow.leftFunc.mapIso e, Arrow.rightFunc.mapIso e, e.hom.w.symm⟩

Result:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
⊢ ∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
e : F.mapArrow.obj (F.mapArrow.objPreimage (Arrow.mk T.mor₁)) ≅ Arrow.mk T.mor₁ :=
  F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
⊢ ∃ X Y f e₁ e₂, F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁

Tactic:
exact ⟨_, _, _, Arrow.leftFunc.mapIso e, Arrow.rightFunc.mapIso e, e.hom.w.symm⟩

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ ∃ X Y f e₁ e₂, F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁

Tactic:
let e := F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)

Result:
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
e : F.mapArrow.obj (F.mapArrow.objPreimage (Arrow.mk T.mor₁)) ≅ Arrow.mk T.mor₁ :=
  F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
⊢ ∃ X Y f e₁ e₂, F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
⊢ ∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)

Tactic:
obtain ⟨W, g, h, H⟩ := distinguished_cocone_triangle f

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
W : C
g : Y ⟶ W
h : W ⟶ (shiftFunctor C 1).obj X
H : Triangle.mk f g h ∈ distinguishedTriangles
⊢ ∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_5, u_2} D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : HasShift D ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
W : C
g : Y ⟶ W
h : W ⟶ (shiftFunctor C 1).obj X
H : Triangle.mk f g h ∈ distinguishedTriangles
⊢ ∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)

Tactic:
exact ⟨_, H, ⟨isoTriangleOfIso₁₂ _ _ (F.map_distinguished _ H) hT e₁ e₂ w⟩⟩

Result:
no goals