awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
⊢ Eq (α := shiftFunctor C (a + b) ⋙ F ≅ F ⋙ shiftFunctor D (a + b)) (Iso.symm (i (a + b)))
    (isoAdd (i a).symm (i b).symm)
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ s (a + b)).obj X) (NatTrans.app (Iso.hom (Iso.symm (i (a + b)))) X)
    (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
⊢ Eq (α := (shiftFunctor C (a + b) ⋙ F).obj X ⟶ (F ⋙ s (a + b)).obj X) (NatTrans.app (Iso.hom (Iso.symm (i (a + b)))) X)
    (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)
have w : Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶ (s (a + b)).obj (F.obj X))
  (NatTrans.app (Iso.inv (i (a + b))) X) (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
⊢ Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶ (s (a + b)).obj (F.obj X))
    (NatTrans.app (Iso.inv (i (a + b))) X) (NatTrans.app (Iso.hom (isoAdd (i a).symm (i b).symm)) X)
have w : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      (s b).map ((i a).inv.app X) ≫
        (s b).map ((i a).hom.app X) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: simp only [isoAdd_hom_app, Iso.symm_hom, shiftFunctorAdd_inv_app_obj_of_induced,
          shiftFunctor_of_induced]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map ((i a).inv.app X) ≫
          (s b).map ((i a).hom.app X) ≫
            (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
              F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      (s b).map (𝟙 ((shiftFunctor C a ⋙ F).obj X)) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: rw [← Functor.map_comp_assoc, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 ((shiftFunctor C a ⋙ F).obj X)) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w₁ : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₁ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w₂ : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
    F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₁ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₂ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w₃ : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
    NatTrans.app (Iso.inv (i (a + b))) X
Tactic: rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₁ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₂ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₃ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w₄ : NatTrans.app (Iso.inv (i (a + b))) X =
  F.map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₁ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₂ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₃ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      NatTrans.app (Iso.inv (i (a + b))) X
w₄ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w₅ : NatTrans.app (Iso.inv (i (a + b))) X =
  𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
this : HasShift.{v_2, u_2, u_3} D A := HasShift.induced F A s i
a b : A
X : C
w :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        𝟙 ((s b).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₁ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₂ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₃ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X ≫ NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫
      NatTrans.app (Iso.inv (i (a + b))) X
w₄ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ≫ NatTrans.app (Iso.inv (i (a + b))) X
w₅ :
  NatTrans.app (Iso.inv (i (a + b))) X =
    𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X)) ≫ NatTrans.app (Iso.inv (i (a + b))) X
⊢ NatTrans.app (Iso.inv (i (a + b))) X =
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
      (i b).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
        (s b).map (𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X))) ≫
          (i b).hom.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have w₆ : Eq (α := F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (a + b)) X) ⟶ (s (a + b)).obj (F.obj X))
  (NatTrans.app (Iso.inv (i (a + b))) X) (NatTrans.app (Iso.inv (i (a + b))) X)
Tactic: rw [Functor.map_id, Category.id_comp, Iso.inv_hom_id_app_assoc,
          ← F.map_comp_assoc, Iso.hom_inv_id_app, F.map_id, Category.id_comp]
-- 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
⊢ Functor.Linear.{u_1, v_2, u_2, v_2, u_2} R (shiftFunctor D n)
have have : ∀ (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)
Tactic: have : Localization.Lifting L W (shiftFunctor C n ⋙ L) (shiftFunctor D n) :=
    ⟨(L.commShiftIso n).symm⟩