awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C m₃)
        (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
    (NatTrans.app
        (Iso.hom
          (Iso.symm (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) ⋯) ≪≫
            shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) ⋯))
        X ≫
      map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) X) ≫
        NatTrans.app (Iso.inv (Iso.symm (shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) ⋯) ≪≫ shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) ⋯))
            (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
          map (shiftFunctor C m₃)
            (NatTrans.app
              (Iso.inv (Iso.symm (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯) ≪≫ shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) ⋯)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C m₁) X))
have dsimp : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C (m₂ + m₃)) (obj.{v, v, u, u} (shiftFunctor C m₁) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C m₃)
      (obj.{v, v, u, u} (shiftFunctor C m₂) (obj.{v, v, u, u} (shiftFunctor C m₁) X)))
  ((NatTrans.app (Iso.inv (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + (m₂ + m₃)) sorry)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C (m₂ + m₃) m₁ (m₁ + (m₂ + m₃)) sorry)) X) ≫
    map (shiftFunctor C m₁) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) sorry)) X) ≫
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C m₃ m₁ (m₁ + m₃) sorry)) (obj.{v, v, u, u} (shiftFunctor C m₂) X) ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₃ (m₁ + m₃) sorry)) (obj.{v, v, u, u} (shiftFunctor C m₂) X)) ≫
        map (shiftFunctor C m₃)
          (NatTrans.app (Iso.inv (shiftFunctorAdd' C m₂ m₁ (m₁ + m₂) sorry)) X ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) sorry)) X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) sorry)) (obj.{v, v, u, u} (shiftFunctor C m₁) X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
⊢ m₂ + m₁ + m₃ = m₁ + (m₂ + m₃)
have rw : m₁ + m₂ + m₃ = m₁ + (m₂ + m₃)
Tactic: rw [add_comm m₂ m₁, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
rw : m₁ + m₂ + m₃ = m₁ + (m₂ + m₃)
⊢ m₂ + m₁ + m₃ = m₁ + (m₂ + m₃)
have rw₁ : m₁ + (m₂ + m₃) = m₁ + (m₂ + m₃)
Tactic: rw [add_comm m₂ m₁, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddCommMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X_1 Y : C
f : X_1 ⟶ Y
m n : A
hmn : m + n = 0
X : C
rw : m + n = 0
⊢ n + m = 0
have rw₁ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [add_comm, hmn]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).hom.app X) =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
        map (shiftFunctor D b) ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)
have dsimp : F.map
    (hF.preimage
      (NatTrans.app (Iso.hom (i (a + b))) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
          𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D a) (F.obj X))) ≫
            map (shiftFunctor D b) ((i a).inv.app X) ≫
              𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (F.obj ((s a).obj X))) ≫
                (i b).inv.app ((s a).obj X) ≫ 𝟙 (F.obj ((s b).obj ((s a).obj X))))) =
  NatTrans.app (Iso.hom (i (a + b))) X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd D a b)) (F.obj X) ≫
      map (shiftFunctor D b) ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)
Tactic: dsimp [add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).inv.app X) =
    (i b).hom.app ((s a).obj X) ≫
      map (shiftFunctor D b) ((i a).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have dsimp : F.map
    (hF.preimage
      ((((((𝟙 (F.obj ((s b).obj ((s a).obj X))) ≫ (i b).hom.app ((s a).obj X)) ≫
                𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (F.obj ((s a).obj X)))) ≫
              map (shiftFunctor D b) ((i a).hom.app X)) ≫
            𝟙 (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D b) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D a) (F.obj X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X)) ≫
        NatTrans.app (Iso.inv (i (a + b))) X)) =
  (i b).hom.app ((s a).obj X) ≫
    map (shiftFunctor D b) ((i a).hom.app X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd D a b)) (F.obj X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
Tactic: dsimp [add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (hypothesis)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
⊢ F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))
have h : Eq.{v_1 + 1} (α :=
  obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
      (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' D (m₁ + m₂) m₃ (m₁ + m₂ + m₃) sorry)) (F.obj X) ≫
      map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ m₂ (m₁ + m₂) sorry)) (F.obj X)) :
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) sorry)) (F.obj X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' D m₂ m₃ (m₂ + m₃) sorry))
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
Tactic: have h := shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl (F.obj X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (hypothesis)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ m₂ (m₁ + m₂) ⋯)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' D m₂ m₃ (m₂ + m₃) ⋯))
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
⊢ F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))
have h₁ : Eq.{v_1 + 1} (α :=
  obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
      (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
      map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) sorry)) (F.obj X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
Tactic: simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
⊢ F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))
have rw : F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫
    (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
  F.map (eqToHom sorry ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X)) ≫
    (i m₃).hom.app ((s m₂).obj ((s m₁).obj X))
