awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift e.hom A
a : A
X : C
w :
  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))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₁ :
  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))
    (e.hom.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₂ :
  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))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫
      Functor.map (shiftFunctor D a) (e.hom.app X) ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
w₃ :
  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))
    (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (e.hom.app X ≫ e.inv.app X))
    (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))
    (app (Iso.hom (Functor.commShiftIso F₂ a)) X ≫ Functor.map (shiftFunctor D a) (e.inv.app X))
    (e.inv.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ app (Iso.hom (Functor.commShiftIso F₁ a)) X)
have w₄ : 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))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X ≫ Functor.map (shiftFunctor D a) (𝟙 (F₁.obj X)))
  (app (Iso.hom (Functor.commShiftIso F₁ a)) X)
Tactic: rw [← cancel_epi (e.hom.app (X⟦a⟧)), e.hom_inv_id_app_assoc, ← shift_app_comm_assoc,
    ← Functor.map_comp, e.hom_inv_id_app, Functor.map_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (hypothesis)
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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_5} C A
inst_4 : HasShift.{v_2, u_2, u_5} D A
inst_5 : F₁.CommShift A
inst_6 : F₂.CommShift A
inst_7 : IsIso τ
inst_8 : CommShift τ A
⊢ CommShift (inv τ) A
have this : CommShift (asIso τ).hom A
Tactic: haveI : NatTrans.CommShift (asIso τ).hom A := by assumption
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} J
F₁ F₂ F₃ : Functor.{v_1, v_2, u_1, u_2} C D
τ : F₁ ⟶ F₂
τ' : F₂ ⟶ F₃
e : F₁ ≅ F₂
G G' : Functor.{v_2, v_3, u_2, u_3} D E
τ'' : G ⟶ G'
H : Functor.{v_3, v_4, u_3, u_4} E J
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_1, u_1, u_5} C A
inst_6 : HasShift.{v_2, u_2, u_5} D A
inst_7 : HasShift.{v_3, u_3, u_5} E A
inst_8 : HasShift.{v_4, u_4, u_5} J A
inst_9 : F₁.CommShift A
inst_10 : F₂.CommShift A
inst_11 : F₃.CommShift A
inst_12 : G.CommShift A
inst_13 : G'.CommShift A
inst_14 : H.CommShift A
inst_15 : CommShift τ A
a : A
⊢ Eq (α := shiftFunctor C a ⋙ F₁ ⋙ G ⟶ (F₂ ⋙ G) ⋙ shiftFunctor E a)
    (Iso.hom (Functor.commShiftIso (F₁ ⋙ G) a) ≫ Functor.whiskerRight (Functor.whiskerRight τ G) (shiftFunctor E a))
    (Functor.whiskerLeft (shiftFunctor C a) (Functor.whiskerRight τ G) ≫ Iso.hom (Functor.commShiftIso (F₂ ⋙ G) a))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C a ⋙ F₁ ⋙ G).obj X ⟶ ((F₂ ⋙ G) ⋙ shiftFunctor E a).obj X)
    (app
      (Iso.hom (Functor.commShiftIso (F₁ ⋙ G) a) ≫ Functor.whiskerRight (Functor.whiskerRight τ G) (shiftFunctor E a))
      X)
    (app (Functor.whiskerLeft (shiftFunctor C a) (Functor.whiskerRight τ G) ≫ Iso.hom (Functor.commShiftIso (F₂ ⋙ G) a))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ G ≅ G ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (isoWhiskerLeft (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) e.symm ≪≫
      commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0))
    (isoZero G A)
