awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app (Iso.hom (commShiftIso G (m + n))) ((Φ a'').obj X) ≫
      map (shiftFunctor E (m + n)) ((hΦ a'').hom.app X) ≫ (F.shiftIso (m + n) a a'' ⋯).hom.app X ≫ (hΦ a).inv.app X =
    G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((Φ a'').obj X)) ≫
      G.map
          (𝟙
            (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n)
              (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X)))) ≫
        NatTrans.app (Iso.hom (commShiftIso G n)) (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X)) ≫
          (map (shiftFunctor E n) (NatTrans.app (Iso.hom (commShiftIso G m)) ((Φ a'').obj X)) ≫
              map (shiftFunctor E n) (map (shiftFunctor E m) ((hΦ a'').hom.app X)) ≫
                map (shiftFunctor E n) ((F.shiftIso m a' a'' ha'').hom.app X) ≫
                  map (shiftFunctor E n) ((hΦ a').inv.app X)) ≫
            map (shiftFunctor E n) ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X ≫ (hΦ a).inv.app X
have w : NatTrans.app (Iso.hom (commShiftIso G (m + n))) ((Φ a'').obj X) ≫
    map (shiftFunctor E (m + n)) ((hΦ a'').hom.app X) ≫
      ((F.functor a'').isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
                ((F.functor a'').associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
                  isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor E n) ≪≫ F.shiftIso n a a' ha').hom.app
          X ≫
        (hΦ a).inv.app X =
  G.map (NatTrans.app (Iso.hom (shiftFunctorAdd D m n)) ((Φ a'').obj X)) ≫
    G.map
        (𝟙
          (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D n) (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X)))) ≫
      NatTrans.app (Iso.hom (commShiftIso G n)) (obj.{u_6, u_6, u_2, u_2} (shiftFunctor D m) ((Φ a'').obj X)) ≫
        (map (shiftFunctor E n) (NatTrans.app (Iso.hom (commShiftIso G m)) ((Φ a'').obj X)) ≫
            map (shiftFunctor E n) (map (shiftFunctor E m) ((hΦ a'').hom.app X)) ≫
              map (shiftFunctor E n) ((F.shiftIso m a' a'' ha'').hom.app X) ≫
                map (shiftFunctor E n) ((hΦ a').inv.app X)) ≫
          map (shiftFunctor E n) ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X ≫ (hΦ a).inv.app X
Tactic: rw [F.shiftIso_add n m a a' a'' ha' ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
ha' : n + a = a'
⊢ Iso.hom (shiftIso (postcomp (F.lift G Φ hΦ) G) n a a' ha') ≫ (hΦ a).hom =
    whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom
have w : ∀ (X : C),
  (Iso.hom (shiftIso (postcomp (F.lift G Φ hΦ) G) n a a' ha') ≫ (hΦ a).hom).app X =
    (whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom).app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
ha' : n + a = a'
X : C
⊢ (Iso.hom (shiftIso (postcomp (F.lift G Φ hΦ) G) n a a' ha') ≫ (hΦ a).hom).app X =
    (whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom).app X
have this : (hΦ a).inv.app X ≫ (hΦ a).hom.app X = 𝟙 ((F.functor a).obj X)
Tactic: have := (hΦ a).inv_hom_id_app X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst_9 : Preadditive.{u_5, u_1} C
inst_10 : Preadditive.{u_6, u_2} D
inst_11 : Preadditive.{u_7, u_3} E
inst_12 : G.Additive
a : A
inst_13 : (F.functor a).Additive
⊢ (functor (F.lift G Φ hΦ) a ⋙ G).Additive
have dsimp : (Φ a ⋙ G).Additive
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctorsLift (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_6, u_2} D
inst_2 : Category.{u_7, u_3} E
A : Type u_4
inst_3 : AddMonoid A
inst_4 : HasShift.{u_6, u_2, u_4} D A
inst_5 : HasShift.{u_7, u_3, u_4} E A
F : SingleFunctors.{u_5, u_1, u_7, u_3, u_4} C E A
G : Functor.{u_6, u_7, u_2, u_3} D E
inst_6 : G.CommShift A
inst_7 : G.Full
inst_8 : G.Faithful
Φ : A → Functor.{u_5, u_6, u_1, u_2} C D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst_9 : Preadditive.{u_5, u_1} C
inst_10 : Preadditive.{u_6, u_2} D
inst_11 : Preadditive.{u_7, u_3} E
inst_12 : G.Additive
a : A
inst_13 : (F.functor a).Additive
⊢ (functor (F.lift G Φ hΦ) a).Additive
have this : (functor (F.lift G Φ hΦ) a ⋙ G).Additive
Tactic: have : ((lift F G Φ hΦ).functor a ⋙ G).Additive := by
    dsimp
    rwa [Functor.additive_iff_of_iso (hΦ a)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : t.Category
⊢ NatTrans.app
        (Iso.hom
          (NatIso.ofComponents
            (fun (X : C) ↦
              HSMul.hSMul (β :=
                Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ≅
                  Functor.obj.{v, v, u, u} (shiftFunctor C (a + b) ⋙ shiftFunctor C c) X)
                (t.z (a + b) c) (Iso.app (shiftFunctorAdd C (a + b) c) X))
            ⋯))
        X ≫
      Functor.map (shiftFunctor C c)
        ((NatIso.ofComponents
                (fun (X : C) ↦
                  HSMul.hSMul (β :=
                    Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
                      Functor.obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor C b) X)
                    (t.z a b) (Iso.app (shiftFunctorAdd C a b) X))
                ⋯).hom.app
          X) =
    eqToHom ⋯ ≫
      NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (X : C) ↦
                HSMul.hSMul (β :=
                  Functor.obj.{v, v, u, u} (shiftFunctor C (a + (b + c))) X ≅
                    Functor.obj.{v, v, u, u} (shiftFunctor C a ⋙ shiftFunctor C (b + c)) X)
                  (t.z a (b + c)) (Iso.app (shiftFunctorAdd C a (b + c)) X))
              ⋯))
          X ≫
        (NatIso.ofComponents
                (fun (X : C) ↦
                  HSMul.hSMul (β :=
                    Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) X ≅
                      Functor.obj.{v, v, u, u} (shiftFunctor C b ⋙ shiftFunctor C c) X)
                    (t.z b c) (Iso.app (shiftFunctorAdd C b c) X))
                ⋯).hom.app
          (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)
have dsimp : (HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ≅
          Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X))
        (t.z (a + b) c) (Iso.app (shiftFunctorAdd C (a + b) c) X)).hom ≫
    Functor.map (shiftFunctor C c)
      (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
            Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
          (t.z a b) (Iso.app (shiftFunctorAdd C a b) X)).hom =
  eqToHom sorry ≫
    (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (a + (b + c))) X ≅
            Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
          (t.z a (b + c)) (Iso.app (shiftFunctorAdd C a (b + c)) X)).hom ≫
      (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X) ≅
            Functor.obj.{v, v, u, u} (shiftFunctor C c)
              (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
          (t.z b c) (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))).hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : t.Category
⊢ (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ≅
            Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X))
          (t.z (a + b) c) (Iso.app (shiftFunctorAdd C (a + b) c) X)).hom ≫
      Functor.map (shiftFunctor C c)
        (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
            (t.z a b) (Iso.app (shiftFunctorAdd C a b) X)).hom =
    eqToHom ⋯ ≫
      (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (a + (b + c))) X ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))
            (t.z a (b + c)) (Iso.app (shiftFunctorAdd C a (b + c)) X)).hom ≫
        (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X) ≅
              Functor.obj.{v, v, u, u} (shiftFunctor C c)
                (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
            (t.z b c) (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))).hom
