awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
rw :
  Eq (α :=
    Iso (C := Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor.{v_1, u_1, u_3} (OppositeShift.{v_1, u_1, u_3} C A) (A := A) 0 ⋙ OppositeShift.functor A F)
      (OppositeShift.functor A F ⋙ shiftFunctor.{v_2, u_2, u_3} (OppositeShift.{v_2, u_2, u_3} D A) (A := A) 0))
    (Iso.symm (NatIso.op (CommShift.isoZero F A))) (CommShift.isoZero (OppositeShift.functor A F) A)
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor.{v_1, u_1, u_3} (OppositeShift.{v_1, u_1, u_3} C A) (A := A) 0 ⋙ OppositeShift.functor A F)
      (OppositeShift.functor A F ⋙ shiftFunctor.{v_2, u_2, u_3} (OppositeShift.{v_2, u_2, u_3} D A) (A := A) 0))
    (Iso.symm (NatIso.op (commShiftIso F 0))) (CommShift.isoZero (OppositeShift.functor A F) A)

Tactic:
rw [commShiftIso_zero]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
w :
  ∀ (x : Cᵒᵖ),
    Eq (α :=
      (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F).op.obj x ⟶
        (F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0).op.obj x)
      (NatTrans.app (Iso.hom (Iso.symm (NatIso.op (CommShift.isoZero F A)))) x)
      (NatTrans.app (Iso.hom (CommShift.isoZero (OppositeShift.functor A F) A)) x)
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor.{v_1, u_1, u_3} (OppositeShift.{v_1, u_1, u_3} C A) (A := A) 0 ⋙ OppositeShift.functor A F)
      (OppositeShift.functor A F ⋙ shiftFunctor.{v_2, u_2, u_3} (OppositeShift.{v_2, u_2, u_3} D A) (A := A) 0))
    (Iso.symm (NatIso.op (CommShift.isoZero F A))) (CommShift.isoZero (OppositeShift.functor A F) A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
x : Cᵒᵖ
w :
  Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop x))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj (Opposite.unop x))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F)
          (NatTrans.app (Iso.hom (shiftFunctorZero (OppositeShift.{v_1, u_1, u_3} C A) A)) x) ≫
        NatTrans.app (Iso.inv (shiftFunctorZero (OppositeShift.{v_2, u_2, u_3} D A) A))
          (obj (OppositeShift.functor A F) x) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} (OppositeShift.{v_1, u_1, u_3} C A) (A := A) 0) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} (OppositeShift.{v_2, u_2, u_3} D A) (A := A) 0)
          (obj (OppositeShift.functor A F) x)))
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F).op.obj x ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0).op.obj x)
    (NatTrans.app (Iso.hom (Iso.symm (NatIso.op (CommShift.isoZero F A)))) x)
    (NatTrans.app (Iso.hom (CommShift.isoZero (OppositeShift.functor A F) A)) x)

Tactic:
simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app,
      CommShift.isoZero_inv_app, op_comp, CommShift.isoZero_hom_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.op_comp, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Iso.symm_hom, CategoryTheory.NatTrans.op_app, CategoryTheory.Functor.CommShift.isoZero_inv_app, CategoryTheory.NatIso.op_inv, CategoryTheory.Functor.op_obj
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
x : Cᵒᵖ
w :
  Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop x))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj (Opposite.unop x))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F) (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop x))) ≫
        Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (Opposite.unop (obj (OppositeShift.functor A F) x))) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} (OppositeShift.{v_1, u_1, u_3} C A) (A := A) 0) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} (OppositeShift.{v_2, u_2, u_3} D A) (A := A) 0)
          (obj (OppositeShift.functor A F) x)))
⊢ Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop x))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj (Opposite.unop x))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F)
          (NatTrans.app (Iso.hom (shiftFunctorZero (OppositeShift.{v_1, u_1, u_3} C A) A)) x) ≫
        NatTrans.app (Iso.inv (shiftFunctorZero (OppositeShift.{v_2, u_2, u_3} D A) A))
          (obj (OppositeShift.functor A F) x) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} (OppositeShift.{v_1, u_1, u_3} C A) (A := A) 0) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} (OppositeShift.{v_2, u_2, u_3} D A) (A := A) 0)
          (obj (OppositeShift.functor A F) x)))

Tactic:
erw [oppositeShiftFunctorZero_inv_app, oppositeShiftFunctorZero_hom_app]

Premises used: CategoryTheory.oppositeShiftFunctorZero_inv_app, CategoryTheory.oppositeShiftFunctorZero_hom_app
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
x : Cᵒᵖ
⊢ Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop x))) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (F.obj (Opposite.unop x))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F) (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop x))) ≫
        Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (Opposite.unop (obj (OppositeShift.functor A F) x))) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} (OppositeShift.{v_1, u_1, u_3} C A) (A := A) 0) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} (OppositeShift.{v_2, u_2, u_3} D A) (A := A) 0)
          (obj (OppositeShift.functor A F) x)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
a b : A
rw :
  Eq (α :=
    Iso (C := Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b) ⋙ OppositeShift.functor A F)
      (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b)))
    (Iso.symm (NatIso.op (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))))
    (CommShift.isoAdd (Iso.symm (NatIso.op (commShiftIso F a))) (Iso.symm (NatIso.op (commShiftIso F b))))
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b) ⋙ OppositeShift.functor A F)
      (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b)))
    (Iso.symm (NatIso.op (commShiftIso F (a + b))))
    (CommShift.isoAdd (Iso.symm (NatIso.op (commShiftIso F a))) (Iso.symm (NatIso.op (commShiftIso F b))))