have w : ∀ (X : C),
  Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ G).obj X ⟶ (G ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X)
    (NatTrans.app
      (Iso.hom
        (isoWhiskerLeft (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) e.symm ≪≫
          commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)))
      X)
    (NatTrans.app (Iso.hom (isoZero G A)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
a b : A
⊢ Eq (α := shiftFunctor C (a + b) ⋙ G ≅ G ⋙ shiftFunctor D (a + b))
    (isoWhiskerLeft (shiftFunctor C (a + b)) e.symm ≪≫
      commShiftIso F (a + b) ≪≫ isoWhiskerRight e (shiftFunctor D (a + b)))
    (isoAdd (isoWhiskerLeft (shiftFunctor C a) e.symm ≪≫ commShiftIso F a ≪≫ isoWhiskerRight e (shiftFunctor D a))
      (isoWhiskerLeft (shiftFunctor C b) e.symm ≪≫ commShiftIso F b ≪≫ isoWhiskerRight e (shiftFunctor D b)))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C (a + b) ⋙ G).obj X ⟶ (G ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app
      (Iso.hom
        (isoWhiskerLeft (shiftFunctor C (a + b)) e.symm ≪≫
          commShiftIso F (a + b) ≪≫ isoWhiskerRight e (shiftFunctor D (a + b))))
      X)
    (NatTrans.app
      (Iso.hom
        (isoAdd (isoWhiskerLeft (shiftFunctor C a) e.symm ≪≫ commShiftIso F a ≪≫ isoWhiskerRight e (shiftFunctor D a))
          (isoWhiskerLeft (shiftFunctor C b) e.symm ≪≫ commShiftIso F b ≪≫ isoWhiskerRight e (shiftFunctor D b))))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
a b : A
X : C
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ G).obj X ⟶ (G ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app
      (Iso.hom
        (isoWhiskerLeft (shiftFunctor C (a + b)) e.symm ≪≫
          commShiftIso F (a + b) ≪≫ isoWhiskerRight e (shiftFunctor D (a + b))))
      X)
    (NatTrans.app
      (Iso.hom
        (isoAdd (isoWhiskerLeft (shiftFunctor C a) e.symm ≪≫ commShiftIso F a ≪≫ isoWhiskerRight e (shiftFunctor D a))
          (isoWhiskerLeft (shiftFunctor C b) e.symm ≪≫ commShiftIso F b ≪≫ isoWhiskerRight e (shiftFunctor D b))))
      X)
have w : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (G.obj X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ map (shiftFunctor D (a + b)) (e.hom.app X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        map (shiftFunctor D b) (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          CategoryStruct.comp (Y :=
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
            (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
            (map (shiftFunctor D b) (map (shiftFunctor D a) (e.hom.app X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (G.obj X))))
Tactic: simp only [comp_obj, F.commShiftIso_add, Iso.trans_hom, isoWhiskerLeft_hom,
      Iso.symm_hom, isoWhiskerRight_hom, NatTrans.comp_app, whiskerLeft_app,
      isoAdd_hom_app, whiskerRight_app, assoc, map_comp, NatTrans.naturality_assoc,
      NatIso.cancel_natIso_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
a b : A
X : C
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (G.obj X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ map (shiftFunctor D (a + b)) (e.hom.app X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor D b) (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          map (shiftFunctor D b) (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            CategoryStruct.comp (Y :=
              obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)))
              (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
              (map (shiftFunctor D b) (map (shiftFunctor D a) (e.hom.app X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (G.obj X))))
have w : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (G.obj X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ map (shiftFunctor D (a + b)) (e.hom.app X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D b) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
      (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso F a)) X ≫ map (shiftFunctor D a) (e.hom.app X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (G.obj X)))
Tactic: simp only [← Functor.map_comp_assoc, e.hom_inv_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (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 G : Functor.{v_1, v_2, u_1, u_2} C D
e : F ≅ G
A : Type u_4
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_4} C A
inst_4 : HasShift.{v_2, u_2, u_4} D A
inst_5 : F.CommShift A
this : G.CommShift A := ofIso e A
a : A
⊢ Eq (α := shiftFunctor C a ⋙ F ⟶ G ⋙ shiftFunctor D a)
    (Iso.hom (commShiftIso F a) ≫ whiskerRight e.hom (shiftFunctor D a))
    (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso G a))
have w : ∀ (x : C),
  Eq (α := (shiftFunctor C a ⋙ F).obj x ⟶ (G ⋙ shiftFunctor D a).obj x)
    (NatTrans.app (Iso.hom (commShiftIso F a) ≫ whiskerRight e.hom (shiftFunctor D a)) x)
    (NatTrans.app (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso G a)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift.{v_1, u_1, u_4} C A := hF.hasShift s i
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (i 0)
    (isoZero F A)
have w : ∀ (X : C),
  Eq (α := (s 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj X) (NatTrans.app (Iso.hom (i 0)) X)
    (NatTrans.app (Iso.hom (isoZero F A)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{v_2, u_2, u_4} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v_1, v_1, u_1, u_1} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift.{v_1, u_1, u_4} C A := hF.hasShift s i
a b : A
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (i (a + b)) (isoAdd (i a) (i b))
have w : ∀ (X : C),
  Eq (α := (s (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X) (NatTrans.app (Iso.hom (i (a + b))) X)
    (NatTrans.app (Iso.hom (isoAdd (i a) (i b))) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a : A
X : C
⊢ Eq (α := G.obj ((shiftFunctor C a ⋙ F).obj X) ⟶ G.obj ((F ⋙ shiftFunctor D a).obj X))
    (G.map (NatTrans.app (Iso.hom (iso e a)) X))
    (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      CategoryStruct.comp (Y := (H ⋙ shiftFunctor E a).obj X) (NatTrans.app (Iso.hom (commShiftIso H a)) X)
        (map (shiftFunctor E a) (e.inv.app X) ≫ NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X)))
have h : Eq (α :=
  obj (obj (whiskeringRight C D E) G) (shiftFunctor C a ⋙ F) ⟶
    obj (obj (whiskeringRight C D E) G) (F ⋙ shiftFunctor D a))
  (map (obj (whiskeringRight C D E) G) (Iso.hom (iso e a)))
  (Iso.hom
    (associator (shiftFunctor C a) F G ≪≫
      isoWhiskerLeft (shiftFunctor C a) e ≪≫
        commShiftIso H a ≪≫
          isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
            F.associator G (shiftFunctor E a) ≪≫
              F.isoWhiskerLeft (Iso.symm (commShiftIso G a)) ≪≫ (F.associator (shiftFunctor D a) G).symm))
Tactic: have h : ((whiskeringRight C D E).obj G).map (iso e a).hom = _ :=
    Functor.map_preimage _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a : A
X : C
⊢ Eq (α := G.obj ((F ⋙ shiftFunctor D a).obj X) ⟶ G.obj ((shiftFunctor C a ⋙ F).obj X))
    (G.map (NatTrans.app (Iso.inv (iso e a)) X))
    (CategoryStruct.comp (Y := (G ⋙ shiftFunctor E a).obj (F.obj X))
      (NatTrans.app (Iso.hom (commShiftIso G a)) (F.obj X))
      (map (shiftFunctor E a) (e.hom.app X) ≫
        NatTrans.app (Iso.inv (commShiftIso H a)) X ≫ e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
have h : Eq (α :=
  obj (obj (whiskeringRight C D E) G) (F ⋙ shiftFunctor D a) ⟶
    obj (obj (whiskeringRight C D E) G) (shiftFunctor C a ⋙ F))
  (map (obj (whiskeringRight C D E) G) (Iso.inv (iso e a)))
  (Iso.inv
    (associator (shiftFunctor C a) F G ≪≫
      isoWhiskerLeft (shiftFunctor C a) e ≪≫
        commShiftIso H a ≪≫
          isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
            F.associator G (shiftFunctor E a) ≪≫
              F.isoWhiskerLeft (Iso.symm (commShiftIso G a)) ≪≫ (F.associator (shiftFunctor D a) G).symm))
Tactic: have h : ((whiskeringRight C D E).obj G).map (iso e a).inv = _ :=
    Functor.map_preimage _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0)
    (OfComp.iso e 0) (isoZero F A)
have w : ∀ (X : C),
  Eq (α :=
    (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
    (NatTrans.app (Iso.hom (OfComp.iso e 0)) X) (NatTrans.app (Iso.hom (isoZero F A)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
X : C
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F).obj X ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X)
    (NatTrans.app (Iso.hom (OfComp.iso e 0)) X) (NatTrans.app (Iso.hom (isoZero F A)) X)
have w : Eq (α :=
  G.obj ((shiftFunctor.{v_1, u_1, u_5} C (A := A) 0 ⋙ F).obj X) ⟶
    G.obj ((F ⋙ shiftFunctor.{v_2, u_2, u_5} D (A := A) 0).obj X))
  (G.map (NatTrans.app (Iso.hom (OfComp.iso e 0)) X)) (G.map (NatTrans.app (Iso.hom (isoZero F A)) X))
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a b : A
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (OfComp.iso e (a + b))
    (isoAdd (OfComp.iso e a) (OfComp.iso e b))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app (Iso.hom (OfComp.iso e (a + b))) X)
    (NatTrans.app (Iso.hom (isoAdd (OfComp.iso e a) (OfComp.iso e b))) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
A_1 : Type u_4
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_3 : G.Full
inst_4 : G.Faithful
A : Type u_5
inst_5 : AddMonoid A
inst_6 : HasShift.{v_1, u_1, u_5} C A
inst_7 : HasShift.{v_2, u_2, u_5} D A
inst_8 : HasShift.{v_3, u_3, u_5} E A
inst_9 : G.CommShift A
inst_10 : H.CommShift A
a b : A
X : C
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app (Iso.hom (OfComp.iso e (a + b))) X)
    (NatTrans.app (Iso.hom (isoAdd (OfComp.iso e a) (OfComp.iso e b))) X)
have w : Eq (α := G.obj ((shiftFunctor C (a + b) ⋙ F).obj X) ⟶ G.obj ((F ⋙ shiftFunctor D (a + b)).obj X))
  (G.map (NatTrans.app (Iso.hom (OfComp.iso e (a + b))) X))
  (G.map (NatTrans.app (Iso.hom (isoAdd (OfComp.iso e a) (OfComp.iso e b))) X))
Tactic: apply G.map_injective