-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma W_iff' {Y Z : C} (g : Y ⟶ Z) :
    S.W g ↔ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ X⟦(1 : ℤ)⟧)
      (_ : Triangle.mk f g h ∈ distTriang C), S.P X

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), S.P Z_1) ↔
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), S.P Z_1) →
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X

case mpr
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z : C
g : Y ⟶ Z
⊢ (∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X) →
    ∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), S.P Z_1

Proof state:
case mpr.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z✝ : C
g✝ : Y ⟶ Z✝
Z : C
g : Z ⟶ Y
h : Z✝ ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g g✝ h ∈ distinguishedTriangles
mem : S.P Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk g✝ g h ∈ distinguishedTriangles), S.P Z

Tactic:
exact ⟨_, _, _, rot_of_distTriang _ H, S.shift _ 1 mem⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z : C
g : Y ⟶ Z
⊢ S.W g ↔ ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X

Tactic:
rw [S.W_iff]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), S.P Z_1) ↔
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X

Proof state:
case mpr
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z : C
g : Y ⟶ Z
⊢ (∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X) →
    ∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), S.P Z_1

Tactic:
rintro ⟨Z, g, h, H, mem⟩

Result:
case mpr.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z✝ : C
g✝ : Y ⟶ Z✝
Z : C
g : Z ⟶ Y
h : Z✝ ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g g✝ h ∈ distinguishedTriangles
mem : S.P Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk g✝ g h ∈ distinguishedTriangles), S.P Z

Proof state:
case mp.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z✝ : C
g✝ : Y ⟶ Z✝
Z : C
g : Z✝ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
H : Triangle.mk g✝ g h ∈ distinguishedTriangles
mem : S.P Z
⊢ ∃ X f h, ∃ (_ : Triangle.mk f g✝ h ∈ distinguishedTriangles), S.P X

Tactic:
exact ⟨_, _, _, inv_rot_of_distTriang _ H, S.shift _ (-1) mem⟩

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), S.P Z_1) →
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P X

Tactic:
rintro ⟨Z, g, h, H, mem⟩

Result:
case mp.intro.intro.intro.intro
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
Y Z✝ : C
g✝ : Y ⟶ Z✝
Z : C
g : Z✝ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
H : Triangle.mk g✝ g h ∈ distinguishedTriangles
mem : S.P Z
⊢ ∃ X f h, ∃ (_ : Triangle.mk f g✝ h ∈ distinguishedTriangles), S.P X