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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ Eq.{v + 1} (α := obj.{v, v, u, u} (𝟭 C) X ⟶ obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C p' p hp)) X)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n' n hn)) X ≫
      CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (shiftFunctor C n)
          (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X)))
        (map (shiftFunctor C n)
            (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C m' m hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) :
          obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n') X) ⟶
            obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X)))
        (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X) :
          obj.{v, v, u, u} (shiftFunctor C n)
              (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X)) ⟶
            obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)))
have dsimp : Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
  (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
  ((NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X) ≫
    map (shiftFunctor C n)
        (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X) ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X))
Tactic: dsimp [shiftFunctorCompIsoId]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    ((NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X) ≫
      map (shiftFunctor C n)
          (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X) ≫
            NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))
have simp : Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
  (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
  (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X))
Tactic: simp only [Functor.map_comp, Category.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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ Eq.{v + 1} (α := X ⟶ obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero C A)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C n)
              (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
              map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))
have e_a : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
    obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
    map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
      map (shiftFunctor C n)
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) 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
inst_1 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X))
have e_a : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
    obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
    map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
      map (shiftFunctor C n)
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C m ⋙ shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h)) (obj.{v, v, u, u} (shiftFunctor C p') X))
Tactic: rw [← NatTrans.naturality]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
      map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C m ⋙ shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h)) (obj.{v, v, u, u} (shiftFunctor C p') X))
have e_a : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
    obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C p' p 0 hp)) X)
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' n 0 hn)) X ≫
    CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (shiftFunctor C n)
        (obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) (obj.{v, v, u, u} (shiftFunctor C n') X)))
      (map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n') X)))
      (map (shiftFunctor C n)
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C m' m 0 hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n) (map (shiftFunctor C m) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h)) (obj.{v, v, u, u} (shiftFunctor C p') 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ p' + m = n'
have rw : p' + m + n = n' + n
Tactic: rw [← add_left_inj n, hn, add_assoc, h, hp]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : p' + m + n = n' + n
⊢ p' + m = n'
have rw₁ : p' + m + n = 0
Tactic: rw [← add_left_inj n, hn, add_assoc, h, hp]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : p' + m + n = n' + n
rw₁ : p' + m + n = 0
⊢ p' + m = n'
have rw₂ : p' + (m + n) = 0
Tactic: rw [← add_left_inj n, hn, add_assoc, h, hp]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : p' + m + n = n' + n
rw₁ : p' + m + n = 0
rw₂ : p' + (m + n) = 0
rw₃ : p' + p = 0
⊢ p' + m = n'
have rw₄ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [← add_left_inj n, hn, add_assoc, h, hp]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ p' + m + n = 0
have rw : p' + (m + n) = 0
Tactic: rw [add_assoc, h, hp]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : p' + (m + n) = 0
rw₁ : p' + p = 0
⊢ p' + m + n = 0
have rw₂ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [add_assoc, h, hp]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' + m = n'
have rw : n' + (m' + m) = n'
Tactic: rw [add_assoc, hm, add_zero]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + (m' + m) = n'
⊢ n' + m' + m = n'
have rw₁ : n' + 0 = n'
Tactic: rw [add_assoc, hm, add_zero]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + (m' + m) = n'
rw₁ : n' + 0 = n'
⊢ n' + m' + m = n'
have rw₂ : n' = n'
Tactic: rw [add_assoc, hm, add_zero]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' = p'
have rw : n' + m' + p = p' + p
Tactic: rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + m' + p = p' + p
⊢ n' + m' = p'
have rw₁ : n' + m' + p = 0
Tactic: rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + m' + p = p' + p
rw₁ : n' + m' + p = 0
⊢ n' + m' = p'
have rw₂ : n' + m' + (m + n) = 0
Tactic: rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + m' + p = p' + p
rw₁ : n' + m' + p = 0
rw₂ : n' + m' + (m + n) = 0
⊢ n' + m' = p'
have rw₃ : n' + (m' + (m + n)) = 0
Tactic: rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + m' + p = p' + p
rw₁ : n' + m' + p = 0
rw₂ : n' + m' + (m + n) = 0
rw₃ : n' + (m' + (m + n)) = 0
⊢ n' + m' = p'
have rw₄ : n' + (m' + m + n) = 0
Tactic: rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + m' + p = p' + p
rw₁ : n' + m' + p = 0
rw₂ : n' + m' + (m + n) = 0
rw₃ : n' + (m' + (m + n)) = 0
rw₄ : n' + (m' + m + n) = 0
⊢ n' + m' = p'
have rw₅ : n' + (0 + n) = 0
Tactic: rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
rw : n' + m' + p = p' + p
rw₁ : n' + m' + p = 0
rw₂ : n' + m' + (m + n) = 0
rw₃ : n' + (m' + (m + n)) = 0
rw₄ : n' + (m' + m + n) = 0
rw₅ : n' + (0 + n) = 0
rw₆ : n' + n = 0
⊢ n' + m' = p'
have rw₇ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ Eq.{v + 1} (α := obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X ⟶ obj.{v, v, u, u} (𝟭 C) X)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C p' p hp)) X)
    (map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m' m hm)) (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n' n hn)) X)
have rw : 𝟙 (obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X) =
  map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' sorry)) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
        (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
      map (shiftFunctor C n)
          (𝟙 (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X)
Tactic: rw [← cancel_mono ((shiftFunctorCompIsoId C p' p hp).inv.app X), Iso.hom_inv_id_app,
    shiftFunctorCompIsoId_add'_inv_app m n p m' n' p' hm hn hp h,
    Category.assoc, Category.assoc, Category.assoc, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app]
-- 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C p' ⋙ shiftFunctor C p) X) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙 (obj.{v, v, u, u} (shiftFunctor C m' ⋙ shiftFunctor C m) (obj.{v, v, u, u} (shiftFunctor C n') X))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
have dsimp : 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
  map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' sorry)) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
        (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
      map (shiftFunctor C n)
          (𝟙
            (obj.{v, v, u, u} (shiftFunctor C m)
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) 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 : AddGroup A
inst_2 : HasShift.{v, u, u_1} C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
    map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' ⋯)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
          (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
        map (shiftFunctor C n)
            (𝟙
              (obj.{v, v, u, u} (shiftFunctor C m)
                (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
            map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' ⋯)) X)
have rw : 𝟙 (obj.{v, v, u, u} (shiftFunctor C p) (obj.{v, v, u, u} (shiftFunctor C p') X)) =
  map (shiftFunctor C p) (NatTrans.app (Iso.hom (shiftFunctorAdd' C n' m' p' sorry)) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C m n p h))
        (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
      𝟙
          (obj.{v, v, u, u} (shiftFunctor C n)
            (obj.{v, v, u, u} (shiftFunctor C m)
              (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)))) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m n p h))
            (obj.{v, v, u, u} (shiftFunctor C m') (obj.{v, v, u, u} (shiftFunctor C n') X)) ≫
          map (shiftFunctor C p) (NatTrans.app (Iso.inv (shiftFunctorAdd' C n' m' p' sorry)) X)
Tactic: rw [Functor.map_id, Category.id_comp, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]