have simp : Eq (α :=
  Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ⟶
    Functor.obj.{v, v, u, u} (shiftFunctor C c)
      (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
  (Iso.hom (Iso.app (shiftFunctorAdd C (a + b) c) X) ≫
    (↑(t.z (a + b) c) : CatCenter t.Category).app
        (Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X)) ≫
      Functor.map (shiftFunctor C c) (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)) ≫
        Functor.map (shiftFunctor C c)
          ((↑(t.z a b) : CatCenter t.Category).app
            (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))
  (eqToHom sorry ≫
    Iso.hom (Iso.app (shiftFunctorAdd C a (b + c)) X) ≫
      (↑(t.z a (b + c)) : CatCenter t.Category).app
          (Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
        Iso.hom (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
          (↑(t.z b c) : CatCenter t.Category).app
            (Functor.obj.{v, v, u, u} (shiftFunctor C c)
              (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))
Tactic: simp only [Functor.map_comp, Category.assoc, CatCenter.smul_iso_hom_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
a b c : A
X : t.Category
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
    (Iso.hom (Iso.app (shiftFunctorAdd C (a + b) c) X) ≫
      (↑(t.z (a + b) c) : CatCenter t.Category).app
          (Functor.obj.{v, v, u, u} (shiftFunctor C c) (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b)) X)) ≫
        Functor.map (shiftFunctor C c) (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)) ≫
          Functor.map (shiftFunctor C c)
            ((↑(t.z a b) : CatCenter t.Category).app
              (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))
    (eqToHom ⋯ ≫
      Iso.hom (Iso.app (shiftFunctorAdd C a (b + c)) X) ≫
        (↑(t.z a (b + c)) : CatCenter t.Category).app
            (Functor.obj.{v, v, u, u} (shiftFunctor C (b + c)) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
          Iso.hom (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫
            (↑(t.z b c) : CatCenter t.Category).app
              (Functor.obj.{v, v, u, u} (shiftFunctor C c)
                (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X))))
have rw : Eq (α :=
  Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X ⟶
    Functor.obj.{v, v, u, u} (shiftFunctor C c)
      (Functor.obj.{v, v, u, u} (shiftFunctor C b) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
  ((↑(t.z a (b + c) * t.z b c) : CatCenter t.Category).app (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X) ≫
    Iso.hom (Iso.app (shiftFunctorAdd C (a + b) c) X) ≫
      Functor.map (shiftFunctor C c) (Iso.hom (Iso.app (shiftFunctorAdd C a b) X)))
  ((↑(t.z a (b + c) * t.z b c) : CatCenter t.Category).app (Functor.obj.{v, v, u, u} (shiftFunctor C (a + b + c)) X) ≫
    eqToHom sorry ≫
      Iso.hom (Iso.app (shiftFunctorAdd C a (b + c)) X) ≫
        Iso.hom (Iso.app (shiftFunctorAdd C b c) (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)))
Tactic: rw [CatCenter.naturality, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      CatCenter.naturality_assoc, CatCenter.naturality_assoc, CatCenter.naturality_assoc,
      t.shift_z_app, CatCenter.naturality, CatCenter.naturality_assoc,
      ← CatCenter.mul_app_assoc, ← CatCenter.mul_app_assoc,
      ← Units.val_mul, ← Units.val_mul, t.assoc a b c]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
have dsimp : NatTrans.app (eqToHom sorry) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd t.Category i j)) X =
  HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X))
    (↑(t.z i j) : CatCenter C) (NatTrans.app (eqToHom sorry) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C i j)) X)
