awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift (W₁ := W₁) (W₂ := W₂) M L₁ L₂ G e
m : M
⊢ Eq (α := shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ⟶ (L₁ ⋙ G) ⋙ shiftFunctor D₂ m)
    (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) m) ≫
      Functor.whiskerRight e.hom (shiftFunctor D₂ m))
    (Functor.whiskerLeft (shiftFunctor C₁ m) e.hom ≫ Iso.hom (Functor.commShiftIso (L₁ ⋙ G) m))
have w : ∀ (X : C₁),
  Eq (α := (shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj X ⟶ ((L₁ ⋙ G) ⋙ shiftFunctor D₂ m).obj X)
    (NatTrans.app
      (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) m) ≫
        Functor.whiskerRight e.hom (shiftFunctor D₂ m))
      X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C₁ m) e.hom ≫ Iso.hom (Functor.commShiftIso (L₁ ⋙ G) m)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
inst_3 : Preadditive.{v_1, u_1} C
n : A
inst_4 : Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (C := OppositeShift.{v_1, u_1, u_2} C A)
    (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) n)
have change : Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.op (shiftFunctor C n))
Tactic: change (shiftFunctor C n).op.Additive
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (OppositeShift.{v_1, u_1, u_2} C A) (A := A) 0) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (OppositeShift.{v_1, u_1, u_2} C A)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero (OppositeShift.{v_1, u_1, u_2} C A) A)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (Opposite.unop X)))
have rw : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (OppositeShift.{v_1, u_1, u_2} C A) (A := A) 0) X) =
  𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} C (A := A) 0) (Opposite.unop X)))
Tactic: rw [← cancel_mono ((shiftFunctorZero (OppositeShift C A) A).inv.app X),
    Iso.hom_inv_id_app, oppositeShiftFunctorZero_inv_app, ← op_comp,
    Iso.hom_inv_id_app, op_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b : A
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) (a + b)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) a ⋙ shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) b) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd (OppositeShift.{v_1, u_1, u_2} C A) a b)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (Opposite.unop X)))
have rw : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, u_2} C A) (a + b)) X) =
  𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) (Opposite.unop X)))
Tactic: rw [← cancel_mono ((shiftFunctorAdd (OppositeShift C A) a b).inv.app X),
    Iso.hom_inv_id_app, oppositeShiftFunctorAdd_inv_app, ← op_comp,
    Iso.hom_inv_id_app, op_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b c : A
h : a + b = c
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b c h)) X =
    Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b c h)) (Opposite.unop X))
have subst : NatTrans.app (Iso.inv (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b (a + b) sorry)) X =
  Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) sorry)) (Opposite.unop X))
Tactic: subst h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
inst_1 : AddMonoid A
inst_2 : HasShift.{v_1, u_1, u_2} C A
X : OppositeShift.{v_1, u_1, u_2} C A
a b c : A
h : a + b = c
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b c h)) X =
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b c h)) (Opposite.unop X))
have subst : NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, u_2} C A) a b (a + b) sorry)) X =
  Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b (a + b) sorry)) (Opposite.unop X))
Tactic: subst h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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
⊢ 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)
have 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)
Tactic: rw [commShiftIso_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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 (α :=
    (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)
have 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)))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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)
          (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)))
have 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)))
Tactic: erw [oppositeShiftFunctorZero_inv_app, oppositeShiftFunctorZero_hom_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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
⊢ 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))))
have 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))))
Tactic: rw [commShiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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
⊢ 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))))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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 (α := (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)
have w : 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)
        (NatTrans.app (Iso.hom (shiftFunctorAdd (OppositeShift.{v_1, u_1, u_3} C A) a b)) 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))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd (OppositeShift.{v_2, u_2, u_3} D A) a b))
            (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: simp only [op_obj, comp_obj, Iso.symm_hom, NatIso.op_inv, NatTrans.op_app,
      CommShift.isoAdd_inv_app, op_comp, Category.assoc, CommShift.isoAdd_hom_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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
⊢ 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)
have 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)
Tactic: rw [commShiftIso_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (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
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
⊢ 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)
have 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))
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]