Tactic: rw [← cancel_mono ((i m₃).hom.app ((s m₂).obj ((s m₁).obj X)))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
⊢ F.map (NatTrans.app (Iso.hom (add hF s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
    F.map (eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add hF s i m₁ (m₂ + m₃))) X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X)) ≫
      (i m₃).hom.app ((s m₂).obj ((s m₁).obj X))
have simp : NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
      map (shiftFunctor D m₃) (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫
        (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
          F.map ((s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫ (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
  F.map (eqToHom sorry) ≫
    NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ (m₂ + m₃))) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) ≫
          map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X)) ≫
            map (shiftFunctor D m₃) ((i m₂).inv.app ((s m₁).obj X))
Tactic: simp only [Functor.comp_obj, Functor.map_comp, map_add_hom_app,
          Category.assoc, Iso.inv_hom_id_app_assoc, NatTrans.naturality_assoc, Functor.comp_map,
          Iso.inv_hom_id_app, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
h :
  Eq.{v_1 + 1} (α :=
    obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
        (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ m₂)) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁ ⋙ shiftFunctor D m₂) (F.obj X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' D m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) :
      obj.{v_1, v_1, u_2, u_2} (shiftFunctor D (m₁ + m₂ + m₃)) (F.obj X) ⟶
        obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₂ ⋙ shiftFunctor D m₃)
          (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)))
⊢ NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
        map (shiftFunctor D m₃) (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫
          (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
            F.map ((s m₃).map ((add hF s i m₁ m₂).hom.app X)) ≫ (i m₃).hom.app ((s m₂).obj ((s m₁).obj X)) =
    F.map (eqToHom ⋯) ≫
      NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ (m₂ + m₃))) (F.obj X) ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) ≫
            map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X)) ≫
              map (shiftFunctor D m₃) ((i m₂).inv.app ((s m₁).obj X))
have erw : NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd D (m₁ + m₂) m₃)) (F.obj X) ≫
      map (shiftFunctor D m₃) (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫
        (i m₃).inv.app ((s (m₁ + m₂)).obj X) ≫
          (i m₃).hom.app ((s (m₁ + m₂)).obj X) ≫ (F ⋙ shiftFunctor D m₃).map ((add hF s i m₁ m₂).hom.app X) =
  F.map (eqToHom sorry) ≫
    NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd D m₁ (m₂ + m₃))) (F.obj X) ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd D m₂ m₃)) (obj.{v_1, v_1, u_2, u_2} (shiftFunctor D m₁) (F.obj X)) ≫
          map (shiftFunctor D m₃) (map (shiftFunctor D m₂) ((i m₁).inv.app X)) ≫
            map (shiftFunctor D m₃) ((i m₂).inv.app ((s m₁).obj X))
Tactic: erw [(i m₃).hom.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (hypothesis)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
⊢ F.map (NatTrans.app (Iso.hom (add hF s i 0 n)) X) = F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X))
have this : Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
  (eqToHom sorry ≫ (i n).hom.app X ≫ eqToHom sorry)
Tactic: have this := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
⊢ F.map (NatTrans.app (Iso.hom (add hF s i 0 n)) X) = F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X))
have rw : F.map (NatTrans.app (Iso.hom (add hF s i 0 n)) X) ≫ (i n).hom.app ((s 0).obj X) =
  F.map (eqToHom sorry ≫ (s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
Tactic: rw [← cancel_mono ((i n).hom.app ((s 0).obj X))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
⊢ F.map (NatTrans.app (Iso.hom (add hF s i 0 n)) X) ≫ (i n).hom.app ((s 0).obj X) =
    F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
have simp : Eq.{v_1 + 1} (α := F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
  (eqToHom sorry ≫
      (i n).hom.app X ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
          map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) :
    F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
  (eqToHom sorry ≫ F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X) :
    F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
Tactic: simp only [comp_obj, map_add_hom_app, this, shiftFunctorAdd_zero_add_hom_app, id_obj,
          Category.assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Iso.inv_hom_id_app,
          Category.comp_id, map_comp, eqToHom_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
⊢ Eq.{v_1 + 1} (α := F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
    (eqToHom ⋯ ≫
        (i n).hom.app X ≫
          map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
            map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) :
      F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
    (eqToHom ⋯ ≫ F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X) :
      F.obj ((s (0 + n)).obj X) ⟶ obj.{v_1, v_1, u_2, u_2} (shiftFunctor D n) (F.obj ((s 0).obj X)))
have e_a : (i n).hom.app X ≫
    map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) =
  F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
D : Type u_2
inst_1 : Category.{v_1, u_2} D
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_1} D A
F : Functor.{v, v_1, u, u_2} C D
hF : F.FullyFaithful
s : A → Functor.{v, v, u, u} C C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
n : A
X : C
this :
  Eq (α := (s (0 + n) ⋙ F).obj X ⟶ (F ⋙ shiftFunctor D (0 + n)).obj X) (NatTrans.app (Iso.hom (i (0 + n))) X)
    (eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯)
⊢ (i n).hom.app X ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) =
    F.map ((s n).map ((zero hF s i).inv.app X)) ≫ (i n).hom.app ((s 0).obj X)
have e_a : (i n).hom.app X ≫
    map (shiftFunctor D n) (NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X)) ≫
      map (shiftFunctor D n) (NatTrans.app (Iso.inv (i 0)) X) =
  (i n).hom.app X ≫ (F ⋙ shiftFunctor D n).map ((zero hF s i).inv.app X)
Tactic: erw [(i n).hom.naturality]