awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
⊢ (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (trW (B.op.inverseImage A.op.ι))

Tactic:
have : (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (B.op.inverseImage A.op.ι).trW := by
    refine Functor.IsLocalization.of_equivalence_source L₁.op (B.inverseImage A.ι).trW.op
      _ _ A.opEquivalence.symm ?_ ?_
      ((Functor.associator _ _ _).symm ≪≫
        Functor.isoWhiskerRight A.opEquivalence.counitIso _ ≪≫ Functor.leftUnitor _)
    · rw [← trW_op, ← inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op]
      intro _ _ f hf
      simp only [MorphismProperty.inverseImage_iff, Equivalence.symm_functor] at hf ⊢
      exact MorphismProperty.le_isoClosure _ _ hf
    · refine fun _ _ _ hf ↦ Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_
      simpa [trW_inverseImage_ι_iff, ← op_inf, trW_op] using hf
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this_2 : L₂.op.IsLocalization B.op.trW
this : (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (trW (B.op.inverseImage A.op.ι))
⊢ LocalizerMorphism.IsLocalizedFullyFaithful (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
    (A.triangulatedLocalizerMorphism B)

Tactic:
LocalizerMorphism.IsLocalizedFullyFaithful.mk' (A.triangulatedLocalizerMorphism B)
    L₁ L₂ F (((A.op.triangulatedLocalizerMorphism B.op).fullyFaithful
    (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op).unop)

Premises used: CategoryTheory.Functor.op, CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk', CategoryTheory.LocalizerMorphism.fullyFaithful, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.triangulatedLocalizerMorphism, CategoryTheory.Equivalence.functor, CategoryTheory.ObjectProperty.opEquivalence, CategoryTheory.ObjectProperty.op, CategoryTheory.Functor.FullyFaithful.unop
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
this_1 : CatCommSq
  (LocalizerMorphism.functor (W₁ := trW (B.op.inverseImage A.op.ι)) (W₂ := B.op.trW)
    (A.op.triangulatedLocalizerMorphism B.op))
  (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op
          (CatCommSq.iso
              (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
                (A.triangulatedLocalizerMorphism B))
              L₁ L₂ F).symm) }
this_2 : L₂.op.IsLocalization B.op.trW
this : (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (trW (B.op.inverseImage A.op.ι))
⊢ LocalizerMorphism.IsLocalizedFullyFaithful (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
    (A.triangulatedLocalizerMorphism B)

Tactic:
exact LocalizerMorphism.IsLocalizedFullyFaithful.mk' (A.triangulatedLocalizerMorphism B)
    L₁ L₂ F (((A.op.triangulatedLocalizerMorphism B.op).fullyFaithful
    (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op).unop)

Premises used: CategoryTheory.Functor.op, CategoryTheory.LocalizerMorphism.IsLocalizedFullyFaithful.mk', CategoryTheory.LocalizerMorphism.fullyFaithful, CategoryTheory.Functor.comp, CategoryTheory.ObjectProperty.triangulatedLocalizerMorphism, CategoryTheory.Equivalence.functor, CategoryTheory.ObjectProperty.opEquivalence, CategoryTheory.ObjectProperty.op, CategoryTheory.Functor.FullyFaithful.unop
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
⊢ (LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
      L₁ L₂).Full

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
⊢ (LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
      L₁ L₂).Faithful

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
inst_16 : A.IsVerdierLeftLocalizing B
inst_17 : Preadditive.{v_3, u_3} D₁
inst_18 : Preadditive.{v_4, u_4} D₂
inst_19 : L₁.Additive
inst_20 : L₂.Additive
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
rw :
  (L₁ ⋙
      LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
        (A.triangulatedLocalizerMorphism B) L₁ L₂).Additive
⊢ (LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
      L₁ L₂).Additive

Tactic:
rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW]

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Localization.functor_additive_iff, CategoryTheory.ObjectProperty.trW, CategoryTheory.ObjectProperty.inverseImage
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
inst_16 : A.IsVerdierLeftLocalizing B
inst_17 : Preadditive.{v_3, u_3} D₁
inst_18 : Preadditive.{v_4, u_4} D₂
inst_19 : L₁.Additive
inst_20 : L₂.Additive
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)) L₁ L₂
    F
⊢ (L₁ ⋙
      LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
        (A.triangulatedLocalizerMorphism B) L₁ L₂).Additive

Tactic:
Functor.additive_of_iso e

Premises used: CategoryTheory.Functor.additive_of_iso
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasShift.{v_1, u_1, 0} C ℤ
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : IsTriangulated.{v_1, u_1} C
inst_10 : A.IsTriangulated
inst_11 : B.IsTriangulated
inst_12 : B.IsClosedUnderIsomorphisms
inst_13 : A.IsVerdierLeftLocalizing B
L₁ : Functor.{v_1, v_3, u_1, u_3} A.FullSubcategory D₁
L₂ : Functor.{v_1, v_4, u_1, u_4} C D₂
inst_14 : L₁.IsLocalization (B.inverseImage A.ι).trW
inst_15 : L₂.IsLocalization B.trW
inst_16 : A.IsVerdierLeftLocalizing B
inst_17 : Preadditive.{v_3, u_3} D₁
inst_18 : Preadditive.{v_4, u_4} D₂
inst_19 : L₁.Additive
inst_20 : L₂.Additive
F : Functor.{v_3, v_4, u_3, u_4} D₁ D₂ :=
  LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)
    L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
  CatCommSq.iso
    (LocalizerMorphism.functor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW) (A.triangulatedLocalizerMorphism B)) L₁ L₂
    F
⊢ (L₁ ⋙
      LocalizerMorphism.localizedFunctor (W₁ := (B.inverseImage A.ι).trW) (W₂ := B.trW)
        (A.triangulatedLocalizerMorphism B) L₁ L₂).Additive

Tactic:
exact Functor.additive_of_iso e

Premises used: CategoryTheory.Functor.additive_of_iso
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
a b : ℤ
⊢ -(a + b) = -a + -b

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : G.CommShift ℤ
τ : F ⟶ G
inst_6 : NatTrans.CommShift τ ℤ
a b : ℤ
⊢ -(a + b) = -a + -b

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
a b : ℤ
⊢ -(a + b) = -a + -b

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
h :
  ∀ (x : Dᵒᵖ),
    adj.op.unit.app x =
      NatTrans.app
        (Adjunction.unit
          (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)))
        x
⊢ adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
x : Dᵒᵖ
h :
  Eq (α := x ⟶ op (F.obj (G.obj (unop x)))) (Quiver.Hom.op (adj.counit.app (unop x)))
    (𝟙 x ≫
      (𝟙 x ≫ Quiver.Hom.op (adj.counit.app (unop x)) ≫ 𝟙 (op (F.obj (G.obj (unop x))))) ≫
        𝟙 (op (F.obj (G.obj (unop x)))))
⊢ adj.op.unit.app x =
    NatTrans.app
      (Adjunction.unit
        (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)))
      x

