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
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 (α := 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))
have w : Eq (α :=
  G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ⟶
    G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X)))
  (e.hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ≫
    H.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      CategoryStruct.comp (Y :=
        obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (CategoryStruct.comp (Y :=
          obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.obj X)))
          (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso H a)) X))
          (map (shiftFunctor E b) (map (shiftFunctor E a) (e.inv.app X)) ≫
            map (shiftFunctor E b) (NatTrans.app (Iso.inv (commShiftIso G a)) (F.obj X)) ≫
              NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
                G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))))
  (G.map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
    e.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)) ≫
      CategoryStruct.comp (Y :=
        obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
        (map (shiftFunctor E b) (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ≫
          CategoryStruct.comp (Y :=
            G.obj (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.inv (commShiftIso G b)) (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
            (G.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (OfComp.iso e a)) X)) ≫
              G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)))))
Tactic: simp only [comp_obj, OfComp.map_iso_hom_app, H.commShiftIso_add, isoAdd_hom_app,
      G.commShiftIso_add, isoAdd_inv_app, NatTrans.naturality_assoc, comp_map, assoc,
      Iso.inv_hom_id_app_assoc, map_comp]
-- 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 (α :=
    G.obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ⟶
      G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (a + b)) (F.obj X)))
    ((F ⋙ G).map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      e.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)) ≫
        CategoryStruct.comp (Y :=
          obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
          (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
          (map (shiftFunctor E b)
              (CategoryStruct.comp (Y := obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.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))) ≫
            NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X))))
    (G.map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X)) ≫
      e.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)) ≫
        CategoryStruct.comp (Y :=
          obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)))
          (NatTrans.app (Iso.hom (commShiftIso H b)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))
          (map (shiftFunctor E b)
              (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
                G.map (NatTrans.app (Iso.hom (OfComp.iso e a)) X)) ≫
            NatTrans.app (Iso.inv (commShiftIso G b)) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X)) ≫
              G.map (NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X))))
have w : Eq (α :=
  obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (H.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X)) ⟶
    obj.{v_3, v_3, u_3, u_3} (shiftFunctor E b) (G.obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj X))))
  (map (shiftFunctor E b)
    (CategoryStruct.comp (Y := obj.{v_3, v_3, u_3, u_3} (shiftFunctor E a) (H.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))))
  (map (shiftFunctor E b)
    (e.inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫ G.map (NatTrans.app (Iso.hom (OfComp.iso e a)) X)))
Tactic: congr 4
-- 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
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
this : (A : Type u_5) →
  [inst_11 : AddMonoid A] →
    [inst_12 : HasShift.{v_1, u_1, u_5} C A] →
      [inst_13 : HasShift.{v_2, u_2, u_5} D A] →
        [inst_14 : HasShift.{v_3, u_3, u_5} E A] → [G.CommShift A] → [H.CommShift A] → F.CommShift A :=
  ofComp e
⊢ NatTrans.CommShift e.hom A
have refine : ∀ (a : A),
  Eq (α := shiftFunctor C a ⋙ F ⋙ G ⟶ H ⋙ shiftFunctor E a)
    (Iso.hom (commShiftIso (F ⋙ G) a) ≫ whiskerRight e.hom (shiftFunctor E a))
    (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso H a))
Tactic: refine ⟨fun a ↦ ?_⟩
-- 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
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
this : (A : Type u_5) →
  [inst_11 : AddMonoid A] →
    [inst_12 : HasShift.{v_1, u_1, u_5} C A] →
      [inst_13 : HasShift.{v_2, u_2, u_5} D A] →
        [inst_14 : HasShift.{v_3, u_3, u_5} E A] → [G.CommShift A] → [H.CommShift A] → F.CommShift A :=
  ofComp e
