awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsStableUnderShift ℤ
X₁ X₂ : C
f : X₁ ⟶ X₂
n : ℤ
hf : P.trW (X := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₁) (Functor.map (shiftFunctor C n) f)
⊢ P.trW f

Tactic:
(P.trW.arrow_mk_iso_iff
     (Arrow.isoOfNatIso (shiftEquiv C n).unitIso (Arrow.mk f))).2 (hf.shift (-n))

Premises used: Iff.mpr, CategoryTheory.Equivalence.unitIso, CategoryTheory.shiftEquiv, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.ObjectProperty.trW, CategoryTheory.Arrow.isoOfNatIso, CategoryTheory.Arrow.mk, CategoryTheory.ObjectProperty.trW.shift, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsStableUnderShift ℤ
n : ℤ
h : ∀ ⦃K L : C⦄ (f : K ⟶ L), P.trW.inverseImage (shiftFunctor C n) f ↔ P.trW f
⊢ P.trW.inverseImage (shiftFunctor C n) = P.trW

Tactic:
ext K L f
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsStableUnderShift ℤ
n : ℤ
K L : C
f : K ⟶ L
⊢ P.trW.inverseImage (shiftFunctor C n) f ↔ P.trW f

Tactic:
⟨fun hf => hf.unshift, fun hf => hf.shift n⟩

Premises used: CategoryTheory.ObjectProperty.trW.unshift, Iff.intro, CategoryTheory.ObjectProperty.trW.shift
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsStableUnderShift ℤ
n : ℤ
K L : C
f : K ⟶ L
⊢ P.trW.inverseImage (shiftFunctor C n) f ↔ P.trW f

Tactic:
exact ⟨fun hf => hf.unshift, fun hf => hf.shift n⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
rw : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P.isoClosure.trW f → P.isoClosure.trW g → P.isoClosure.trW (f ≫ g)
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P.trW f → P.trW g → P.trW (f ≫ g)

Tactic:
rw [← trW_isoClosure]

Premises used: CategoryTheory.ObjectProperty.trW_isoClosure
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X₁ X₂ X₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
Z₁₂ : C
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
H₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
mem₁₂ : P.isoClosure Z₁₂
Z₂₃ : C
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂
H₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
mem₂₃ : P.isoClosure Z₂₃
obtain :
  ∀ (Z₁₃ : C) (v₁₃ : X₃ ⟶ Z₁₃) (w₁₂ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁)
    (H₁₃ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk (u₁₂ ≫ u₂₃) v₁₃ w₁₂)),
    P.isoClosure.trW (u₁₂ ≫ u₂₃)
⊢ P.isoClosure.trW (u₁₂ ≫ u₂₃)

Tactic:
obtain ⟨Z₁₃, v₁₃, w₁₂, H₁₃⟩ := distinguished_cocone_triangle (u₁₂ ≫ u₂₃)

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X₁ X₂ X₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
Z₁₂ : C
v₁₂ : X₂ ⟶ Z₁₂
w₁₂_1 : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
H₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂_1)
mem₁₂ : P.isoClosure Z₁₂
Z₂₃ : C
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂
H₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
mem₂₃ : P.isoClosure Z₂₃
Z₁₃ : C
v₁₃ : X₃ ⟶ Z₁₃
w₁₂ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
H₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (u₁₂ ≫ u₂₃) v₁₃ w₁₂)
⊢ P.isoClosure.trW (u₁₂ ≫ u₂₃)

Tactic:
⟨_, _, _, H₁₃, P.isoClosure.ext_of_isTriangulatedClosed₂
      _ (someOctahedron rfl H₁₂ H₂₃ H₁₃).mem mem₁₂ mem₂₃⟩

Premises used: CategoryTheory.Triangulated.Octahedron.mem, CategoryTheory.Triangulated.someOctahedron, CategoryTheory.ObjectProperty.trW, CategoryTheory.ObjectProperty.isoClosure, Exists.intro, CategoryTheory.ObjectProperty.ext_of_isTriangulatedClosed₂, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X₁ X₂ X₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
Z₁₂ : C
v₁₂ : X₂ ⟶ Z₁₂
w₁₂_1 : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
H₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂_1)
mem₁₂ : P.isoClosure Z₁₂
Z₂₃ : C
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂
H₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
mem₂₃ : P.isoClosure Z₂₃
Z₁₃ : C
v₁₃ : X₃ ⟶ Z₁₃
w₁₂ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
H₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (u₁₂ ≫ u₂₃) v₁₃ w₁₂)
⊢ P.isoClosure.trW (u₁₂ ≫ u₂₃)

