awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (hypothesis)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
⊢ F.map (NatTrans.app (Iso.hom (add hF s i n 0)) X) = F.map (eqToHom ⋯ ≫ (zero hF s i).inv.app ((s n).obj X))
have this : Eq (α := (s (n + 0) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (n + 0)).obj X) (NatTrans.app (Iso.hom (i (n + 0))) X)
  (eqToHom sorry ≫ (i n).hom.app X ≫ eqToHom sorry)
Tactic: have := dcongr_arg (fun a => (i a).hom.app X) (add_zero n)
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
⊢ 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)
    (isoZero' F A 0 ⋯) (isoZero F A)
have w : ∀ (x : C),
  Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F).obj x ⟶ (F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0).obj x)
    (NatTrans.app (Iso.hom (isoZero' F A 0 sorry)) x) (NatTrans.app (Iso.hom (isoZero F A)) x)
Tactic: ext
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
⊢ isoAdd' ⋯ e (isoZero F A) = e
have w : ∀ (X : C), NatTrans.app (Iso.hom (isoAdd' sorry e (isoZero F A))) X = e.hom.app X
Tactic: ext X
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
⊢ isoAdd' ⋯ (isoZero F A) e = e
have w : ∀ (X : C), NatTrans.app (Iso.hom (isoAdd' sorry (isoZero F A) e)) X = e.hom.app X
Tactic: ext X
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
a : A
e : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
X : C
⊢ NatTrans.app (Iso.hom (isoAdd' ⋯ (isoZero F A) e)) X = e.hom.app X
have this : Eq (α :=
  (shiftFunctor C a ⋙ F).obj (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
    (F ⋙ shiftFunctor D a).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))
  ((shiftFunctor C a ⋙ F).map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫
    e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))
  (e.hom.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ≫
    (F ⋙ shiftFunctor D a).map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X))
Tactic: have := e.hom.naturality ((shiftFunctorZero C A).inv.app X)
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
⊢ Eq (α := shiftFunctor C abc ⋙ F ≅ F ⋙ shiftFunctor D abc) (isoAdd' ⋯ (isoAdd' hab ea eb) ec)
    (isoAdd' ⋯ ea (isoAdd' hbc eb ec))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C abc ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D abc).obj X)
    (NatTrans.app (Iso.hom (isoAdd' sorry (isoAdd' hab ea eb) ec)) X)
    (NatTrans.app (Iso.hom (isoAdd' sorry ea (isoAdd' hbc eb ec))) X)
Tactic: ext X
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
⊢ Eq (α := (shiftFunctor C abc ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D abc).obj X)
    (NatTrans.app (Iso.hom (isoAdd' ⋯ (isoAdd' hab ea eb) ec)) X)
    (NatTrans.app (Iso.hom (isoAdd' ⋯ ea (isoAdd' hbc eb ec))) X)
have this : Eq (α :=
  (shiftFunctor C c ⋙ F).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X) ⟶
    (F ⋙ shiftFunctor D c).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
  ((shiftFunctor C c ⋙ F).map (Iso.hom (Iso.app (shiftFunctorAdd' C a b ab hab) X)) ≫
    ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ≫
      (F ⋙ shiftFunctor D c).map (Iso.inv (Iso.app (shiftFunctorAdd' C a b ab hab) X)))
  (ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
Tactic: have := NatTrans.naturality_2 ec.hom ((shiftFunctorAdd' C a b ab hab).app X)
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
this :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C c) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D c) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X)))
    (F.map (map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        map (shiftFunctor D c) (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C a b ab hab)) X)))
    (ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C abc) X) ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D abc) (F.obj X))
    (NatTrans.app (Iso.hom (isoAdd' ⋯ (isoAdd' hab ea eb) ec)) X)
    (NatTrans.app (Iso.hom (isoAdd' ⋯ ea (isoAdd' hbc eb ec))) X)