Tactic:
rw [commShiftIso_add]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_add
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
a b : A
w :
  ∀ (x : Cᵒᵖ),
    Eq (α := (shiftFunctor C (a + b) ⋙ F).op.obj x ⟶ (F ⋙ shiftFunctor D (a + b)).op.obj x)
      (NatTrans.app (Iso.hom (Iso.symm (NatIso.op (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))))) x)
      (NatTrans.app
        (Iso.hom (CommShift.isoAdd (Iso.symm (NatIso.op (commShiftIso F a))) (Iso.symm (NatIso.op (commShiftIso F b)))))
        x)
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b) ⋙ OppositeShift.functor A F)
      (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b)))
    (Iso.symm (NatIso.op (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))))
    (CommShift.isoAdd (Iso.symm (NatIso.op (commShiftIso F a))) (Iso.symm (NatIso.op (commShiftIso F b))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
a b : A
x : Cᵒᵖ
⊢ Eq (α :=
    Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
      Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (Quiver.Hom.op (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
              (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x)))))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Opposite.unop x))))
          (Quiver.Hom.op (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj (Opposite.unop x)))) :
      Opposite.op (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop x))) ⟶
        Opposite.op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj (Opposite.unop x))))
    (map (OppositeShift.functor A F)
          (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop x))) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
            (obj (OppositeShift.functor A F)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x)))
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (commShiftIso F b))
              (Opposite.unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a) x))))
          (map (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) b)
              (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F a)) (Opposite.unop x))) ≫
            Quiver.Hom.op
              (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (Opposite.unop (obj (OppositeShift.functor A F) x)))) :
      Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A)
        (obj (OppositeShift.functor A F)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) (a + b)) x))
        (obj.{v_2, v_2, u_2, u_2} (shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) (a + b))
          (obj (OppositeShift.functor A F) x)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift A
a : A
⊢ Eq (α :=
    Iso (C := Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
      (shiftFunctor (OppositeShift.{v_1, u_1, u_3} C A) a ⋙ OppositeShift.functor A F)
      (OppositeShift.functor A F ⋙ shiftFunctor (OppositeShift.{v_2, u_2, u_3} D A) a))
    (commShiftIso (OppositeShift.functor A F) a) (Iso.symm (NatIso.op (commShiftIso F a)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
rw :
  Eq (α := shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0)
    (NatIso.removeOp (Iso.symm (CommShift.isoZero (OppositeShift.functor A F) A))) (CommShift.isoZero F A)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0)
    (NatIso.removeOp (Iso.symm (commShiftIso (OppositeShift.functor A F) 0))) (CommShift.isoZero F A)

Tactic:
rw [commShiftIso_zero]

Premises used: CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
w :
  ∀ (x : C),
    Eq (α :=
      (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F).obj x ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0).obj x)
      (NatTrans.app (Iso.hom (NatIso.removeOp (Iso.symm (CommShift.isoZero (OppositeShift.functor A F) A)))) x)
      (NatTrans.app (Iso.hom (CommShift.isoZero F A)) x)
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0)
    (NatIso.removeOp (Iso.symm (CommShift.isoZero (OppositeShift.functor A F) A))) (CommShift.isoZero F A)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
x : C
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (obj
            (OppositeShift.functor A F :
              Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
            (Opposite.op x)))
        (Quiver.Hom.unop
          (map (OppositeShift.functor A F) (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ A)) (Opposite.op x))))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.hom (shiftFunctorZero Dᵒᵖ A))
            (obj
              (OppositeShift.functor A F :
                Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
              (Opposite.op x)))) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) x) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj x) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0 ⋙ F).obj x ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_3} D (A := A) 0).obj x)
    (NatTrans.app (Iso.hom (NatIso.removeOp (Iso.symm (CommShift.isoZero (OppositeShift.functor A F) A)))) x)
    (NatTrans.app (Iso.hom (CommShift.isoZero F A)) x)

Tactic:
simp only [comp_obj, NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app, op_obj,
      CommShift.isoZero_inv_app, unop_comp, CommShift.isoZero_hom_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Iso.symm_hom, CategoryTheory.unop_comp, CategoryTheory.Functor.CommShift.isoZero_inv_app, CategoryTheory.NatIso.removeOp_hom, CategoryTheory.NatTrans.removeOp_app, CategoryTheory.Functor.op_obj
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 :
  CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (D := OppositeShift.{v_2, u_2, u_3} D A)
    (OppositeShift.functor A F) A
x : C
w :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (Quiver.Hom.unop
          (map (OppositeShift.functor A F)
            (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C A)) (Opposite.unop (Opposite.op x))))) ≫
        Quiver.Hom.unop
          (Quiver.Hom.op
            (NatTrans.app (Iso.inv (shiftFunctorZero D A))
              (Opposite.unop
                (obj
                  (OppositeShift.functor A F :
                    Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A)
                      (OppositeShift.{v_2, u_2, u_3} D A))
                  (Opposite.op x))))) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) x) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj x) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (obj
            (OppositeShift.functor A F :
              Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
            (Opposite.op x)))
        (Quiver.Hom.unop
          (map (OppositeShift.functor A F) (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ A)) (Opposite.op x))))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.hom (shiftFunctorZero Dᵒᵖ A))
            (obj
              (OppositeShift.functor A F :
                Functor.{v_1, v_2, u_1, u_2} (OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.{v_2, u_2, u_3} D A))
              (Opposite.op x)))) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) x) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj x) :
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) x) ⟶
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_3} D (A := A) 0) (F.obj x))

Tactic:
erw [oppositeShiftFunctorZero_hom_app, oppositeShiftFunctorZero_inv_app]

Premises used: CategoryTheory.oppositeShiftFunctorZero_inv_app, CategoryTheory.oppositeShiftFunctorZero_hom_app