Tactic: dsimp [shiftFunctorAdd']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    (↑(t.z i j) : CatCenter C) •
      (t.shiftIso k).hom.app X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
          Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
            (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
have this : NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
  HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
    (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
Tactic: have : (shiftFunctorAdd' t.Category i j k h).hom.app X =
      (t.z i j).val • (shiftFunctorAdd' C i j k h).hom.app X := by
    dsimp [shiftFunctorAdd']
    cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    (↑(t.z i j) : CatCenter C) •
      (t.shiftIso k).hom.app X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
          Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
            (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
have rw : HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
    (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X) =
  (↑(t.z i j) : CatCenter C) •
    (t.shiftIso k).hom.app X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
          (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
⊢ HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X) =
    (↑(t.z i j) : CatCenter C) •
      (t.shiftIso k).hom.app X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
          Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
            (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
have e_a : NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X =
  (t.shiftIso k).hom.app X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
      Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
        (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X =
    (t.shiftIso k).hom.app X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).inv.app X) ≫
          (t.shiftIso j).inv.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X)
have e_a : NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X =
  𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C k) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
      Functor.map (shiftFunctor C j) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
        𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X))
Tactic: change _ = 𝟙 _ ≫ _ ≫ (shiftFunctor C j).map (𝟙 _) ≫ 𝟙 _
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
have dsimp : NatTrans.app (Iso.inv (shiftFunctorAdd t.Category i j)) X ≫ NatTrans.app (eqToHom sorry) X =
  HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
    (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd C i j)) X ≫ NatTrans.app (eqToHom sorry) X)
Tactic: dsimp [shiftFunctorAdd']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Twist (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    (↑(t.z i j)⁻¹ : CatCenter C) •
      (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
have this : NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
  HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
    (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
Tactic: have : (shiftFunctorAdd' t.Category i j k h).inv.app X =
      ((t.z i j)⁻¹).val • (shiftFunctorAdd' C i j k h).inv.app X := by
    dsimp [shiftFunctorAdd']
    cat_disch