mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₃ = (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₃ = -a₃
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝ : PullbackShift C φ
⊢ (isoWhiskerRight (pullbackShiftIso C φ 0 (φ 0) ⋯) F ≪≫
            commShiftIso F (φ 0) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ 0 (φ 0) ⋯).symm).hom.app
      x✝ =
    (CommShift.isoZero (PullbackShift.functor φ F) A).hom.app x✝

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ 0)).hom.app x✝ ≫ (pullbackShiftIso D φ 0 (φ 0) ⋯).inv.app (F.obj x✝) =
    (CommShift.isoZero (PullbackShift.functor φ F) A).hom.app x✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map
              ((𝟙 ((shiftFunctor C (-m)).obj (Opposite.unop ((shiftFunctor C (-n)).op.obj X)))).op ≫
                  ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op).unop).op

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map
              ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X) ≫
                𝟙 ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X))))).op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)) ≫
        (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X))) ≫
          (shiftFunctor C n).map
              ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X))) ≫
            (shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
          ((shiftFunctor C n).map
              ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op) ≫
        ((shiftFunctorAdd' C m n p h).hom.app
            ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op) ≫
      ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
          (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
            𝟙 ((shiftFunctor C a ⋙ shiftFunctor C b).obj (G.obj (F.obj X)))

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor C b).map (G.map (e₁.hom.app X)) ≫
          (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫
            𝟙 ((shiftFunctor C b).obj ((shiftFunctor C a).obj (G.obj (F.obj X))))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ (𝟙 (((opShiftFunctorEquivalence C p).functor ⋙ (opShiftFunctorEquivalence C p).inverse).obj X)).unop =
    (((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op ≫
        ((shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m).obj X))).op ≫
          ((shiftFunctor C n).map
                ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
            ((shiftFunctor C n).map
                  ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop).op ≫
              ((shiftFunctorAdd' C m n p h).hom.app
                    (Opposite.unop ((opShiftFunctorEquivalence C m).functor.obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
                ((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op).unop

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X))) =
    (((((shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop ≫
              (shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))) ≫
            (shiftFunctor C n).map
              ((opShiftFunctorEquivalence C m).unitIso.hom.app ((shiftFunctor Cᵒᵖ n).obj X)).unop) ≫
          (shiftFunctor C n).map ((opShiftFunctorEquivalence C m).unitIso.inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop) ≫
        (shiftFunctorAdd' C m n p h).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))) ≫
      (shiftFunctor C p).map ((shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctorAdd C a b).hom.app X ≫ (shiftFunctor C a ⋙ shiftFunctor C b).map (adj.unit.app X) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map ((shiftFunctor C a).map (adj.unit.app X)) ≫
        𝟙 ((shiftFunctor C b).obj ((shiftFunctor C a).obj (G.obj (F.obj X))))

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctorAdd C a b).hom.app X ≫ (shiftFunctor C b).map ((shiftFunctor C a).map (adj.unit.app X)) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map ((shiftFunctor C a).map (adj.unit.app X)) ≫
        𝟙 ((shiftFunctor C b).obj ((shiftFunctor C a).obj (G.obj (F.obj X))))
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.op z ≫ f).unop) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f ≫ z)) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop).op ≫
          ((shiftFunctorAdd' C a b c ⋯).inv.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X)))).op ≫
            ((shiftFunctor C b).map
                  ((opShiftFunctorEquivalence C a).unitIso.inv.app
                      ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop).op ≫
              (opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C c).map
        (f ≫ (shiftFunctor Cᵒᵖ a).map g ≫ (shiftFunctorAdd' Cᵒᵖ b a c h).inv.app (Opposite.op X)).unop =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ (((((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
            (shiftFunctor C b).map
              ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop) ≫
          (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))))) ≫
        (shiftFunctor C c).map ((shiftFunctorAdd' Cᵒᵖ b a c ⋯).hom.app (Opposite.op X)).unop) ≫
      (shiftFunctor C c).map
        ((((shiftFunctorAdd' Cᵒᵖ b a c h).inv.app (Opposite.op X)).unop ≫ ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
          Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
          (shiftFunctor C c).map
            ((𝟙 ((shiftFunctor Cᵒᵖ b ⋙ shiftFunctor Cᵒᵖ a).obj (Opposite.op X))).unop ≫
              ((shiftFunctor Cᵒᵖ a).map g).unop ≫ Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app
            (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
          (shiftFunctor C c).map
            (𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ a).obj ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X)))) ≫
              ((shiftFunctor Cᵒᵖ a).map g).unop ≫ Quiver.Hom.unop f) =
    (((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C b).map (Quiver.Hom.unop g)) ≫
      (shiftFunctor C b).map ((opEquiv a).symm f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map ((shiftFunctor Cᵒᵖ a).map g).unop ≫
          (shiftFunctor C a ⋙ shiftFunctor C b).map (Quiver.Hom.unop f) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map (Quiver.Hom.unop g) ≫
        (shiftFunctor C b).map
            (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
              (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
          (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
        (shiftFunctor C b).map ((shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
          (shiftFunctor C b).map ((shiftFunctor C a).map (Quiver.Hom.unop f)) ≫ (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map (Quiver.Hom.unop g) ≫
        (shiftFunctor C b).map
            (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
              (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
          (shiftFunctorAdd' C a b c ⋯).inv.app Z
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (adj.homEquiv ((shiftFunctor C a).obj ((𝟭 C).obj X✝)) ((shiftFunctor D a).obj (F.obj X✝))).symm
      ((shiftFunctor C a).map (adj.unit.app X✝) ≫
        adj.unit.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝))))) ≫
            G.map
                ((shiftFunctor D a).map
                  ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝))))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝))))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app (F.obj X✝)))) =
    (adj.homEquiv ((shiftFunctor C a).obj ((𝟭 C).obj X✝)) ((shiftFunctor D a).obj (F.obj X✝))).symm
      (adj.unit.app ((shiftFunctor C a).obj X✝) ≫
        G.map ((Functor.commShiftIso F a).hom.app X✝) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj X✝)))

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (adj.homEquiv ((shiftFunctor C a).obj X✝) ((shiftFunctor D a).obj (F.obj X✝))).symm
      ((shiftFunctor C a).map (adj.unit.app X✝) ≫
        adj.unit.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝))))) ≫
            G.map
                ((shiftFunctor D a).map
                  ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝))))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝))))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app (F.obj X✝)))) =
    (adj.homEquiv ((shiftFunctor C a).obj X✝) ((shiftFunctor D a).obj (F.obj X✝))).symm
      (adj.unit.app ((shiftFunctor C a).obj X✝) ≫
        G.map ((Functor.commShiftIso F a).hom.app X✝) ≫ 𝟙 (G.obj ((shiftFunctor D a).obj (F.obj X✝))))
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (𝟭 D).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝))) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ F.map ((shiftFunctor C a).map (adj.unit.app X✝)) ≫
      (Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝)) ≫
        (shiftFunctorCompIsoId D (-a) a ⋯).inv.app ((shiftFunctor D a).obj (F.obj (G.obj (F.obj X✝)))) ≫
          (shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝)))) ≫
            (shiftFunctor D a).map (adj.counit.app (F.obj X✝)) =
    (Functor.commShiftIso F a).hom.app X✝