Tactic:
exact ⟨_, _, _, H₁₃, P.isoClosure.ext_of_isTriangulatedClosed₂
      _ (someOctahedron rfl H₁₂ H₂₃ H₁₃).mem mem₁₂ mem₂₃⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : P.trW T.mor₁ → P T.obj₃
mpr : P T.obj₃ → P.trW T.mor₁
⊢ P.trW T.mor₁ ↔ P T.obj₃

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk T.mor₁ g h)
mem : P Z
mp :
  ∀ (e : Triangle.mk T.mor₁ g h ≅ T),
    e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁))) ∧
        e.hom.hom₂ = Arrow.Hom.right (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁))) →
      P T.obj₃
⊢ P T.obj₃

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

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk T.mor₁ g h)
mem : P Z
e : Triangle.mk T.mor₁ g h ≅ T
h_1 :
  e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁))) ∧
    e.hom.hom₂ = Arrow.Hom.right (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)))
⊢ P T.obj₃

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

Premises used: CategoryTheory.Pretriangulated.Triangle.π₃, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk T.mor₁ g h)
mem : P Z
e : Triangle.mk T.mor₁ g h ≅ T
h_1 :
  e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁))) ∧
    e.hom.hom₂ = Arrow.Hom.right (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁)))
⊢ P T.obj₃

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

Premises used: CategoryTheory.Pretriangulated.Triangle.π₃, CategoryTheory.ObjectProperty.prop_of_iso, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : P T.obj₃
⊢ P.trW T.mor₁

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

Premises used: CategoryTheory.ObjectProperty.trW, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
h : P T.obj₃
⊢ P.trW T.mor₁

Tactic:
exact ⟨_, _, _, hT, h⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsStableUnderShift ℤ
inst_7 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ P.trW T.mor₂ ↔ P T.obj₁

Tactic:
simpa [P.prop_shift_iff_of_isStableUnderShift]
    using P.trW_iff_of_distinguished _ (rot_of_distTriang _ hT)

Premises used: CategoryTheory.ObjectProperty.prop_shift_iff_of_isStableUnderShift, CategoryTheory.ObjectProperty.trW_iff_of_distinguished, CategoryTheory.Pretriangulated.rot_of_distTriang
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
obtain :
  ∀ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X)
    (hT :
      Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
        (Triangle.mk s g h)),
    (P.inverseImage F).trW s ↔ P.trW (F.map s)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)

Tactic:
obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle s

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
⊢ (P.inverseImage F).trW (Triangle.mk s g h).mor₁ ↔ P.inverseImage F (Triangle.mk s g h).obj₃

Tactic:
have eq₁ := (P.inverseImage F).trW_iff_of_distinguished _ hT
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
eq₁ : (P.inverseImage F).trW (Triangle.mk s g h).mor₁ ↔ P.inverseImage F (Triangle.mk s g h).obj₃
⊢ P.trW (X := Triangle.obj₁ (Functor.obj F.mapTriangle (Triangle.mk s g h)))
      (Triangle.mor₁ (Functor.obj F.mapTriangle (Triangle.mk s g h))) ↔
    P (Triangle.obj₃ (Functor.obj F.mapTriangle (Triangle.mk s g h)))

Tactic:
have eq₂ := P.trW_iff_of_distinguished _ (F.map_distinguished _ hT)
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
rw : P.inverseImage F Z ↔ P.trW (F.map s)
rw₁ : P (F.obj Z) ↔ P.trW (F.map s)
rw₂ rw₃ : P (F.obj Z) ↔ P (F.obj Z)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)

Tactic:
rw [eq₁, prop_inverseImage_iff, eq₂]

Premises used: CategoryTheory.ObjectProperty.prop_inverseImage_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
E : Type u_4
inst_15 : Category.{u_5, u_4} E
L : Functor.{v_1, u_5, u_1, u_4} C E
inst_16 : L.IsLocalization P.trW
X Y : D
f : X ⟶ Y
hf : (P.inverseImage F).trW f
⊢ P.trW (F.map f)

Tactic:
simpa only [inverseImage_trW_iff] using hf

Premises used: CategoryTheory.ObjectProperty.inverseImage_trW_iff