awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
m₀ : M
hm₀ : m₀ = 0
g : ShiftedHom X Y m₀
⊢ (fun (f : X ⟶ Y) ↦ (mk₀ m₀ hm₀ f : ShiftedHom X Y m₀))
      ((fun (g : ShiftedHom X Y m₀) ↦ g ≫ NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) Y) g) =
    g

Tactic:
simp [mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
rw : a + 0 = a
rw₁ rw₂ : a = a
⊢ a + m₀ = a

Tactic:
rw [hm₀, add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
subst : comp (mk₀ 0 ⋯ f) g ⋯ = f ≫ g
⊢ comp (mk₀ m₀ hm₀ f) g ⋯ = f ≫ g

Tactic:
subst hm₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ comp (mk₀ 0 ⋯ f) g ⋯ = f ≫ g

Tactic:
simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero']

Premises used: CategoryTheory.shiftFunctorAdd'_add_zero_inv_app, CategoryTheory.ShiftedHom.comp, CategoryTheory.ShiftedHom.mk₀, CategoryTheory.shiftFunctorZero'
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
rw : a + 0 = a
rw₁ rw₂ : a = a
⊢ a + m₀ = a

Tactic:
rw [hm₀, add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 : C
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
⊢ comp (mk₀ m₀ hm₀ (𝟙 X)) f ⋯ = f

Tactic:
simp [mk₀_comp]

Premises used: CategoryTheory.ShiftedHom.mk₀_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
rw : 0 + a = a
rw₁ rw₂ : a = a
⊢ m₀ + a = a

Tactic:
rw [hm₀, zero_add]

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
subst : f.comp (mk₀ 0 ⋯ g) ⋯ = f ≫ Functor.map (shiftFunctor C a) g
⊢ f.comp (mk₀ m₀ hm₀ g) ⋯ = f ≫ Functor.map (shiftFunctor C a) g

Tactic:
subst hm₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
a : M
f : ShiftedHom X Y a
g : Y ⟶ Z
⊢ f.comp (mk₀ 0 ⋯ g) ⋯ = f ≫ Functor.map (shiftFunctor C a) g

Tactic:
simp only [comp, shiftFunctorAdd'_zero_add_inv_app, mk₀, shiftFunctorZero',
    eqToIso_refl, Iso.refl_trans, ← Functor.map_comp, assoc, Iso.inv_hom_id_app,
    Functor.id_obj, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctorAdd'_zero_add_inv_app, CategoryTheory.Category.comp_id, CategoryTheory.ShiftedHom.comp, CategoryTheory.Iso.refl_trans, CategoryTheory.ShiftedHom.mk₀, CategoryTheory.eqToIso_refl, CategoryTheory.shiftFunctorZero', CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
rw : 0 + a = a
rw₁ rw₂ : a = a
⊢ m₀ + a = a

Tactic:
rw [hm₀, zero_add]

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
⊢ f.comp (mk₀ m₀ hm₀ (𝟙 Y)) ⋯ = f

Tactic:
simp [comp_mk₀]

Premises used: CategoryTheory.ShiftedHom.comp_mk₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 b c : M
h : b + a = c
ha : a = 0
hb : b = 0
rw : b + a = 0
rw₁ : b + 0 = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
rw₃ rw₄ : Eq.{u_4 + 1} (α := M) 0 0
⊢ c = 0

Tactic:
rw [← h, ha, hb, add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
subst :
  ∀ (h : HAdd.hAdd (α := M) 0 0 = c), Eq (α := ShiftedHom X Z c) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ c ⋯ (f ≫ g))
⊢ Eq (α := ShiftedHom X Z c) (comp (mk₀ a ha f) (mk₀ b hb g) h) (mk₀ c ⋯ (f ≫ g))

Tactic:
subst ha hb
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : HAdd.hAdd (α := M) 0 0 = c
rw : HAdd.hAdd (α := M) 0 0 = 0
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ c = 0

Tactic:
rw [← h, zero_add]

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : HAdd.hAdd (α := M) 0 0 = c
obtain :
  ∀ (h : HAdd.hAdd (α := M) 0 0 = 0),
    Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ 0 ⋯ (f ≫ g))
⊢ Eq (α := ShiftedHom X Z c) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ c ⋯ (f ≫ g))

Tactic:
obtain rfl : c = 0 := by rw [← h, zero_add]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
f : X ⟶ Y
g : Y ⟶ Z
h : HAdd.hAdd (α := M) 0 0 = 0
rw : Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ mk₀ 0 ⋯ g) (mk₀ 0 ⋯ (f ≫ g))
rw₁ :
  Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
    (mk₀ 0 ⋯ (f ≫ g))
rw₂ :
  Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
    ((f ≫ g) ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
rw₃ rw₄ :
  Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
    (f ≫ g ≫ NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Z)
⊢ Eq (α := ShiftedHom.{v_1, u_1, u_4} (M := M) X Z 0) (comp (mk₀ 0 ⋯ f) (mk₀ 0 ⋯ g) h) (mk₀ 0 ⋯ (f ≫ g))

Tactic:
rw [mk₀_comp, mk₀, mk₀, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShiftedHom.mk₀_comp, CategoryTheory.ShiftedHom.mk₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
rw₁ rw₂ : d = d
⊢ d + a = d

Tactic:
rw [ha, add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
subst : comp (b := d) (mk₀ 0 ⋯ f) (comp (mk₀ 0 ⋯ g) h ⋯) ⋯ = comp (mk₀ 0 ⋯ (f ≫ g)) h ⋯
⊢ comp (b := d) (mk₀ a ha f) (comp (mk₀ a ha g) h ⋯) ⋯ = comp (mk₀ a ha (f ≫ g)) h ⋯

Tactic:
subst ha
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
h₁ : d + 0 + 0 = d
⊢ comp (b := d) (mk₀ 0 ⋯ f) (comp (mk₀ 0 ⋯ g) h ⋯) ⋯ = comp (mk₀ 0 ⋯ (f ≫ g)) h ⋯

Tactic:
rw [← comp_assoc, mk₀_comp_mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀_comp_mk₀, CategoryTheory.ShiftedHom.comp_assoc
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
⊢ HAdd.hAdd (α := M) 0 0 = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
⊢ d + 0 + 0 = d

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 : C
inst_3 : Preadditive.{v_1, u_1} C
m₀ : M
hm₀ : m₀ = 0
⊢ Eq.{v_1 + 1} (α := ShiftedHom X Y m₀) (mk₀ m₀ hm₀ 0) 0

Tactic:
simp [mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 : C
inst_3 : Preadditive.{v_1, u_1} C
m₀ : M
hm₀ : m₀ = 0
f g : X ⟶ Y
⊢ mk₀ m₀ hm₀ (f + g) = HAdd.hAdd (α := ShiftedHom X Y m₀) (mk₀ m₀ hm₀ f) (mk₀ m₀ hm₀ g)

Tactic:
simp [mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 : C
inst_3 : Preadditive.{v_1, u_1} C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
⊢ Eq (α := ShiftedHom X Y m₀) (mk₀ m₀ hm₀ (-f)) (-mk₀ m₀ hm₀ f)

Tactic:
simp [mk₀]

Premises used: CategoryTheory.ShiftedHom.mk₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
rw₅ 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

Tactic:
rw [comp, comp, comp, Functor.map_add, Preadditive.add_comp, Preadditive.comp_add]

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.ShiftedHom.comp, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
rw₃ 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

Tactic:
rw [comp, comp, comp, Preadditive.add_comp]

Premises used: CategoryTheory.ShiftedHom.comp, CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
rw₄ 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

Tactic:
rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]

Premises used: CategoryTheory.Preadditive.comp_neg, CategoryTheory.ShiftedHom.comp, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_neg
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
rw₂ 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

Tactic:
rw [comp, comp, Preadditive.neg_comp]

Premises used: CategoryTheory.ShiftedHom.comp, CategoryTheory.Preadditive.neg_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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
rw₁ : Eq (α := ShiftedHom X Z c) (β ≫ 0 ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) 0
rw₂ : Eq (α := ShiftedHom X Z c) (β ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := ShiftedHom X Z c) 0 0
⊢ Eq (α := ShiftedHom X Z c) (β.comp 0 h) 0

Tactic:
rw [comp, Functor.map_zero, Limits.zero_comp, Limits.comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.ShiftedHom.comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 Y Z b
h : b + a = c
rw :
  Eq (α := ShiftedHom X Z c)
    (0 ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := ShiftedHom X Z c) 0 0
⊢ Eq (α := ShiftedHom X Z c) (comp 0 β h) 0

Tactic:
rw [comp, Limits.zero_comp]

Premises used: CategoryTheory.ShiftedHom.comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift M
subst : Eq (α := ShiftedHom.{v_2, u_2, u_4} (M := M) (F.obj X) (F.obj Y) 0) (map (mk₀ 0 ⋯ f) F) (mk₀ 0 ⋯ (F.map f))
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Y) m₀) (map (mk₀ m₀ hm₀ f) F) (mk₀ m₀ hm₀ (F.map f))

Tactic:
subst hm₀
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
M : Type u_4
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_4} C M
inst_4 : HasShift.{v_2, u_2, u_4} D M
X Y : C
f : X ⟶ Y
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift M
⊢ Eq (α := ShiftedHom.{v_2, u_2, u_4} (M := M) (F.obj X) (F.obj Y) 0) (map (mk₀ 0 ⋯ f) F) (mk₀ 0 ⋯ (F.map f))

Tactic:
simp [map, mk₀, shiftFunctorZero', F.commShiftIso_zero M, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.ShiftedHom.map, CategoryTheory.ShiftedHom.mk₀, CategoryTheory.shiftFunctorZero', CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 : C
a : M
f : ShiftedHom X Y a
⊢ f.map (𝟭 C) = f

Tactic:
simp [map]

Premises used: CategoryTheory.ShiftedHom.map
-- Module: Mathlib.CategoryTheory.Shift.ShiftedHom
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 : C
a : M
f : ShiftedHom X Y a
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_7 : F.CommShift M
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : G.CommShift M
⊢ Eq (α := ShiftedHom ((F ⋙ G).obj X) ((F ⋙ G).obj Y) a) (f.map (F ⋙ G)) (map (f.map F) G)

Tactic:
simp [map, Functor.commShiftIso_comp_hom_app]

Premises used: CategoryTheory.Functor.commShiftIso_comp_hom_app, CategoryTheory.ShiftedHom.map