awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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ᵒᵖ
⊢ adj.op.unit.app x =
    NatTrans.app
      (Adjunction.unit
        (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) ⋯) (OppositeShift.adjunction ℤ adj)))
      x
have 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)))))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (hypothesis)
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.CommShift ℤ
have eq : adj.op = PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) sorry) (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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)
⊢ adj.op.CommShift ℤ
have rw : Adjunction.CommShift (C := Dᵒᵖ) (D := Cᵒᵖ) (F := G.op) (G := F.op)
  (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) sorry) (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) sorry))
      (D :=
      PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ) (A := ℤ) (B := ℤ)
        (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) sorry))
      (PullbackShift.functor (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) sorry) (OppositeShift.functor ℤ G))
      (PullbackShift.functor (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) sorry) (OppositeShift.functor ℤ F)))
  ℤ
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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
⊢ 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))))
have 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))))
Tactic: obtain rfl : m = -n := by lia
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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
⊢ Eq (α := (F.op ⋙ shiftFunctor Dᵒᵖ n).obj X ⟶ (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)
    (NatTrans.app (Iso.inv (commShiftIso F.op n)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (commShiftIso F m)) (unop X)) ≫
        Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n m h)) X))))
have rw : Eq.{v_2 + 1} (α := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X ⟶ (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)
  (𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X))
  (Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m h)) X))) ≫
    CategoryStruct.comp (Y := op ((F ⋙ shiftFunctor D m).obj (unop 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))) ≫
        NatTrans.app (Iso.hom (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))) ≫
          Quiver.Hom.op (NatTrans.app (Iso.hom (commShiftIso F m)) (unop X)) ≫
            Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n m h)) X)))))
Tactic: rw [← cancel_epi ((F.op.commShiftIso n).hom.app X), Iso.hom_inv_id_app,
    op_commShiftIso_hom_app _ X n m h, assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 : ℤ
⊢ Eq (α :=
    F.obj
        (unop
          (obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
            X)) ⟶
      F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)))
    (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C n))) X)))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D n).obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)))
        (map (shiftFunctor D n) (Quiver.Hom.unop (NatTrans.app (Iso.inv (commShiftIso F.op n)) X)))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))))))
have dsimp : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
    F.obj (unop X))
  (F.map
      (map (shiftFunctor C n) (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) sorry)) X)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-n) n sorry)) (unop X)) :
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
      F.obj (unop X))
  (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
          (unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))))
        (map (shiftFunctor D n) (Quiver.Hom.unop (NatTrans.app (Iso.inv (commShiftIso F.op n)) X)) :
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
              (unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))))
        (map (shiftFunctor D n)
              (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) sorry)) (op (F.obj (unop X))))) ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)) :
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
              (unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))) ⟶
            F.obj (unop X))) :
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
      F.obj (unop X))
Tactic: dsimp [opShiftFunctorEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 : ℤ
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
      F.obj (unop X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (map (shiftFunctor D n) (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F (-n))) (unop X)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X))))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (map (shiftFunctor D n) (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
            (unop (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X))))))
          (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F (-n))) (unop X)))
          (map (shiftFunctor D n)
              (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
            map (shiftFunctor D n)
                (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))))
have e_a : Eq.{v_2 + 1} (α :=
  obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
    obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)) :
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
  (map (shiftFunctor D n)
        (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) sorry)) (op (F.obj (unop X))))) ≫
      map (shiftFunctor D n)
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) sorry)) (op (F.obj (unop X))))) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)) :
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
        (unop (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X))))) ⟶
      F.obj (unop X))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 : ℤ
⊢ Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
        obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (map (shiftFunctor D n)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
        map (shiftFunctor D n)
            (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
          (unop (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X))))) ⟶
        F.obj (unop X))
have e_a : Eq.{v_2 + 1} (α :=
  obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
    obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)))
  (map (shiftFunctor D n)
      (Quiver.Hom.unop (𝟙 (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X)))))) ≫
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)))
Tactic: rw [← Functor.map_comp_assoc, ← unop_comp,
    Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 : ℤ
⊢ Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))
    (map (shiftFunctor D n)
        (Quiver.Hom.unop (𝟙 (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X)))))) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))
have e_a : Eq.{v_2 + 1} (α :=
  obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
    F.obj (unop X))
  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)) :
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
  (map (shiftFunctor D n) (𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)) :
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
      F.obj (unop X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 : ℤ
⊢ Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
      F.obj (unop X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
        obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (map (shiftFunctor D n) (𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
        F.obj (unop X))
have e_a : NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)) =
  𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X))
Tactic: rw [map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 : ℤ
e_a :
  NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) =
    𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X))
⊢ Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
      F.obj (unop X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
        obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (map (shiftFunctor D n) (𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
        F.obj (unop X))
have e_a₁ : Eq.{v_2 + 1} (α :=
  obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
    F.obj (unop X))
  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)))
  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n sorry)) (F.obj (unop X)))
Tactic: rw [map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 : ℤ
⊢ Eq (α :=
    op
        (F.obj
          (unop
            (obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C n))
              X))) ⟶
      op (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))))
    (Quiver.Hom.op
      (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence C n))) X))))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        unop
          (obj.{v_2, v_2, u_2, u_2}
            (Equivalence.inverse (opShiftFunctorEquivalence D n) ⋙ Equivalence.functor (opShiftFunctorEquivalence D n))
            (op (F.obj (unop X)))))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))))
        (CategoryStruct.comp (Y :=
          unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((shiftFunctor C n ⋙ F).obj (unop X)))))
          (Quiver.Hom.unop
              (map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F n)) (unop X)))) :
            unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((F ⋙ shiftFunctor D n).obj (unop X)))) ⟶
              unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op ((shiftFunctor C n ⋙ F).obj (unop X)))))
          (Quiver.Hom.unop
              (NatTrans.app (Iso.hom (commShiftIso F.op n))
                (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) :
            unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))) ⟶
              unop ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))))))))
have a : Eq (α :=
  op
      (F.obj
        (unop
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
            (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))))) ⟶
    op (F.obj (unop X)))
  (Quiver.Hom.op
    (F.map
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n (-n) sorry)) (unop X) ≫
        Quiver.Hom.unop
          (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) sorry))
            (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X)))))))
  (CategoryStruct.comp (Y :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))))
    (NatTrans.app (Iso.hom (commShiftIso F.op n)) (op (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop X))) ≫
      map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F n)) (unop X))))
    (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) sorry))
        (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D n (-n) sorry)) (F.obj (unop X)))))
Tactic: dsimp [opShiftFunctorEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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 ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
X Y : (Triangle.{v_1, u_1} C)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    Triangle.obj₁ (obj (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) X) ⟶
      Triangle.obj₁ (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) Y))
    (TriangleMorphism.hom₁
      (map (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) f ≫
        Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            Y)))
    (TriangleMorphism.hom₁
      (Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            X) ≫
        map (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) f))
have h₁ : Eq.{v_2 + 1} (α := op (F.obj (unop X).obj₃) ⟶ op (F.obj (unop Y).obj₃))
  ((F.map f.unop.hom₃).op ≫ 𝟙 (op (F.obj (unop Y).obj₃))) (𝟙 (op (F.obj (unop X).obj₃)) ≫ (F.map f.unop.hom₃).op)
Tactic: dsimp