awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
| F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X)) ≫
      (Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C (a + b)) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
          NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
            map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F.obj X) ≫
                map (shiftFunctor E (a + b)) ((Lifting.iso L W F F').inv.app X)
have erw : CategoryStruct.comp (Y :=
  F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
  (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
  ((Lifting.iso L W F F').hom.app
      (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    CategoryStruct.comp (Y :=
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))
      (CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
        (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
        (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X)))))
Tactic: erw [← NatTrans.naturality_assoc]
      dsimp
      rw [← Functor.map_comp_assoc, ← map_comp_assoc, Category.assoc,
        ← map_comp, Iso.inv_hom_id_app]
      dsimp
      rw [map_id, Category.comp_id, ← NatTrans.naturality]
      dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
| CategoryStruct.comp (Y := F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) ((L ⋙ shiftFunctor D a).obj X)))
    (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso L a)) X)))
    (CategoryStruct.comp (Y :=
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X))))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
        (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X)))
      (CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
        (map (shiftFunctor E b) (F'.map (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
        (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          CategoryStruct.comp (Y :=
            obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
            (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
            (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
have erw : CategoryStruct.comp (Y := F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) ((L ⋙ shiftFunctor D a).obj X)))
  (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso L a)) X)))
  (CategoryStruct.comp (Y := (shiftFunctor D b ⋙ F').obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
    ((shiftFunctor D b ⋙ F').map (NatTrans.app (Iso.inv (commShiftIso L a)) X))
    (CategoryStruct.comp (Y := (F' ⋙ shiftFunctor E b).obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
        (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
      (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
          (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
          (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
Tactic: erw [← NatTrans.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
| CategoryStruct.comp (Y := F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) ((L ⋙ shiftFunctor D a).obj X)))
    (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso L a)) X)))
    (CategoryStruct.comp (Y := (shiftFunctor D b ⋙ F').obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
      ((shiftFunctor D b ⋙ F').map (NatTrans.app (Iso.inv (commShiftIso L a)) X))
      (CategoryStruct.comp (Y := (F' ⋙ shiftFunctor E b).obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
        (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
          (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
        (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          CategoryStruct.comp (Y :=
            obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
            (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
            (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
have dsimp : CategoryStruct.comp (Y :=
  F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X))))
  (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso L a)) X)))
  (CategoryStruct.comp (Y :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
    (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
    (CategoryStruct.comp (Y :=
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
        (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
      (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
          (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
          (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
| CategoryStruct.comp (Y :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X))))
    (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso L a)) X)))
    (CategoryStruct.comp (Y :=
      F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
      (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
      (CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
        (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
          (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
        (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          CategoryStruct.comp (Y :=
            obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
            (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
            (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
have rw : F'.map (map (shiftFunctor D b) (𝟙 ((shiftFunctor C a ⋙ L).obj X))) ≫
  CategoryStruct.comp (Y :=
    obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
      (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
    (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
        (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
        (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))
Tactic: rw [← Functor.map_comp_assoc, ← map_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
| F'.map (map (shiftFunctor D b) (𝟙 ((shiftFunctor C a ⋙ L).obj X))) ≫
    CategoryStruct.comp (Y :=
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
        (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
      (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
          (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
          (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))
have dsimp : F'.map (map (shiftFunctor D b) (𝟙 (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))) ≫
  CategoryStruct.comp (Y :=
    obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
      (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
    (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
      CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
        (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
        (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
| F'.map (map (shiftFunctor D b) (𝟙 (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))) ≫
    CategoryStruct.comp (Y :=
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
        (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
      (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
        CategoryStruct.comp (Y :=
          obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
          (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
          (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))
have rw : CategoryStruct.comp (Y := F'.obj ((shiftFunctor C b ⋙ L).obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
  (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
  ((Lifting.iso L W F F').hom.app
      (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    CategoryStruct.comp (Y := (F ⋙ shiftFunctor E b).obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))
      (CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
        (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
        (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X)))))
Tactic: rw [map_id, map_id, Category.id_comp, commShiftOfLocalization.iso_hom_app,
        Category.assoc, Category.assoc, Category.assoc, ← map_comp_assoc,
        Iso.inv_hom_id_app, map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
a b : A
X : C
| CategoryStruct.comp (Y := F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) ((L ⋙ shiftFunctor D a).obj X)))
    (F'.map (map (shiftFunctor D b) (NatTrans.app (Iso.hom (commShiftIso L a)) X)))
    (CategoryStruct.comp (Y :=
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X))))
      (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' b))
        (obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X)))
      (CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))))
        (map (shiftFunctor E b) (F'.map (NatTrans.app (Iso.inv (commShiftIso L a)) X)))
        (map (shiftFunctor E b) ((Lifting.iso L W F F').hom.app (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
          CategoryStruct.comp (Y :=
            obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
            (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
            (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X))))))
have erw : CategoryStruct.comp (Y := F'.obj ((shiftFunctor C b ⋙ L).obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
  (F'.map (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)))
  ((Lifting.iso L W F F').hom.app
      (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)) ≫
    CategoryStruct.comp (Y := (F ⋙ shiftFunctor E b).obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))
      (NatTrans.app (Iso.hom (commShiftIso F b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X))
      (CategoryStruct.comp (Y :=
        obj.{v₃, v₃, u₃, u₃} (shiftFunctor E b) (obj.{v₃, v₃, u₃, u₃} (shiftFunctor E a) (F.obj X)))
        (map (shiftFunctor E b) (NatTrans.app (Iso.hom (commShiftIso F a)) X))
        (map (shiftFunctor E b) (map (shiftFunctor E a) ((Lifting.iso L W F F').inv.app X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd E a b)) (F'.obj (L.obj X)))))
Tactic: erw [← NatTrans.naturality_assoc]
      dsimp
      rw [← Functor.map_comp_assoc, ← map_comp, Iso.hom_inv_id_app]
      dsimp
      rw [map_id, map_id, Category.id_comp, commShiftOfLocalization.iso_hom_app,
        Category.assoc, Category.assoc, Category.assoc, ← map_comp_assoc,
        Iso.inv_hom_id_app, map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
this : F'.CommShift A := L.commShiftOfLocalization W A F F'
⊢ CommShift (Lifting.iso L W F F').hom A
have shift_comm : autoParam
  (∀ (a : A),
    Eq (α := shiftFunctor C a ⋙ L ⋙ F' ⟶ F ⋙ shiftFunctor E a)
      (Iso.hom (Functor.commShiftIso (L ⋙ F') a) ≫ Functor.whiskerRight (Lifting.iso L W F F').hom (shiftFunctor E a))
      (Functor.whiskerLeft (shiftFunctor C a) (Lifting.iso L W F F').hom ≫ Iso.hom (Functor.commShiftIso F a)))
  CommShift.shift_comm._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
A : Type w
inst_4 : AddMonoid A
inst_5 : HasShift.{v₁, u₁, w} C A
F : Functor.{v₁, v₃, u₁, u₃} C E
F' : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : Lifting L W F F'
inst_7 : HasShift.{v₂, u₂, w} D A
inst_8 : HasShift.{v₃, u₃, w} E A
inst_9 : L.CommShift A
inst_10 : F.CommShift A
this : F'.CommShift A := L.commShiftOfLocalization W A F F'
a : A
⊢ Eq (α := shiftFunctor C a ⋙ L ⋙ F' ⟶ F ⋙ shiftFunctor E a)
    (Iso.hom (Functor.commShiftIso (L ⋙ F') a) ≫ Functor.whiskerRight (Lifting.iso L W F F').hom (shiftFunctor E a))
    (Functor.whiskerLeft (shiftFunctor C a) (Lifting.iso L W F F').hom ≫ Iso.hom (Functor.commShiftIso F a))
have shift_comm : ∀ (X : C),
  Eq (α := (shiftFunctor C a ⋙ L ⋙ F').obj X ⟶ (F ⋙ shiftFunctor E a).obj X)
    (app
      (Iso.hom (Functor.commShiftIso (L ⋙ F') a) ≫ Functor.whiskerRight (Lifting.iso L W F F').hom (shiftFunctor E a))
      X)
    (app (Functor.whiskerLeft (shiftFunctor C a) (Lifting.iso L W F F').hom ≫ Iso.hom (Functor.commShiftIso F a)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C₁ M
inst_4 : HasShift.{v_2, u_2, u_3} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst_6 : Category.{v_3, u_4} D₁
inst_7 : Category.{v_4, u_5} D₂
L₁ : Functor.{v_1, v_3, u_1, u_4} C₁ D₁
inst_8 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_5} C₂ D₂
inst_9 : HasShift.{v_3, u_4, u_3} D₁ M
inst_10 : HasShift.{v_4, u_5, u_3} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
G : Functor.{v_3, v_4, u_4, u_5} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift (W₁ := W₁) (W₂ := W₂) M L₁ L₂ G e
⊢ NatTrans.CommShift e.hom M
have refine : ∀ (m : M),
  Eq (α := shiftFunctor C₁ m ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ⟶ (L₁ ⋙ G) ⋙ shiftFunctor D₂ m)
    (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) m) ≫
      Functor.whiskerRight e.hom (shiftFunctor D₂ m))
    (Functor.whiskerLeft (shiftFunctor C₁ m) e.hom ≫ Iso.hom (Functor.commShiftIso (L₁ ⋙ G) m))
Tactic: refine ⟨fun m ↦ ?_⟩