a : A
⊢ Eq (α := shiftFunctor C a ⋙ F ⋙ G ⟶ H ⋙ shiftFunctor E a)
    (Iso.hom (commShiftIso (F ⋙ G) a) ≫ whiskerRight e.hom (shiftFunctor E a))
    (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso H a))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C a ⋙ F ⋙ G).obj X ⟶ (H ⋙ shiftFunctor E a).obj X)
    (NatTrans.app (Iso.hom (commShiftIso (F ⋙ G) a) ≫ whiskerRight e.hom (shiftFunctor E a)) X)
    (NatTrans.app (whiskerLeft (shiftFunctor C a) e.hom ≫ Iso.hom (commShiftIso H a)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShift (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D₁
inst_4 : Category.{v_5, u_5} D₂
inst_5 : Category.{v_6, u_6} D₃
F₁₂ : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F₂₃ : Functor.{v_2, v_3, u_2, u_3} C₂ C₃
F₁₃ : Functor.{v_1, v_3, u_1, u_3} C₁ C₃
α : F₁₃ ⟶ F₁₂ ⋙ F₂₃
G₁₂ : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
G₂₃ : Functor.{v_5, v_6, u_5, u_6} D₂ D₃
G₁₃ : Functor.{v_4, v_6, u_4, u_6} D₁ D₃
β : G₁₂ ⋙ G₂₃ ⟶ G₁₃
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
L₃ : Functor.{v_3, v_6, u_3, u_6} C₃ D₃
e₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ G₁₂
e₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ G₂₃
e₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ G₁₃
A : Type u_7
inst_6 : AddMonoid A
inst_7 : HasShift.{v_1, u_1, u_7} C₁ A
inst_8 : HasShift.{v_2, u_2, u_7} C₂ A
inst_9 : HasShift.{v_3, u_3, u_7} C₃ A
inst_10 : HasShift.{v_4, u_4, u_7} D₁ A
inst_11 : HasShift.{v_5, u_5, u_7} D₂ A
inst_12 : HasShift.{v_6, u_6, u_7} D₃ A
inst_13 : F₁₂.CommShift A
inst_14 : F₂₃.CommShift A
inst_15 : F₁₃.CommShift A
inst_16 : CommShift α A
inst_17 : G₁₂.CommShift A
inst_18 : G₂₃.CommShift A
inst_19 : G₁₃.CommShift A
inst_20 : CommShift β A
inst_21 : L₁.CommShift A
inst_22 : L₂.CommShift A
inst_23 : L₃.CommShift A
inst_24 : CommShift e₁₂ A
inst_25 : CommShift e₂₃ A
h₁₃ :
  e₁₃ =
    Functor.whiskerRight α L₃ ≫
      (F₁₂.associator F₂₃ L₃).hom ≫
        F₁₂.whiskerLeft e₂₃ ≫
          (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β
⊢ CommShift e₁₃ A
have subst : CommShift
  (Functor.whiskerRight α L₃ ≫
    (F₁₂.associator F₂₃ L₃).hom ≫
      F₁₂.whiskerLeft e₂₃ ≫
        (F₁₂.associator L₂ G₂₃).inv ≫ Functor.whiskerRight e₁₂ G₂₃ ≫ (L₁.associator G₁₂ G₂₃).hom ≫ L₁.whiskerLeft β)
  A
Tactic: subst h₁₃
Cleared hypotheses: e₁₃, h₁₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (goal)
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
inst_5 : Preadditive.{v_5, u_5} D
inst_6 : HasShift.{v_5, u_5, 0} D ℤ
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_5, u_5, v_5, u_5} (shiftFunctor D n)
x x_1 x_2 : ℤ × ℤ
⊢ HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        ((x + x_1).1 * x_2.2) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * x_1.2) =
    HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * (x_1 + x_2).2) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x_1.1 * x_2.2)
