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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
              G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X)) ≫
                f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
                  Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                    NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
have slice_rhs : Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
          ((G.map (𝟙 (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))) ≫
                f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
              Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X))) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
Tactic: slice_rhs 5 6 => rw [← G.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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            ((G.map (𝟙 (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a ⋙ shiftFunctor D b) (F.obj X))) ≫
                  f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
                Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X))) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
have simp : Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
          f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
            Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
Tactic: simp only [Functor.comp_obj, Functor.map_id, id_comp, 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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          G.map (Functor.map (shiftFunctor D b) (e₁.hom.app X)) ≫
            f₂.hom.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
have erw : Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
            Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
Tactic: erw [f₂.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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      adj.unit.app
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          f₂.hom.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
              Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) (G.obj (F.obj X))
have rw : Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
        Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
          𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) (G.obj (F.obj X)))
Tactic: rw [← reassoc_of% this, ← cancel_mono ((shiftFunctorAdd C a b).hom.app _),
    assoc, assoc, assoc, assoc, assoc, assoc, Iso.inv_hom_id_app_assoc, 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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
          Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
            𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) (G.obj (F.obj X)))
have dsimp : Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      Functor.map (shiftFunctor C b) (G.map (e₁.hom.app X)) ≫
        Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
          𝟙
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
              (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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ Functor.map (shiftFunctor C (a + b)) (adj.unit.app X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) (G.obj (F.obj X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        Functor.map (shiftFunctor C b) (G.map (e₁.hom.app X)) ≫
          Functor.map (shiftFunctor C b) (e₂.hom.app (F.obj X)) ≫
            𝟙
              (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
have rw : NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫ Functor.map (shiftFunctor C a ⋙ shiftFunctor C b) (adj.unit.app X) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      𝟙
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
Tactic: rw [← (shiftFunctor C b).map_comp_assoc, ← (shiftFunctor C b).map_comp_assoc,
    assoc, ← h X, NatTrans.naturality]
-- 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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C a ⋙ shiftFunctor C b) (adj.unit.app X) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
        𝟙
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
have dsimp : NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) =
  NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
      𝟙
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
          (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 : 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 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 :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ⟶
      G.obj
        (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))))
    (Functor.map (shiftFunctor C b) (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      f₂.inv.app (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
    (adj.unit.app
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      G.map (f₁.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) =
    NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
      Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)) ≫
        𝟙
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
have rw : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X))))
  (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫
    Functor.map (shiftFunctor C b) (Functor.map (shiftFunctor C a) (adj.unit.app X)))
Tactic: rw [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 : AddMonoid 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
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
⊢ Eq (α := shiftFunctor D a ⋙ G ⋙ F ⟶ 𝟭 D ⋙ shiftFunctor D a)
    (Iso.hom (Functor.commShiftIso (G ⋙ F) a) ≫ Functor.whiskerRight adj.counit (shiftFunctor D a))
    (Functor.whiskerLeft (shiftFunctor D a) adj.counit ≫ Iso.hom (Functor.commShiftIso (𝟭 D) a))
have w : ∀ (x : D),
  Eq (α := (shiftFunctor D a ⋙ G ⋙ F).obj x ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D ⋙ shiftFunctor D a) x)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a) ≫ Functor.whiskerRight adj.counit (shiftFunctor D a)) x)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor D a) adj.counit ≫ Iso.hom (Functor.commShiftIso (𝟭 D) a)) x)
Tactic: ext
-- 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 : AddMonoid 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
inst_6 : G.CommShift A
h : NatTrans.CommShift adj.unit A
a : A
x : D
⊢ Eq (α := (shiftFunctor D a ⋙ G ⋙ F).obj x ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (𝟭 D ⋙ shiftFunctor D a) x)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (G ⋙ F) a) ≫ Functor.whiskerRight adj.counit (shiftFunctor D a)) x)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor D a) adj.counit ≫ Iso.hom (Functor.commShiftIso (𝟭 D) a)) x)
have w : Eq (α :=
  F.obj (G.obj (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)) ⟶
    Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x)
  (CategoryStruct.comp (Y := F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj x)))
    (F.map (NatTrans.app (Iso.hom (Functor.commShiftIso G a)) x))
    (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (G.obj x) ≫ Functor.map (shiftFunctor D a) (adj.counit.app x)))
  (adj.counit.app (Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) x))
Tactic: simp only [Functor.comp_obj, Functor.id_obj, NatTrans.comp_app,
      Functor.commShiftIso_comp_hom_app, Functor.whiskerRight_app, assoc, Functor.whiskerLeft_app,
      Functor.commShiftIso_id_hom_app, comp_id]