awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.left.{v, u} (Arrow.mk f.op)) (Arrow.right.{v, u} (Arrow.mk g.op)))
    ((Arrow.Hom.right h.r).op ≫ Arrow.hom (Arrow.mk g.op)) (Arrow.hom (Arrow.mk f.op) ≫ (Arrow.Hom.left h.r).op)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.left.{v, u} (Arrow.mk g.op)) (Arrow.right.{v, u} (Arrow.mk f.op)))
    ((Arrow.Hom.right h.i).op ≫ Arrow.hom (Arrow.mk f.op)) (Arrow.hom (Arrow.mk g.op) ≫ (Arrow.Hom.left h.i).op)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
h₁ :
  Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.left.{v, u} (Arrow.mk f.op)) (Arrow.left.{v, u} (Arrow.mk f.op)))
    (Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯)))
    (Arrow.Hom.left (𝟙 (Arrow.mk f.op)))
h₂ :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.right.{v, u} (Arrow.mk f.op)) (Arrow.right.{v, u} (Arrow.mk f.op)))
    (Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯)))
    (Arrow.Hom.right (𝟙 (Arrow.mk f.op)))
⊢ Eq.{v + 1} (α := Quiver.Hom (V := Arrow.{v, u} Cᵒᵖ) (Arrow.mk f.op) (Arrow.mk f.op))
    (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
      (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯))
    (𝟙 (Arrow.mk f.op))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Eq.{v + 1} (α := Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.left.{v, u} (Arrow.mk f.op)) (Arrow.left.{v, u} (Arrow.mk f.op)))
    (Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯)))
    (Arrow.Hom.left (𝟙 (Arrow.mk f.op)))

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := Cᵒᵖ) (Arrow.right.{v, u} (Arrow.mk f.op)) (Arrow.right.{v, u} (Arrow.mk f.op)))
    (Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk g.op) (Arrow.homMk (Arrow.Hom.right h.r).op (Arrow.Hom.left h.r).op ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).op (Arrow.Hom.left h.i).op ⋯)))
    (Arrow.Hom.right (𝟙 (Arrow.mk f.op)))

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y_1 Z_1 W_1 : C
f_1 : X_1 ⟶ Y_1
g_1 : Z_1 ⟶ W_1
h_1 : RetractArrow f_1 g_1
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) (W := W) f g
⊢ (Arrow.Hom.right h.r).unop ≫ (Arrow.mk g.unop).hom = (Arrow.mk f.unop).hom ≫ (Arrow.Hom.left h.r).unop

Tactic:
simp [← unop_comp]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y_1 Z_1 W_1 : C
f_1 : X_1 ⟶ Y_1
g_1 : Z_1 ⟶ W_1
h_1 : RetractArrow f_1 g_1
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) (W := W) f g
⊢ (Arrow.Hom.right h.i).unop ≫ (Arrow.mk f.unop).hom = (Arrow.mk g.unop).hom ≫ (Arrow.Hom.left h.i).unop

Tactic:
simp [← unop_comp]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y_1 Z_1 W_1 : C
f_1 : X_1 ⟶ Y_1
g_1 : Z_1 ⟶ W_1
h_1 : RetractArrow f_1 g_1
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) (W := W) f g
h₁ :
  Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk f.unop))
h₂ :
  Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯)) =
    Arrow.Hom.right (𝟙 (Arrow.mk f.unop))
⊢ CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
      (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯) =
    𝟙 (Arrow.mk f.unop)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y_1 Z_1 W_1 : C
f_1 : X_1 ⟶ Y_1
g_1 : Z_1 ⟶ W_1
h_1 : RetractArrow f_1 g_1
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) (W := W) f g
⊢ Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk f.unop))

Tactic:
simp [← unop_comp]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X_1 Y_1 Z_1 W_1 : C
f_1 : X_1 ⟶ Y_1
g_1 : Z_1 ⟶ W_1
h_1 : RetractArrow f_1 g_1
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow.{v, u} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Z) (W := W) f g
⊢ Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk g.unop) (Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯)
        (Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯)) =
    Arrow.Hom.right (𝟙 (Arrow.mk f.unop))

Tactic:
simp [← unop_comp]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ F.map h.i ≫ (Arrow.mk (τ.app Y)).hom = (Arrow.mk (τ.app X)).hom ≫ G.map h.i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ F.map h.r ≫ (Arrow.mk (τ.app X)).hom = (Arrow.mk (τ.app Y)).hom ≫ G.map h.r

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
τ : F ⟶ G
X Y : C
h : Retract X Y
h₁ :
  Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
        (Arrow.homMk (F.map h.r) (G.map h.r) ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk (τ.app X)))
h₂ :
  Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
        (Arrow.homMk (F.map h.r) (G.map h.r) ⋯)) =
    Arrow.Hom.right (𝟙 (Arrow.mk (τ.app X)))
⊢ CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
      (Arrow.homMk (F.map h.r) (G.map h.r) ⋯) =
    𝟙 (Arrow.mk (τ.app X))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
        (Arrow.homMk (F.map h.r) (G.map h.r) ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk (τ.app X)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Retract
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
τ : F ⟶ G
X Y : C
h : Retract X Y
⊢ Arrow.Hom.right
      (CategoryStruct.comp (Y := Arrow.mk (τ.app Y)) (Arrow.homMk (F.map h.i) (G.map h.i) ⋯)
        (Arrow.homMk (F.map h.r) (G.map h.r) ⋯)) =
    Arrow.Hom.right (𝟙 (Arrow.mk (τ.app X)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ e₂.hom.app (F.obj (G.obj Y)))

Tactic:
have eq := h (G.obj Y)
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ e₂.hom.app (F.obj (G.obj Y)))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))

Tactic:
simp only [← cancel_mono (e₂.inv.app _ ≫ G.map (e₁.inv.app _)),
    assoc, Iso.hom_inv_id_app_assoc, comp_id, ← Functor.map_comp,
    Iso.hom_inv_id_app, Functor.comp_obj, Functor.map_id] at eq

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
a₁ :
  adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))
⊢ adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
          e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y))) ≫
        G.map (e₁.hom.app (G.obj Y) ≫ Functor.map (shiftFunctor D a) (adj.counit.app Y))

Tactic:
simp only [assoc, ← Functor.map_comp, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app_assoc
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
a₁ :
  adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app Y
⊢ adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))

Tactic:
erw [← e₂.inv.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
a₁ :
  adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        Functor.map (shiftFunctor C a) (G.map (adj.counit.app Y)) ≫ e₂.inv.app Y
⊢ adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app Y

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      G.obj (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y))))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)))
⊢ adj.unit.app (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) ≫
      G.map (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) Y)) =
    e₂.hom.app Y ≫
      Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
        Functor.map (shiftFunctor C a) (G.map (adj.counit.app Y)) ≫ e₂.inv.app Y

Tactic:
simp only [right_triangle_components, ← Functor.map_comp_assoc, Functor.map_id, id_comp,
    Iso.hom_inv_id_app, Functor.comp_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ e₂.hom.app (F.obj (G.obj Y)))

Tactic:
have := h (G.obj Y)
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ e₂.hom.app (F.obj (G.obj Y)))
⊢ Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))

Tactic:
rw [← cancel_mono (e₂.inv.app _), assoc, assoc, Iso.hom_inv_id_app] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))

Tactic:
erw [comp_id] at this

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Shift.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
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
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj Y)) ⟶
      (shiftFunctor D a ⋙ G).obj (F.obj (G.obj Y)))
    (Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)))
rw :
  e₂.inv.app Y =
    Functor.map (shiftFunctor C a) (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))
⊢ e₂.inv.app Y =
    adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ G.map (Functor.map (shiftFunctor D a) (adj.counit.app Y))

Tactic:
rw [← assoc, ← this, assoc]

Premises used: CategoryTheory.Category.assoc