awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
a : A
X : C
⊢ Eq (α :=
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
        (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
have a₁ : Eq (α :=
  F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
  (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
    CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-a))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a sorry))
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))))
        (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-a) a sorry))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))))
  (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
Tactic: rw [shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app_assoc,
    Functor.commShiftIso_hom_naturality_assoc, ← Functor.map_comp,
    left_triangle_components, Functor.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
a : A
X : C
a₁ :
  Eq (α :=
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
        (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-a))
              (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))))
          (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))))
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-a) a ⋯))
              (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
⊢ Eq (α :=
    F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X))))
        (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)))
        (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D (-a) a ⋯))
            (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj (G.obj (F.obj X)))) ≫
          Functor.map (shiftFunctor D a)
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D a (-a) ⋯)) (F.obj (G.obj (F.obj X)))) ≫
            Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X))))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
have a₂ : Eq (α :=
  F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))
  (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj (F.obj X)) ≫
      Functor.map (shiftFunctor D a) (adj.counit.app (F.obj X)))
  (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
Tactic: rw [shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_id_app_assoc,
    Functor.commShiftIso_hom_naturality_assoc, ← Functor.map_comp,
    left_triangle_components, Functor.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
⊢ Eq (α := shiftFunctor.{v_2, u_2, u_3} D (A := A) 0 ⋙ G ≅ G ⋙ shiftFunctor.{v_1, u_1, u_3} C (A := A) 0) (iso adj 0)
    (Functor.CommShift.isoZero G A)
have refine : CommShift.CompatibilityUnit adj (Functor.commShiftIso F 0) (Functor.CommShift.isoZero G A)
Tactic: refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso 0) _ _
      (compatibilityUnit_iso adj 0) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.commShiftIso F 0) (Functor.CommShift.isoZero G A)
have rw : CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)
Tactic: rw [F.commShiftIso_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
a b : A
⊢ Eq (α := shiftFunctor D (a + b) ⋙ G ≅ G ⋙ shiftFunctor C (a + b)) (iso adj (a + b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
have refine : CommShift.CompatibilityUnit adj (Functor.commShiftIso F (a + b)) (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
Tactic: refine CommShift.compatibilityUnit_unique_right adj (F.commShiftIso (a + b)) _ _
      (compatibilityUnit_iso adj (a + b)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.commShiftIso F (a + b)) (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
have rw : CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (Functor.commShiftIso F a) (Functor.commShiftIso F b))
  (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
Tactic: rw [F.commShiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
this : G.CommShift A := adj.rightAdjointCommShift A
⊢ adj.CommShift A
have refine : ∀ (a : A),
  Eq (α := shiftFunctor C a ⋙ 𝟭 C ⟶ (F ⋙ G) ⋙ shiftFunctor C a)
    (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a))
    (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a))
Tactic: refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : F.CommShift A
this : G.CommShift A := adj.rightAdjointCommShift A
a : A
X : C
⊢ Eq (α := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ 𝟭 C) X ⟶ ((F ⋙ G) ⋙ shiftFunctor C a).obj X)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)) X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X)
have w : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
  (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a)) X ≫ Functor.map (shiftFunctor C a) (adj.unit.app X) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
  (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
a b : A
h : a + b = 0
inst_5 : G.CommShift A
X : C
⊢ Eq (α := (shiftFunctor C a ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D a).obj X) (NatTrans.app (Iso.hom (iso adj a)) X)
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map
          (Functor.map (shiftFunctor C a) (G.map (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a b h)) (F.obj X)))) ≫
        F.map
            (Functor.map (shiftFunctor C a)
              (NatTrans.app (Iso.hom (Functor.commShiftIso G b))
                (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
          F.map
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C b a ⋯))
                (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
            adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
have obtain : ∀ (h : a + -a = 0),
  Eq (α := (shiftFunctor C a ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D a).obj X) (NatTrans.app (Iso.hom (iso adj a)) X)
    (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      F.map
          (Functor.map (shiftFunctor C a)
            (G.map (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a (-a) h)) (F.obj X)))) ≫
        F.map
            (Functor.map (shiftFunctor C a)
              (NatTrans.app (Iso.hom (Functor.commShiftIso G (-a)))
                (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
          F.map
              (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-a) a sorry))
                (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
            adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
Tactic: obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
a : A
X : C
⊢ 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) X) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj X))
    (Functor.map (shiftFunctor C a) (adj.unit.app X))
    (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor D a).obj X)) (G.map (NatTrans.app (Iso.hom (iso adj a)) X))
        (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))
have rw : 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) X) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) ((F ⋙ G).obj X))
  (Functor.map (shiftFunctor C a) (adj.unit.app X))
  (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
    CategoryStruct.comp (Y := G.obj ((F ⋙ shiftFunctor D a).obj X))
      (G.map
        (F.map (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
          F.map
              (Functor.map (shiftFunctor C a)
                (G.map (NatTrans.app (Iso.inv (shiftFunctorCompIsoId D a (-a) sorry)) (F.obj X)))) ≫
            F.map
                (Functor.map (shiftFunctor C a)
                  (NatTrans.app (Iso.hom (Functor.commShiftIso G (-a)))
                    (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
              F.map
                  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-a) a sorry))
                    (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
                adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
      (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))
Tactic: rw [LeftAdjointCommShift.iso_hom_app adj _ _ (add_neg_cancel a)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
a : A
X : C
| CategoryStruct.comp (Y :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
      (G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-a))
          (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))))
    (Functor.map (shiftFunctor C a)
      (NatTrans.app (Iso.inv (Functor.commShiftIso G (-a)))
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
    (Functor.map (shiftFunctor C a)
      (NatTrans.app (Iso.hom (Functor.commShiftIso G (-a)))
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
have a₁ : Functor.map (shiftFunctor C a)
  (𝟙 ((G ⋙ shiftFunctor C (-a)).obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
Tactic: rw [← Functor.map_comp, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
a : A
X : C
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
    (Functor.map (shiftFunctor C a) (adj.unit.app X))
    (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫
      Functor.map (shiftFunctor C a) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C a (-a) ⋯)) (G.obj (F.obj X))) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
              (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))))
          (Functor.map (shiftFunctor C a)
            (Functor.map (shiftFunctor C (-a)) (NatTrans.app (Iso.inv (Functor.commShiftIso G a)) (F.obj X))))
          (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-a) a ⋯))
              (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X)))
have rw : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
  (Functor.map (shiftFunctor C a) (adj.unit.app X))
  (Functor.map (shiftFunctor C a) (adj.unit.app X) ≫
    CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-a))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))))
      (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-a) a sorry))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
      (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C (-a) a sorry))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C)
            (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
          (Functor.map (𝟭 C) (NatTrans.app (Iso.inv (Functor.commShiftIso G a)) (F.obj X)))
          (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) (F.obj X))))
Tactic: rw [shift_shiftFunctorCompIsoId_inv_app, ← Functor.comp_map,
    (shiftFunctorCompIsoId C _ _ (neg_add_cancel a)).hom.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift 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) (iso adj 0)
    (Functor.CommShift.isoZero F A)
have refine : CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.commShiftIso G 0)
Tactic: refine CommShift.compatibilityUnit_unique_left adj _ _ (G.commShiftIso 0)
      (compatibilityUnit_iso adj 0) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.commShiftIso G 0)
have rw : CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)
Tactic: rw [G.commShiftIso_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
a b : A
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (iso adj (a + b))
    (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
have refine : CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b)) (Functor.commShiftIso G (a + b))
Tactic: refine CommShift.compatibilityUnit_unique_left adj _ _ (G.commShiftIso (a + b))
      (compatibilityUnit_iso adj (a + b)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
a b : A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b)) (Functor.commShiftIso G (a + b))
have rw : CommShift.CompatibilityUnit adj (Functor.CommShift.isoAdd (iso adj a) (iso adj b))
  (Functor.CommShift.isoAdd (Functor.commShiftIso G a) (Functor.commShiftIso G b))
Tactic: rw [G.commShiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
⊢ adj.CommShift A
have refine : ∀ (a : A),
  Eq (α := shiftFunctor C a ⋙ 𝟭 C ⟶ (F ⋙ G) ⋙ shiftFunctor C a)
    (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a))
    (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a))
Tactic: refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
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 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
⊢ Eq (α := shiftFunctor C a ⋙ 𝟭 C ⟶ (F ⋙ G) ⋙ shiftFunctor C a)
    (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a))
    (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a))
have w : ∀ (X : C),
  Eq (α := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ 𝟭 C) X ⟶ ((F ⋙ G) ⋙ shiftFunctor C a).obj X)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)) X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X)
Tactic: ext X