awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = a''
have rw : m + n + a = m + a'
Tactic: rw [← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = m + a'
⊢ m + n + a = a''
have rw₁ : m + n + a = m + (n + a)
Tactic: rw [← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = m + a'
rw₁ : m + n + a = m + (n + a)
⊢ m + n + a = a''
have rw₂ : m + (n + a) = m + (n + a)
Tactic: rw [← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ m + n + a = a''
have rw : m + (n + a) = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + (n + a) = a''
rw₁ : m + a' = a''
⊢ m + n + a = a''
have rw₂ : a'' = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = a''
have rw : m + (n + a) = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + (n + a) = a''
rw₁ : m + a' = a''
⊢ m + n + a = a''
have rw₂ : a'' = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''
have rw : m + n + a = a''
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + n + a = a''
⊢ mn + a = a''
have rw₁ : m + n + a = m + a'
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
⊢ mn + a = a''
have rw₂ : m + n + a = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
rw₂ : m + n + a = m + (n + a)
⊢ mn + a = a''
have rw₃ : m + (n + a) = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso mn a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n mn hnm) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
have subst : F.shiftIso (m + n) a a'' sorry =
  isoWhiskerRight (shiftFunctorAdd' C m n (m + n) sorry) (F.shift a) ≪≫
    associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
      isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
Tactic: subst hnm
Cleared hypotheses: mn, hnm
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n (m + n) ⋯) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
have rw : F.shiftIso (m + n) a a'' sorry =
  isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
    associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
      isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw :
  F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n (m + n) ⋯) (F.shift a) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
        isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
have rw₁ : isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
    associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
      isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha'' =
  isoWhiskerRight (shiftFunctorAdd C m n) (F.shift a) ≪≫
    associator (shiftFunctor C m) (shiftFunctor C n) (F.shift a) ≪≫
      isoWhiskerLeft (shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ mn + a = a''
have rw : m + n + a = a''
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = a''
⊢ mn + a = a''
have rw₁ : m + n + a = m + a'
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
⊢ mn + a = a''
have rw₂ : m + n + a = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
rw₂ : m + n + a = m + (n + a)
⊢ mn + a = a''
have rw₃ : m + (n + a) = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) X
have rw : NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
    NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
  (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
    (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
Tactic: rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) X
have rw₁ : NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
    NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
  (F.shift a).map
      (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
    NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
Tactic: rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₁ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) X
have rw₂ : NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
    NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
  (F.shift a).map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n) X)) ≫
    NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
Tactic: rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₁ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₂ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n) X)) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) X
have rw₃ : NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
    NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
  𝟙 ((F.shift a).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n) X)) ≫
    NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
Tactic: rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
inst_4 : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      (F.shift a).map (NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₁ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₂ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (𝟙 (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n) X)) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
rw₃ :
  NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    𝟙 ((F.shift a).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m ⋙ shiftFunctor C n) X)) ≫
      NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X
⊢ NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X =
    (F.shift a).map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n mn hnm)) X) ≫
      NatTrans.app (Iso.hom (F.shiftIso mn a a'' ⋯)) X
have rw₄ : Eq (α := (shiftFunctor C n ⋙ F.shift a).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ⟶ (F.shift a'').obj X)
  (NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
    NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X)
  (NatTrans.app (Iso.hom (F.shiftIso n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
    NatTrans.app (Iso.hom (F.shiftIso m a' a'' ha'')) X)
Tactic: rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''
have rw : mn + a = m + a'
Tactic: rw [← ha'', ← ha', ← hnm, add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
inst_6 : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
rw : mn + a = m + a'
⊢ mn + a = a''
have rw₁ : mn + a = m + (n + a)
Tactic: rw [← ha'', ← ha', ← hnm, add_assoc]