awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Linear (goal)
Goal:
R : Type u_1
inst : Ring R
C : Type u_4
inst_1 : Category.{v_1, u_4} C
inst_2 : Preadditive.{v_1, u_4} C
inst_3 : Linear.{u_1, v_1, u_4} R C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : Linear.{u_1, v_2, u_2} R D
M : Type u_3
inst_7 : AddMonoid M
inst_8 : HasShift.{v_1, u_4, u_3} C M
inst_9 : ∀ (n : M), Functor.Linear.{u_1, v_1, u_4, v_1, u_4} R (shiftFunctor C n)
L : Functor.{v_1, v_2, u_4, u_2} C D
W : MorphismProperty.{v_1, u_4} C
inst_10 : L.IsLocalization W
inst_11 : Functor.Linear R L
inst_12 : HasShift.{v_2, u_2, u_3} D M
inst_13 : L.CommShift M
n : M
this : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n)
⊢ Functor.Linear.{u_1, v_2, u_2, v_2, u_2} R (shiftFunctor D n)
have rw : Functor.Linear R (shiftFunctor C n ⋙ L)
Tactic: rw [← Localization.functor_linear_iff L W R (shiftFunctor C n ⋙ L) (shiftFunctor D n)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v₁, u₁, w} C A
inst_3 : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
| W f
have rw : W.inverseImage (shiftFunctor C a) f
Tactic: rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Localization (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v₁, u₁, w} C A
inst_3 : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
⊢ W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) (Functor.map (shiftFunctor C a) f) ↔ W f
have conv_rhs : W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) (Functor.map (shiftFunctor C a) f) ↔
  W.inverseImage (shiftFunctor C a) f
Tactic: conv_rhs => rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]
-- 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
inst_6 : W.IsCompatibleWithShift A
a : A
⊢ W ≤ W.inverseImage (shiftFunctor C a)
have rw : W ≤ W
Tactic: rw [MorphismProperty.IsCompatibleWithShift.condition]
-- 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
⊢ Eq (α := shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F' ≅ F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0)
    (commShiftOfLocalization.iso L W F F' 0) (CommShift.isoZero F' A)
have w : Eq (α := shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F' ⟶ F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0)
  (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (Iso.hom (CommShift.isoZero F' A))
Tactic: ext1
-- 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
⊢ Eq (α := shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F' ⟶ F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0)
    (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (Iso.hom (CommShift.isoZero F' A))
have w : ∀ (X : C),
  Eq (α :=
    (shiftFunctor.{v₂, u₂, w} D (A := A) 0 ⋙ F').obj (L.obj X) ⟶
      (F' ⋙ shiftFunctor.{v₃, u₃, w} E (A := A) 0).obj (L.obj X))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (L.obj X))
    (NatTrans.app (Iso.hom (CommShift.isoZero F' A)) (L.obj X))
Tactic: apply natTrans_ext L W
-- 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
X : C
⊢ Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' 0)) (L.obj X))
    (NatTrans.app (Iso.hom (CommShift.isoZero F' A)) (L.obj X))
have w : Eq (α :=
  F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
    obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
  (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
    CategoryStruct.comp (Y := F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w} C (A := A) 0) X)))
      (F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
      ((L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
        (Lifting.iso L W F F').hom.app X ≫
          map (𝟭 E) ((Lifting.iso L W F F').inv.app X) ≫
            NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X))))
  (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
    NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X)))
Tactic: simp only [commShiftOfLocalization.iso_hom_app, comp_obj, commShiftIso_zero,
      CommShift.isoZero_inv_app, map_comp, CommShift.isoZero_hom_app, Category.assoc,
      ← NatTrans.naturality_assoc, ← NatTrans.naturality]
-- 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
X : C
⊢ Eq (α :=
    F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
      obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      CategoryStruct.comp (Y := F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w} C (A := A) 0) X)))
        (F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
        ((L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X) ≫
          (Lifting.iso L W F F').hom.app X ≫
            map (𝟭 E) ((Lifting.iso L W F F').inv.app X) ≫
              NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X))))
    (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X)))
have w : Eq (α :=
  F'.obj (obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w} D (A := A) 0) (L.obj X)) ⟶
    obj.{v₃, v₃, u₃, u₃} (shiftFunctor.{v₃, u₃, w} E (A := A) 0) (F'.obj (L.obj X)))
  (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
    CategoryStruct.comp (Y := F'.obj (L.obj (obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w} C (A := A) 0) X)))
      (F'.map (L.map (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X)))
      (F'.map (L.map (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X)) ≫
        (Lifting.iso L W F F').hom.app X ≫
          (Lifting.iso L W F F').inv.app X ≫ NatTrans.app (Iso.inv (shiftFunctorZero E A)) (F'.obj (L.obj X))))
  (F'.map (NatTrans.app (Iso.hom (shiftFunctorZero D A)) (L.obj X)) ≫
    NatTrans.app (Iso.inv (shiftFunctorZero E A)) (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
⊢ Eq (α := shiftFunctor D (a + b) ⋙ F' ≅ F' ⋙ shiftFunctor E (a + b)) (commShiftOfLocalization.iso L W F F' (a + b))
    (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b))
have w : Eq (α := shiftFunctor D (a + b) ⋙ F' ⟶ F' ⋙ shiftFunctor E (a + b))
  (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b)))
  (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))
Tactic: ext1
-- 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
⊢ Eq (α := shiftFunctor D (a + b) ⋙ F' ⟶ F' ⋙ shiftFunctor E (a + b))
    (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b)))
    (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor D (a + b) ⋙ F').obj (L.obj X) ⟶ (F' ⋙ shiftFunctor E (a + b)).obj (L.obj X))
    (NatTrans.app (Iso.hom (commShiftOfLocalization.iso L W F F' (a + b))) (L.obj X))
    (NatTrans.app
      (Iso.hom (CommShift.isoAdd (commShiftOfLocalization.iso L W F F' a) (commShiftOfLocalization.iso L W F F' b)))
      (L.obj X))
Tactic: apply natTrans_ext L W
-- 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 : 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)) ≫
    (L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) 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)) ≫
        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)
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
| 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)) ≫
      (L ⋙ F').map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) 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)) ≫
          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 dsimp : 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)) ≫
    F'.map (L.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) 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)) ≫
        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)
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 (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)) ≫
      F'.map (L.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) 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)) ≫
          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 rw : F'.map
    (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
      L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a ⋙ shiftFunctor C b) 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)) ≫
    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)
Tactic: rw [← Functor.map_comp_assoc, ← map_comp_assoc, Category.assoc,
        ← map_comp, Iso.inv_hom_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
      (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a ⋙ shiftFunctor C b) 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)) ≫
      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 dsimp : F'.map
    (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
      L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C 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)) ≫
    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)
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
      (NatTrans.app (Iso.inv (commShiftIso L b)) (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X) ≫
        L.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (shiftFunctor C 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)) ≫
      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 rw : 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)) ≫
    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) ≫
        map (shiftFunctor E a ⋙ shiftFunctor E b) ((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, Category.comp_id, ← NatTrans.naturality]
-- 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 (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)) ≫
      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) ≫
          map (shiftFunctor E a ⋙ shiftFunctor E b) ((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 (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: dsimp