-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma mem_W_iff_of_distinguished
    [S.P.IsClosedUnderIsomorphisms] (T : Triangle C) (hT : T ∈ distTriang C) :
    S.W T.mor₁ ↔ S.P T.obj₃

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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
h : S.P T.obj₃
⊢ S.W T.mor₁

Tactic:
exact ⟨_, _, _, hT, h⟩

Result:
no goals

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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ S.P T.obj₃ → S.W T.mor₁

Tactic:
intro h

Result:
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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
h : S.P T.obj₃
⊢ S.W T.mor₁

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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ S.W T.mor₁ → S.P T.obj₃

Tactic:
rintro ⟨Z, g, h, hT', 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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
hT' : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
mem : S.P Z
⊢ S.P T.obj₃

Proof state:
case mp.intro.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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
hT' : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
mem : S.P Z
e : Triangle.mk T.mor₁ g h ≅ T
h✝ :
  e.hom.hom₁ = (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom.left ∧
    e.hom.hom₂ = (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom.right
⊢ S.P T.obj₃

Tactic:
exact S.P.prop_of_iso (Triangle.π₃.mapIso e) mem

Result:
no goals

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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
hT' : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
mem : S.P Z
⊢ S.P T.obj₃

Tactic:
obtain ⟨e, _⟩ := exists_iso_of_arrow_iso _ _ hT' hT (Iso.refl _)

Result:
case mp.intro.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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj T.obj₁
hT' : Triangle.mk T.mor₁ g h ∈ distinguishedTriangles
mem : S.P Z
e : Triangle.mk T.mor₁ g h ≅ T
h✝ :
  e.hom.hom₁ = (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom.left ∧
    e.hom.hom₂ = (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)).hom.right
⊢ S.P T.obj₃

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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ S.W T.mor₁ ↔ S.P T.obj₃

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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ S.W T.mor₁ → S.P T.obj₃

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
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ S.P T.obj₃ → S.W T.mor₁