have w : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C abc) X) ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D abc) (F.obj X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C ab c abc sorry)) X) ≫
    ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C ab) X) ≫
      map (shiftFunctor D c)
          (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b ab hab)) X) ≫
            eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
              map (shiftFunctor D b) (ea.hom.app X) ≫
                NatTrans.app (Iso.inv (shiftFunctorAdd' D a b ab hab)) (F.obj X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D ab c abc sorry)) (F.obj X))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C a bc abc sorry)) X) ≫
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd' C b c bc hbc)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
      ec.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
        map (shiftFunctor D c) (eb.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D b c bc hbc))
              (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
            map (shiftFunctor D bc) (ea.hom.app X) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' D a bc abc sorry)) (F.obj X))
Tactic: simp only [isoAdd'_hom_app, Category.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 : Functor.{v_1, v_2, u_1, u_2} C D
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 : A
h : a = 0
⊢ Eq (α := shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a) (commShiftIso F a) (CommShift.isoZero' F A a h)
have subst : 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)
  (commShiftIso F 0) (CommShift.isoZero' F A 0 sorry)
Tactic: subst h
Cleared hypotheses: a, h
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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 ⋙ F ≅ F ⋙ shiftFunctor.{v_2, u_2, u_4} D (A := A) 0)
    (commShiftIso F 0) (CommShift.isoZero' F A 0 ⋯)
have rw : 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)
  (commShiftIso F 0) (CommShift.isoZero F A)
Tactic: rw [CommShift.isoZero'_eq_isoZero, commShiftIso_zero]
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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
rw :
  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)
    (commShiftIso F 0) (CommShift.isoZero F A)
⊢ 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)
    (commShiftIso F 0) (CommShift.isoZero' F A 0 ⋯)
have rw₁ : 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)
  (CommShift.isoZero F A) (CommShift.isoZero F A)
Tactic: rw [CommShift.isoZero'_eq_isoZero, commShiftIso_zero]
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
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 c : A
h : a + b = c
⊢ Eq (α := shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c) (commShiftIso F c)
    (CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b))
have subst : Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (commShiftIso F (a + b))
  (CommShift.isoAdd' sorry (commShiftIso F a) (commShiftIso F b))
Tactic: subst h
Cleared hypotheses: c, h
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
⊢ Eq (α := shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ⋙ G ≅ (F ⋙ G) ⋙ shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)
    (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) F G) ≪≫
      isoWhiskerRight (commShiftIso F 0) G ≪≫
        F.associator (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) G ≪≫
          F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)).symm)
    (isoZero (F ⋙ G) A)
have w : ∀ (X : C),
  Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ⋙ G).obj X ⟶
      ((F ⋙ G) ⋙ shiftFunctor.{v_3, u_3, u_4} E (A := A) 0).obj X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) F G) ≪≫
          isoWhiskerRight (commShiftIso F 0) G ≪≫
            F.associator (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) G ≪≫
              F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)).symm))
      X)
    (NatTrans.app (Iso.hom (isoZero (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
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
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
X : C
⊢ Eq (α :=
    (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0 ⋙ F ⋙ G).obj X ⟶
      ((F ⋙ G) ⋙ shiftFunctor.{v_3, u_3, u_4} E (A := A) 0).obj X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) F G) ≪≫
          isoWhiskerRight (commShiftIso F 0) G ≪≫
            F.associator (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) G ≪≫
              F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0)).symm))
      X)
    (NatTrans.app (Iso.hom (isoZero (F ⋙ G) A)) X)
have w : 𝟙 (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_4} C (A := A) 0) X))) ≫
    G.map (NatTrans.app (Iso.hom (commShiftIso F 0)) X) ≫
      𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor.{v_2, u_2, u_4} D (A := A) 0) (F.obj X))) ≫
        NatTrans.app (Iso.hom (commShiftIso G 0)) (F.obj X) ≫
          𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor.{v_3, u_3, u_4} E (A := A) 0) (G.obj (F.obj X))) =
  NatTrans.app (Iso.hom (isoZero (F ⋙ G) A)) X
