awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα :
  α =
    φ -
      ψ ≫
        ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
            (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
          h
hα₀ : α ≫ G.map T.mor₃ = 0
β : F.obj Y ⟶ T.obj₂
hβ :
  ((Equiv.symm (adj.homEquiv Y T.obj₃) : Equiv.{v_1 + 1, v_2 + 1} (Y ⟶ G.obj T.obj₃) (F.obj Y ⟶ T.obj₃)) :
        (a : Y ⟶ G.obj T.obj₃) → F.obj Y ⟶ T.obj₃)
      α =
    β ≫ T.mor₂
⊢ ∃ (β : Y ⟶ Z),
    β ≫
        ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
            (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
          h =
      α

Tactic:
⟨adj.homEquiv _ _ β ≫ f, ?_⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Adjunction.homEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this_2 :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
this :
  IsIso.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) (G.map T.mor₂)
      (G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁))

Tactic:
isomorphic_distinguished _ mem _ (Iso.symm ?_)

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this_2 :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
this :
  IsIso.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
refine :
  Triangle.mk (G.map T.mor₁) f g ≅
    Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) (G.map T.mor₂)
      (G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁))

Tactic:
refine isomorphic_distinguished _ mem _ (Iso.symm ?_)

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this_2 :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
this :
  IsIso.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
⊢ (Triangle.mk (G.map T.mor₁) f g).mor₁ ≫ Iso.hom (Iso.refl (Triangle.mk (G.map T.mor₁) f g).obj₂) =
    Iso.hom (Iso.refl (Triangle.mk (G.map T.mor₁) f g).obj₁) ≫
      Triangle.mor₁
        (Triangle.mk (G.map T.mor₁) (G.map T.mor₂)
          (G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this_2 :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
this :
  IsIso.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
refine_3 :
  g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (G.obj T.obj₁)) =
    ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁
⊢ (Triangle.mk (G.map T.mor₁) f g).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (Iso.refl (Triangle.mk (G.map T.mor₁) f g).obj₁)) =
    Iso.hom
        (asIso
          (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
              (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
            h)) ≫
      Triangle.mor₃
        (Triangle.mk (G.map T.mor₁) (G.map T.mor₂)
          (G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : G.IsTriangulated
⊢ F.op.IsTriangulated

Tactic:
have := isTriangulated_rightAdjoint adj.op
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : G.IsTriangulated
this : F.op.IsTriangulated
⊢ F.IsTriangulated

Tactic:
F.isTriangulated_of_op

Premises used: CategoryTheory.Functor.isTriangulated_of_op
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : G.IsTriangulated
this : F.op.IsTriangulated
⊢ F.IsTriangulated

Tactic:
exact F.isTriangulated_of_op

Premises used: CategoryTheory.Functor.isTriangulated_of_op
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_12 : E.functor.CommShift ℤ
inst_13 : E.inverse.CommShift ℤ
inst_14 : E.CommShift ℤ
inst_15 : E.IsTriangulated
⊢ E.functor.IsTriangulated

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_12 : E.functor.CommShift ℤ
inst_13 : E.inverse.CommShift ℤ
inst_14 : E.CommShift ℤ
inst_15 : E.IsTriangulated
⊢ E.inverse.IsTriangulated

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_12 : E.functor.CommShift ℤ
inst_13 : E.inverse.CommShift ℤ
inst_14 : E.CommShift ℤ
h : E.functor.IsTriangulated
⊢ E.symm.inverse.IsTriangulated

Tactic:
h

Premises used: CategoryTheory.Equivalence.CommShift.instCommShiftInverseSymm._aux_1
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_12 : E.functor.CommShift ℤ
inst_13 : E.inverse.CommShift ℤ
inst_14 : E.CommShift ℤ
h : E.inverse.IsTriangulated
⊢ E.symm.functor.IsTriangulated

Tactic:
h

Premises used: CategoryTheory.Equivalence.CommShift.instCommShiftFunctorSymm._aux_1
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_12 : E.functor.CommShift ℤ
inst_13 : E.inverse.CommShift ℤ
inst_14 : E.CommShift ℤ
⊢ Adjunction.IsTriangulated.{v_1, u_1, v_1, u_1} (C := C) Adjunction.id

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_12 : E.functor.CommShift ℤ
inst_13 : E.inverse.CommShift ℤ
inst_14 : E.CommShift ℤ
D' : Type u_3
inst_15 : Category.{v_3, u_3} D'
inst_16 : HasZeroObject.{v_3, u_3} D'
inst_17 : Preadditive.{v_3, u_3} D'
inst_18 : HasShift.{v_3, u_3, 0} D' ℤ
inst_19 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D' n)
inst_20 : Pretriangulated.{v_3, u_3} D'
E' : Equivalence.{v_2, v_3, u_2, u_3} D D'
inst_21 : E'.functor.CommShift ℤ
inst_22 : E'.inverse.CommShift ℤ
inst_23 : E'.CommShift ℤ
inst_24 : E.IsTriangulated
inst_25 : E'.IsTriangulated
rw : (E.toAdjunction.comp E'.toAdjunction).IsTriangulated
⊢ (E.trans E').toAdjunction.IsTriangulated

Tactic:
rw [trans_toAdjunction]

Premises used: CategoryTheory.Equivalence.trans_toAdjunction
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
inst_12 : E.functor.CommShift ℤ
inst_13 : E.inverse.CommShift ℤ
inst_14 : E.CommShift ℤ
D' : Type u_3
inst_15 : Category.{v_3, u_3} D'
inst_16 : HasZeroObject.{v_3, u_3} D'
inst_17 : Preadditive.{v_3, u_3} D'
inst_18 : HasShift.{v_3, u_3, 0} D' ℤ
inst_19 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D' n)
inst_20 : Pretriangulated.{v_3, u_3} D'
E' : Equivalence.{v_2, v_3, u_2, u_3} D D'
inst_21 : E'.functor.CommShift ℤ
inst_22 : E'.inverse.CommShift ℤ
inst_23 : E'.CommShift ℤ
inst_24 : E.IsTriangulated
inst_25 : E'.IsTriangulated
⊢ (E.toAdjunction.comp E'.toAdjunction).IsTriangulated

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
f g : A ⟶ B
h₁ : f.hom₁ = g.hom₁
h₂ : f.hom₂ = g.hom₂
h₃ : f.hom₃ = g.hom₃
⊢ f = g

Tactic:
TriangleMorphism.ext h₁ h₂ h₃

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A : Triangle.{v, u} C
⊢ TriangleMorphism.hom₁ (𝟙 A) = 𝟙 A.obj₁

Tactic:
rfl

Premises used: rfl