awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a : M
ha : a = 0
d : M
h : ShiftedHom Z T d
⊢ d + a = d
have rw : d + 0 = d
Tactic: rw [ha, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
M : Type u_4
inst_3 : AddMonoid M
inst_4 : HasShift.{v_1, u_1, u_4} C M
inst_5 : HasShift.{v_2, u_2, u_4} D M
inst_6 : HasShift.{v_3, u_3, u_4} E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a : M
ha : a = 0
d : M
h : ShiftedHom Z T d
rw : d + 0 = d
⊢ d + a = d
have rw₁ : d = d
Tactic: rw [ha, add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a : M
ha : a = 0
d : M
h : ShiftedHom Z T d
⊢ comp (b := d) (mk₀ a ha f) (comp (mk₀ a ha g) h ⋯) ⋯ = comp (mk₀ a ha (f ≫ g)) h ⋯
have subst : comp (b := d) (mk₀ 0 sorry f) (comp (mk₀ 0 sorry g) h sorry) sorry = comp (mk₀ 0 sorry (f ≫ g)) h sorry
Tactic: subst ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ comp (b := d) (mk₀ 0 ⋯ f) (comp (mk₀ 0 ⋯ g) h ⋯) ⋯ = comp (mk₀ 0 ⋯ (f ≫ g)) h ⋯
have h₁₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [← comp_assoc, mk₀_comp_mk₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
h₁₂ : HAdd.hAdd (α := M) 0 0 = 0
⊢ comp (b := d) (mk₀ 0 ⋯ f) (comp (mk₀ 0 ⋯ g) h ⋯) ⋯ = comp (mk₀ 0 ⋯ (f ≫ g)) h ⋯
have h₁ : d + 0 + 0 = d
Tactic: rw [← comp_assoc, mk₀_comp_mk₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
have rw : α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α.comp β₁ h + α.comp β₂ h
Tactic: rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
rw :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α.comp β₁ h + α.comp β₂ h
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
have rw₁ : α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α.comp β₂ h
Tactic: rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
rw :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α.comp β₁ h + α.comp β₂ h
rw₁ :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α.comp β₂ h
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
have rw₂ : α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
rw :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α.comp β₁ h + α.comp β₂ h
rw₁ :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α.comp β₂ h
rw₂ :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
have rw₃ : α ≫
    HAdd.hAdd (α :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
        (Functor.map (shiftFunctor C a) β₁) (Functor.map (shiftFunctor C a) β₂) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
rw :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α.comp β₁ h + α.comp β₂ h
rw₁ :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α.comp β₂ h
rw₂ :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₃ :
  α ≫
      HAdd.hAdd (α :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
          (Functor.map (shiftFunctor C a) β₁) (Functor.map (shiftFunctor C a) β₂) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
have rw₄ : α ≫
    (Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) =
  α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
rw :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α.comp β₁ h + α.comp β₂ h
rw₁ :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α.comp β₂ h
rw₂ :
  α ≫ Functor.map (shiftFunctor C a) (β₁ + β₂) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₃ :
  α ≫
      HAdd.hAdd (α :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
          (Functor.map (shiftFunctor C a) β₁) (Functor.map (shiftFunctor C a) β₂) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₄ :
  α ≫
      (Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
        Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) =
    α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
have rw₅ : α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α ≫ Functor.map (shiftFunctor C a) β₁ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α ≫ Functor.map (shiftFunctor C a) β₂ ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
a b c : M
α₁ α₂ : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
have rw : (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α₁.comp β h + α₂.comp β h
Tactic: rw [comp, comp, comp, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
a b c : M
α₁ α₂ : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw :
  (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α₁.comp β h + α₂.comp β h
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
have rw₁ : (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α₁ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α₂.comp β h
Tactic: rw [comp, comp, comp, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
a b c : M
α₁ α₂ : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw :
  (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α₁.comp β h + α₂.comp β h
rw₁ :
  (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α₁ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α₂.comp β h
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
have rw₂ : (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α₁ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α₂ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, comp, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
a b c : M
α₁ α₂ : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw :
  (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α₁.comp β h + α₂.comp β h
rw₁ :
  (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α₁ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z + α₂.comp β h
rw₂ :
  (α₁ + α₂) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    α₁ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
      α₂ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
have rw₃ : α₁ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α₂ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  α₁ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z +
    α₂ ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, comp, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (-β) h = -α.comp β h
have rw : α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
Tactic: rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
⊢ α.comp (-β) h = -α.comp β h
have rw₁ : α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
rw₁ :
  α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (-β) h = -α.comp β h
have rw₂ : α ≫ (-Functor.map (shiftFunctor C a) β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
rw₁ :
  α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₂ :
  α ≫ (-Functor.map (shiftFunctor C a) β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (-β) h = -α.comp β h
have rw₃ : α ≫ (-Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) =
  -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C a)
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
rw₁ :
  α ≫ Functor.map (shiftFunctor C a) (-β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₂ :
  α ≫ (-Functor.map (shiftFunctor C a) β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₃ :
  α ≫ (-Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) =
    -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (-β) h = -α.comp β h
have rw₄ : -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (-α).comp β h = -α.comp β h
have rw : (-α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
Tactic: rw [comp, comp, Preadditive.neg_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : (-α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
⊢ (-α).comp β h = -α.comp β h
have rw₁ : (-α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, Preadditive.neg_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : (-α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = -α.comp β h
rw₁ :
  (-α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ (-α).comp β h = -α.comp β h
have rw₂ : -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  -α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, Preadditive.neg_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.PreservesZeroMorphisms.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
a : M
β : ShiftedHom X Y a
b c : M
h : b + a = c
⊢ Eq (α := ShiftedHom X Z c) (β.comp 0 h) 0
have rw : Eq (α := ShiftedHom X Z c)
  (β ≫ Functor.map (shiftFunctor C a) 0 ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) 0
Tactic: rw [comp, Functor.map_zero, Limits.zero_comp, Limits.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHom (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
M : Type u_4
inst_1 : AddMonoid M
inst_2 : HasShift.{v_1, u_1, u_4} C M
X Y Z : C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (a : M), Functor.PreservesZeroMorphisms.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
a : M
β : ShiftedHom X Y a
b c : M
h : b + a = c
rw :
  Eq (α := ShiftedHom X Z c)
    (β ≫ Functor.map (shiftFunctor C a) 0 ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) 0
⊢ Eq (α := ShiftedHom X Z c) (β.comp 0 h) 0
have rw₁ : Eq (α := ShiftedHom X Z c) (β ≫ 0 ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) 0
Tactic: rw [comp, Functor.map_zero, Limits.zero_comp, Limits.comp_zero]