Tactic: dsimp
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
a b : A
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ⋙ G ≅ (F ⋙ G) ⋙ shiftFunctor E (a + b))
    (Iso.symm (associator (shiftFunctor C (a + b)) F G) ≪≫
      isoWhiskerRight (commShiftIso F (a + b)) G ≪≫
        F.associator (shiftFunctor D (a + b)) G ≪≫
          F.isoWhiskerLeft (commShiftIso G (a + b)) ≪≫ (F.associator G (shiftFunctor E (a + b))).symm)
    (isoAdd
      (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
        isoWhiskerRight (commShiftIso F a) G ≪≫
          F.associator (shiftFunctor D a) G ≪≫
            F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
      (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
        isoWhiskerRight (commShiftIso F b) G ≪≫
          F.associator (shiftFunctor D b) G ≪≫
            F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C (a + b) ⋙ F ⋙ G).obj X ⟶ ((F ⋙ G) ⋙ shiftFunctor E (a + b)).obj X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor C (a + b)) F G) ≪≫
          isoWhiskerRight (commShiftIso F (a + b)) G ≪≫
            F.associator (shiftFunctor D (a + b)) G ≪≫
              F.isoWhiskerLeft (commShiftIso G (a + b)) ≪≫ (F.associator G (shiftFunctor E (a + b))).symm))
      X)
    (NatTrans.app
      (Iso.hom
        (isoAdd
          (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
            isoWhiskerRight (commShiftIso F a) G ≪≫
              F.associator (shiftFunctor D a) G ≪≫
                F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
          (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
            isoWhiskerRight (commShiftIso F b) G ≪≫
              F.associator (shiftFunctor D b) G ≪≫
                F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)))
      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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
A : Type u_4
B : Type u_5
inst_3 : AddMonoid A
inst_4 : AddCommMonoid B
inst_5 : HasShift.{v_1, u_1, u_4} C A
inst_6 : HasShift.{v_2, u_2, u_4} D A
inst_7 : HasShift.{v_3, u_3, u_4} E A
inst_8 : HasShift.{v_1, u_1, u_5} C B
inst_9 : HasShift.{v_2, u_2, u_5} D B
inst_10 : F.CommShift A
inst_11 : G.CommShift A
a b : A
X : C
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F ⋙ G).obj X ⟶ ((F ⋙ G) ⋙ shiftFunctor E (a + b)).obj X)
    (NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor C (a + b)) F G) ≪≫
          isoWhiskerRight (commShiftIso F (a + b)) G ≪≫
            F.associator (shiftFunctor D (a + b)) G ≪≫
              F.isoWhiskerLeft (commShiftIso G (a + b)) ≪≫ (F.associator G (shiftFunctor E (a + b))).symm))
      X)
    (NatTrans.app
      (Iso.hom
        (isoAdd
          (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
            isoWhiskerRight (commShiftIso F a) G ≪≫
              F.associator (shiftFunctor D a) G ≪≫
                F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
          (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
            isoWhiskerRight (commShiftIso F b) G ≪≫
              F.associator (shiftFunctor D b) G ≪≫
                F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)))
      X)
have w : 𝟙 (G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X))) ≫
    G.map (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X) ≫
      𝟙 (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))) ≫
        NatTrans.app (Iso.hom (commShiftIso G (a + b))) (F.obj X) ≫
          𝟙 (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E (a + b)) (G.obj (F.obj X))) =
  NatTrans.app
    (Iso.hom
      (isoAdd
        (Iso.symm (associator (shiftFunctor C a) F G) ≪≫
          isoWhiskerRight (commShiftIso F a) G ≪≫
            F.associator (shiftFunctor D a) G ≪≫
              F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
        (Iso.symm (associator (shiftFunctor C b) F G) ≪≫
          isoWhiskerRight (commShiftIso F b) G ≪≫
            F.associator (shiftFunctor D b) G ≪≫
              F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)))
    X
Tactic: dsimp
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).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) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm D a b)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
have eq : Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
  (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
  (NatTrans.app (Iso.hom (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))) X)
Tactic: have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add a b)) X
-- 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 : Functor.{v_1, v_2, u_1, u_2} C D
B : Type u_5
inst_2 : AddCommMonoid B
inst_3 : HasShift.{v_1, u_1, u_5} C B
inst_4 : HasShift.{v_2, u_2, u_5} D B
inst_5 : F.CommShift B
X : C
a b : B
eq :
  Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F (a + b))) X)
    (NatTrans.app (Iso.hom (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))) X)
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ shiftFunctor C b) X) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b ⋙ shiftFunctor C a) X))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorComm C a b)) X))
    (CategoryStruct.comp (Y := (F ⋙ shiftFunctor D b).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) ≫
        NatTrans.app (Iso.hom (shiftFunctorComm D a b)) (F.obj X) ≫
          map (shiftFunctor D a) (NatTrans.app (Iso.inv (commShiftIso F b)) X) ≫
            NatTrans.app (Iso.inv (commShiftIso F a)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) X)))
have eq₁ : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X))
  (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.hom (commShiftIso F (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) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))
Tactic: simp only [comp_obj, CommShift.isoAdd_hom_app,
    ← cancel_epi (F.map ((shiftFunctorAdd C a b).inv.app X)),
    ← F.map_comp_assoc, Iso.inv_hom_id_app, F.map_id, Category.id_comp] at eq
Cleared hypotheses: eq