have dsimp : HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      ((x.1 + x_1.1) * x_2.2) *
    HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      (x.1 * x_1.2) =
  HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      (x.1 * (x_1.2 + x_2.2)) *
    HPow.hPow (α :=
      (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
      (x_1.1 * x_2.2)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (goal)
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
inst_5 : Preadditive.{v_5, u_5} D
inst_6 : HasShift.{v_5, u_5, 0} D ℤ
inst_7 : ∀ (n : ℤ), Functor.Additive.{v_5, u_5, v_5, u_5} (shiftFunctor D n)
x x_1 x_2 : ℤ × ℤ
⊢ HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        ((x.1 + x_1.1) * x_2.2) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * x_1.2) =
    HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x.1 * (x_1.2 + x_2.2)) *
      HPow.hPow (α :=
        (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
        (x_1.1 * x_2.2)
have rw : HPow.hPow (α :=
    (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
    ((x.1 + x_1.1) * x_2.2 + x.1 * x_1.2) =
  HPow.hPow (α :=
    (CatCenter.{v_5, u_5} (PullbackShift.{v_5, u_5, 0, 0} D (AddMonoidHom.fst ℤ ℤ + AddMonoidHom.snd ℤ ℤ)))ˣ) (-1)
    (x.1 * (x_1.2 + x_2.2) + x_1.1 * x_2.2)
Tactic: rw [← zpow_add, ← zpow_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (goal)
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_2, u_2, u_6} C₁' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_2, v_1, u_2, u_1} C₁' C₁
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁' Y₁' : C₁'
f : X₁' ⟶ Y₁'
⊢ NatTrans.CommShift ((F ⋙ G).map f) M
have dsimp : NatTrans.CommShift (G.map (F.map f)) M
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (hypothesis)
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_2, u_2, u_6} C₁' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_2, v_1, u_2, u_1} C₁' C₁
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
⊢ Eq (α :=
    (shiftFunctor C₂ n ⋙ (F ⋙ G).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁')).obj X₂ ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) (((F ⋙ G).flip.obj X₂ ⋙ shiftFunctor D m).obj X₁'))
    (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).obj (obj.{v_2, v_2, u_2, u_2} (shiftFunctor C₁' m) X₁')) n)) X₂ ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).flip.obj X₂) m)) X₁'))
    (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m)) X₁' ≫
      map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso ((F ⋙ G).obj X₁') n)) X₂) ≫
        Iso.inv (shiftComm (((F ⋙ G).obj X₁').obj X₂) m n) ≫
          (↑(h.ε m n) : CatCenter D).app
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) (((F ⋙ G).obj X₁').obj X₂))))
have this : Eq (α :=
  (shiftFunctor C₂ n ⋙ G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))).obj X₂ ⟶
    obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) ((G.flip.obj X₂ ⋙ shiftFunctor D m).obj (F.obj X₁')))
  (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) (F.obj X₁'))) n)) X₂ ≫
    map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj X₂) m)) (F.obj X₁')))
  (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) X₂)) m)) (F.obj X₁') ≫
    map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj (F.obj X₁')) n)) X₂) ≫
      Iso.inv (shiftComm ((G.obj (F.obj X₁')).obj X₂) m n) ≫
        (↑(h.ε m n) : CatCenter D).app
          (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj (F.obj X₁')).obj X₂))))
Tactic: have := G.commShift₂_comm h (F.obj X₁') X₂ m n
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (hypothesis)
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_4, u_4, u_6} C₂' M
inst_8 : HasShift.{v_3, u_3, u_6} C₂ M
inst_9 : HasShift.{v_5, u_5, u_6} D M
F : Functor.{v_4, v_3, u_4, u_3} C₂' C₂
inst_10 : F.CommShift M
G : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_11 : G.CommShift₂ h
X₁ : C₁
X₂' : C₂'
m n : M
⊢ Eq (α :=
    (shiftFunctor C₂' n ⋙
            (G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj
        X₂' ⟶
      obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
        (((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj X₂' ⋙ shiftFunctor D m).obj X₁))
    (NatTrans.app
        (Iso.hom
          (commShiftIso ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁))
            n))
        X₂' ≫
      map (shiftFunctor D n)
        (NatTrans.app (Iso.hom (commShiftIso ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj X₂') m)) X₁))
    (NatTrans.app
        (Iso.hom
          (commShiftIso
            ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).flip.obj (obj.{v_4, v_4, u_4, u_4} (shiftFunctor C₂' n) X₂')) m))
        X₁ ≫
      map (shiftFunctor D m)
          (NatTrans.app (Iso.hom (commShiftIso ((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj X₁) n)) X₂') ≫
        Iso.inv (shiftComm (((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj X₁).obj X₂') m n) ≫
          (↑(h.ε m n) : CatCenter D).app
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
              (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) (((G ⋙ obj (whiskeringLeft C₂' C₂ D) F).obj X₁).obj X₂'))))
have this : Eq (α :=
  (shiftFunctor C₂ n ⋙ G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)).obj (F.obj X₂') ⟶
    obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n) ((G.flip.obj (F.obj X₂') ⋙ shiftFunctor D m).obj X₁))
  (NatTrans.app (Iso.hom (commShiftIso (G.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C₁ m) X₁)) n)) (F.obj X₂') ≫
    map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (F.obj X₂')) m)) X₁))
  (NatTrans.app (Iso.hom (commShiftIso (G.flip.obj (obj.{v_3, v_3, u_3, u_3} (shiftFunctor C₂ n) (F.obj X₂'))) m)) X₁ ≫
    map (shiftFunctor D m) (NatTrans.app (Iso.hom (commShiftIso (G.obj X₁) n)) (F.obj X₂')) ≫
      Iso.inv (shiftComm ((G.obj X₁).obj (F.obj X₂')) m n) ≫
        (↑(h.ε m n) : CatCenter D).app
          (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D n)
            (obj.{v_5, v_5, u_5, u_5} (shiftFunctor D m) ((G.obj X₁).obj (F.obj X₂')))))
Tactic: have := G.commShift₂_comm h X₁ (F.obj X₂') m n
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (goal)
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
x : C₂
⊢ CommShift (flipApp (𝟙 G₁) x) M
have simp : CommShift (𝟙 (G₁.flip.obj x)) M
Tactic: simp only [flipApp, flipFunctor_obj, Functor.map_id, id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.CommShiftTwo (goal)
Goal:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₁'
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₂'
inst_4 : Category.{v_5, u_5} D
M : Type u_6
inst_5 : AddCommMonoid M
inst_6 : HasShift.{v_1, u_1, u_6} C₁ M
inst_7 : HasShift.{v_3, u_3, u_6} C₂ M
inst_8 : HasShift.{v_5, u_5, u_6} D M
G₁ G₂ G₃ : C₁ ⥤ Functor.{v_3, v_5, u_3, u_5} C₂ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup.{v_5, u_5, u_6} D M
inst_9 : G₁.CommShift₂ h
inst_10 : G₂.CommShift₂ h
inst_11 : G₃.CommShift₂ h
inst_12 : CommShift₂ τ h
inst_13 : CommShift₂ τ' h
x : C₂
⊢ CommShift (flipApp (τ ≫ τ') x) M
have simp : CommShift (F₁ := G₁.flip.obj x) (F₂ := G₃.flip.obj x)
  (CategoryStruct.comp (Y := G₂.flip.obj x) (app (Functor.map (flipFunctor C₁ C₂ D) τ) x)
      (app (Functor.map (flipFunctor C₁ C₂ D) τ') x) :
    G₁.flip.obj x ⟶ G₃.flip.obj x)
  M
Tactic: simp only [flipApp, flipFunctor_obj, Functor.map_comp, comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
⊢ (zero F s i).hom.app (F.obj X) =
    NatTrans.app (Iso.hom (i 0)) X ≫ F.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)
have h : F.whiskerLeft (zero F s i).hom =
  (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
Tactic: have h : whiskerLeft F (zero F s i).hom = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
X : C
⊢ (zero F s i).inv.app (F.obj X) =
    F.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X) ≫ NatTrans.app (Iso.inv (i 0)) X
have h : F.whiskerLeft (zero F s i).inv =
  (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
Tactic: have h : whiskerLeft F (zero F s i).inv = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _