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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃) X)
    (NatTrans.app
      (Iso.hom
        (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯ ≪≫
          isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯) (shiftFunctor C a₃) ≪≫
            associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃)))
      X)
    (NatTrans.app
      (Iso.hom
        (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫
          isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)))
      X)
have w : NatTrans.app (Iso.hom (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) sorry)) X ≫
    map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) sorry)) X) ≫
      𝟙
        (obj.{v, v, u, u} (shiftFunctor C a₃)
          (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X))) =
  NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) sorry)) X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) sorry)) (obj.{v, v, u, u} (shiftFunctor C a₁) 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
X : C
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C (a₁ + a₂) a₃ (a₁ + a₂ + a₃) ⋯)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ a₂ (a₁ + a₂) ⋯)) X) ≫
        𝟙
          (obj.{v, v, u, u} (shiftFunctor C a₃)
            (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X))) =
    NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a₂ a₃ (a₂ + a₃) ⋯)) (obj.{v, v, u, u} (shiftFunctor C a₁) X)
have w : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
    obj.{v, v, u, u} (shiftFunctor C a₃)
      (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
    map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
  (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) sorry)) X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
Tactic: simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, 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
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
have w : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
    obj.{v, v, u, u} (shiftFunctor C a₃)
      (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
    map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
  ((NatTrans.app (eqToHom sorry) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ (a₂ + a₃))) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
Tactic: dsimp [shiftFunctorAdd']
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₃)
        (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
      map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
    ((NatTrans.app (eqToHom ⋯) X ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ (a₂ + a₃))) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
have w : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
    obj.{v, v, u, u} (shiftFunctor C a₃)
      (obj.{v, v, u, u} (shiftFunctor C a₂) (obj.{v, v, u, u} (shiftFunctor C a₁) X)))
  (NatTrans.app (Iso.hom (shiftFunctorAdd C (a₁ + a₂) a₃)) X ≫
    map (shiftFunctor C a₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ a₂)) X))
  ((eqToHom sorry ≫ NatTrans.app (Iso.hom (shiftFunctorAdd C a₁ (a₂ + a₃))) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd C a₂ a₃)) (obj.{v, v, u, u} (shiftFunctor C a₁) X))
Tactic: simp only [eqToHom_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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ : A
⊢ Eq (α :=
    Iso (C := Functor.{v, v, u, u} C C) (shiftFunctor C (a₁ + a₂ + a₃))
      (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃))
    (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
        associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃))
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫ isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃))
have w : ∀ (X : C),
  Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C (a₁ + a₂ + a₃)) X ⟶
      obj.{v, v, u, u} (shiftFunctor C a₁ ⋙ shiftFunctor C a₂ ⋙ shiftFunctor C a₃) X)
    (NatTrans.app
      (Iso.hom
        (shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
          isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
            associator (shiftFunctor C a₁) (shiftFunctor C a₂) (shiftFunctor C a₃)))
      X)
    (NatTrans.app
      (Iso.hom
        (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) sorry ≪≫
          isoWhiskerLeft (shiftFunctor C a₁) (shiftFunctorAdd C a₂ a₃)))
      X)
Tactic: ext X
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (shiftFunctor C (0 + a)) X = obj.{v, v, u, u} (shiftFunctor C a) (obj.{v, v, u, u} (𝟭 C) X)
have dsimp : obj.{v, v, u, u} (shiftFunctor C (0 + a)) X = obj.{v, v, u, u} (shiftFunctor C a) 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (shiftFunctor C (0 + a)) X = obj.{v, v, u, u} (shiftFunctor C a) X
have rw : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
Tactic: rw [zero_add]
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (shiftFunctor C a) (obj.{v, v, u, u} (𝟭 C) X) = obj.{v, v, u, u} (shiftFunctor C (0 + a)) X
have dsimp : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (0 + a)) 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (0 + a)) X
have rw : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
Tactic: rw [zero_add]
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (shiftFunctor C (a + 0)) X = obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C a) X)
have dsimp : obj.{v, v, u, u} (shiftFunctor C (a + 0)) X = obj.{v, v, u, u} (shiftFunctor C a) 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (shiftFunctor C (a + 0)) X = obj.{v, v, u, u} (shiftFunctor C a) X
have rw : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
Tactic: rw [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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C a) X) = obj.{v, v, u, u} (shiftFunctor C (a + 0)) X
have dsimp : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (a + 0)) 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a : A
X : C
⊢ obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C (a + 0)) X
have rw : obj.{v, v, u, u} (shiftFunctor C a) X = obj.{v, v, u, u} (shiftFunctor C a) X
Tactic: rw [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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
rw : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁₂ + a₃ = a₁₂₃
have rw₁ : a₁₂₃ = a₁₂₃
Tactic: rw [← h₁₂, h₁₂₃]
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃
have rw : a₁ + (a₂ + a₃) = a₁₂₃
Tactic: rw [← h₂₃, ← add_assoc, h₁₂₃]
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
rw : a₁ + (a₂ + a₃) = a₁₂₃
rw₁ : a₁ + a₂ + a₃ = a₁₂₃
⊢ a₁ + a₂₃ = a₁₂₃
have rw₂ : a₁₂₃ = a₁₂₃
Tactic: rw [← h₂₃, ← add_assoc, h₁₂₃]
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
    (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f) (Iso.hom (shiftZero A X) ≫ f ≫ Iso.inv (shiftZero A Y))
have symm : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
  (Iso.hom (shiftZero A X) ≫ f ≫ Iso.inv (shiftZero A Y)) (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f)
Tactic: symm
-- 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 : AddMonoid A
inst_2 : HasShift.{v, u, u_1} C A
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
      obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
    (Iso.hom (shiftZero A X) ≫ f ≫ Iso.inv (shiftZero A Y)) (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f)
have rw : Eq (α :=
  obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) X ⟶
    obj.{v, v, u, u} (shiftFunctor.{v, u, u_1} C (A := A) 0) Y)
  (NatTrans.app (Iso.hom (shiftFunctorZero C A)) X ≫ f ≫ NatTrans.app (Iso.inv (shiftFunctorZero C A)) Y)
  (map (shiftFunctor.{v, u, u_1} C (A := A) 0) f)
Tactic: rw [Iso.app_inv, Iso.app_hom]
-- 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
i j : A
h : i + j = 0
⊢ j + i = 0
have rw : j + i + j = 0 + j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
rw : j + i + j = 0 + j
⊢ j + i = 0
have rw₁ : j + (i + j) = 0 + j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
⊢ j + i = 0
have rw₂ : j + 0 = 0 + j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
rw₂ : j + 0 = 0 + j
⊢ j + i = 0
have rw₃ : j + 0 = j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
rw₂ : j + 0 = 0 + j
rw₃ : j + 0 = j
⊢ j + i = 0
have rw₄ : j = j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
X : C
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := j : Discrete A } { as := i : Discrete A }).as =
    Discrete.as (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))
have dsimp : j + i = 0
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
i j : A
h : i + j = 0
X : C
⊢ j + i = 0
have rw : j + i + j = 0 + j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
X : C
rw : j + i + j = 0 + j
⊢ j + i = 0
have rw₁ : j + (i + j) = 0 + j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
X : C
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
⊢ j + i = 0
have rw₂ : j + 0 = 0 + j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
X : C
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
rw₂ : j + 0 = 0 + j
⊢ j + i = 0
have rw₃ : j + 0 = j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i j : A
h : i + j = 0
X : C
rw : j + i + j = 0 + j
rw₁ : j + (i + j) = 0 + j
rw₂ : j + 0 = 0 + j
rw₃ : j + 0 = j
⊢ j + i = 0
have rw₄ : j = j
Tactic: rw [← add_left_inj j, add_assoc, h, zero_add, 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
i : A
⊢ IsEquivalence.{v, v, u, u} (shiftFunctor C i)
have change : IsEquivalence.{v, v, u, u} (Equivalence.functor (shiftEquiv C i))
Tactic: change (shiftEquiv C i).functor.IsEquivalence
-- 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_1 Y : C
f : X_1 ⟶ Y
n m : A
h : n + m = 0
X : C
⊢ m + n = 0
have rw : m + -m = 0
Tactic: rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]
-- 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_1 Y : C
f : X_1 ⟶ Y
n m : A
h : n + m = 0
X : C
rw : m + -m = 0
⊢ m + n = 0
have rw₁ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]
-- 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
n m : A
h : n + m = 0
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C m) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C n m h)) X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C m n ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X))
have dsimp : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C n) (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) X)
  (map (shiftFunctor C n)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' C n m 0 h)) X ≫ NatTrans.app (Iso.hom (shiftFunctorZero C A)) X))
  (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n 0 sorry)) (obj.{v, v, u, u} (shiftFunctor C n) X) ≫
    NatTrans.app (Iso.hom (shiftFunctorZero C A)) (obj.{v, v, u, u} (shiftFunctor C n) 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
n m : A
h : n + m = 0
X : C
⊢ m + n = 0
have rw : m + -m = 0
Tactic: rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]
-- 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
n m : A
h : n + m = 0
X : C
rw : m + -m = 0
⊢ m + n = 0
have rw₁ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [← neg_eq_of_add_eq_zero_left h, add_neg_cancel]
-- 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
n m : A
h : n + m = 0
X : C
⊢ n + m + n = n
have rw : 0 + n = n
Tactic: rw [h, zero_add]
-- 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
n m : A
h : n + m = 0
X : C
rw : 0 + n = n
⊢ n + m + n = n
have rw₁ : n = n
Tactic: rw [h, zero_add]
-- 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
n m : A
h : n + m = 0
X : C
⊢ Eq.{v + 1} (α :=
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X) ⟶
      obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (shiftFunctor C n ⋙ shiftFunctor C m) X))
    (map (shiftFunctor C n) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C n m h)) X))
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C m n ⋯)) (obj.{v, v, u, u} (shiftFunctor C n) X))
have rw : Eq.{v + 1} (α :=
  obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X) ⟶
    obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X))
  (𝟙 (obj.{v, v, u, u} (shiftFunctor C n) (obj.{v, v, u, u} (𝟭 C) X)))
  (𝟙 (obj.{v, v, u, u} (𝟭 C) (obj.{v, v, u, u} (shiftFunctor C n) X)))
Tactic: rw [← cancel_mono (((shiftFunctorCompIsoId C n m h).hom.app X)⟦n⟧'),
    ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id,
    shift_shiftFunctorCompIsoId_hom_app, Iso.inv_hom_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 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]