Tactic:
dsimp [PullbackShift.adjunction, NatTrans.PullbackShift.natIsoId,
      NatTrans.PullbackShift.natIsoComp, PullbackShift.functor, PullbackShift.natTrans,
      OppositeShift.adjunction, OppositeShift.natTrans, NatTrans.OppositeShift.natIsoId,
      NatTrans.OppositeShift.natIsoComp, OppositeShift.functor]

Premises used: CategoryTheory.OppositeShift.natTrans, CategoryTheory.NatTrans.PullbackShift.natIsoComp, CategoryTheory.NatTrans.PullbackShift.natIsoId, CategoryTheory.PullbackShift.natTrans, CategoryTheory.OppositeShift.adjunction, CategoryTheory.NatTrans.OppositeShift.natIsoComp, CategoryTheory.PullbackShift.adjunction, CategoryTheory.OppositeShift.functor, CategoryTheory.PullbackShift.functor, CategoryTheory.NatTrans.OppositeShift.natIsoId
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
x : Dᵒᵖ
⊢ Eq (α := x ⟶ op (F.obj (G.obj (unop x)))) (Quiver.Hom.op (adj.counit.app (unop x)))
    (𝟙 x ≫
      (𝟙 x ≫ Quiver.Hom.op (adj.counit.app (unop x)) ≫ 𝟙 (op (F.obj (G.obj (unop x))))) ≫
        𝟙 (op (F.obj (G.obj (unop x)))))

Tactic:
simp only [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
⊢ adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)

Tactic:
have eq : adj.op = PullbackShift.adjunction
    (AddMonoidHom.mk' (fun (n : ℤ) => -n) (by intros; dsimp; lia))
      (OppositeShift.adjunction ℤ adj) := by
    ext
    dsimp [PullbackShift.adjunction, NatTrans.PullbackShift.natIsoId,
      NatTrans.PullbackShift.natIsoComp, PullbackShift.functor, PullbackShift.natTrans,
      OppositeShift.adjunction, OppositeShift.natTrans, NatTrans.OppositeShift.natIsoId,
      NatTrans.OppositeShift.natIsoComp, OppositeShift.functor]
    simp only [Category.comp_id, Category.id_comp]
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
rw :
  Adjunction.CommShift (C := Dᵒᵖ) (D := Cᵒᵖ) (F := G.op) (G := F.op)
    (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj) :
      Adjunction (C :=
        PullbackShift.{v_2, u_2, 0, 0} (OppositeShift.{v_2, u_2, 0} D ℤ) (A := ℤ) (B := ℤ)
          (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯))
        (D :=
        PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ) (A := ℤ) (B := ℤ)
          (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯))
        (PullbackShift.functor (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.functor ℤ G))
        (PullbackShift.functor (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.functor ℤ F)))
    ℤ
⊢ adj.op.CommShift ℤ

Tactic:
rw [eq]
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
a b : ℤ
⊢ -(a + b) = -a + -b

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
G : Functor.{v_2, v_1, u_2, u_1} D C
inst_5 : G.CommShift ℤ
adj : F ⊣ G
inst_6 : adj.CommShift ℤ
eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)
⊢ Adjunction.CommShift (C := Dᵒᵖ) (D := Cᵒᵖ) (F := G.op) (G := F.op)
    (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj) :
      Adjunction (C :=
        PullbackShift.{v_2, u_2, 0, 0} (OppositeShift.{v_2, u_2, 0} D ℤ) (A := ℤ) (B := ℤ)
          (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯))
        (D :=
        PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ) (A := ℤ) (B := ℤ)
          (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯))
        (PullbackShift.functor (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.functor ℤ G))
        (PullbackShift.functor (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.functor ℤ F)))
    ℤ

Tactic:
exact inferInstanceAs (Adjunction.CommShift (PullbackShift.adjunction
    (AddMonoidHom.mk' (fun (n : ℤ) => -n) (by intros; dsimp; lia))
      (OppositeShift.adjunction ℤ adj)) ℤ)
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ m = -n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
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 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
obtain :
  ∀ (h : n + -n = 0),
    Eq (α := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X ⟶ (F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)
      (NatTrans.app (Iso.hom (commShiftIso F.op n)) X)
      (Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) h)) X))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F (-n))) (unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) h)) (op (F.obj (unop X))))
⊢ Eq (α := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X ⟶ (F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F.op n)) X)
    (Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m h)) X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F m)) (unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl