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
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
⊢ Eq (α := ShiftedHom X Z c) (β.comp 0 h) 0
have rw₂ : Eq (α := ShiftedHom X Z c) (β ≫ 0) 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
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
⊢ Eq (α := ShiftedHom X Z c) (β.comp 0 h) 0
have rw₃ : Eq.{v_1 + 1} (α := ShiftedHom X Z c) 0 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
a b c : M
β : ShiftedHom Y Z b
h : b + a = c
⊢ Eq (α := ShiftedHom X Z c) (comp 0 β h) 0
have rw : Eq (α := ShiftedHom X Z c)
  (0 ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) 0
Tactic: rw [comp, Limits.zero_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 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
⊢ Eq (α := ShiftedHom X Z c) (comp 0 β h) 0
have rw₁ : Eq.{v_1 + 1} (α := ShiftedHom X Z c) 0 0
Tactic: rw [comp, Limits.zero_comp]
-- 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
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
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Y) m₀) (map (mk₀ m₀ hm₀ f) F) (mk₀ m₀ hm₀ (F.map f))
have subst : Eq (α := ShiftedHom.{v_2, u_2, u_4} (M := M) (F.obj X) (F.obj Y) 0) (map (mk₀ 0 sorry f) F) (mk₀ 0 sorry (F.map f))
Tactic: subst hm₀
Cleared hypotheses: m₀, hm₀
-- 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
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
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
have rw : Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
  (comp (mk₀ 0 sorry (τ.app X)) (f.map G) sorry)
Tactic: rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]
-- 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
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
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
rw :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
have rw₁ : Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y)) (τ.app X ≫ f.map G)
Tactic: rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]
-- 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
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
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
rw :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
rw₁ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y)) (τ.app X ≫ f.map G)
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
have rw₂ : Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
  ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
  (τ.app X ≫ f.map G)
Tactic: rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]
-- 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
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
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
rw :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
rw₁ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y)) (τ.app X ≫ f.map G)
rw₂ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ f.map G)
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
have rw₃ : Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
  ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
  (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
Tactic: rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]
-- 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
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
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
rw :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
rw₁ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y)) (τ.app X ≫ f.map G)
rw₂ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ f.map G)
rw₃ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
have rw₄ : Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
  (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y ≫ Functor.map (shiftFunctor D a) (τ.app Y))
  (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
Tactic: rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]
-- 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
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
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
rw :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
rw₁ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y)) (τ.app X ≫ f.map G)
rw₂ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ f.map G)
rw₃ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
rw₄ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
have rw₅ : Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
  (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y ≫ Functor.map (shiftFunctor D a) (τ.app Y))
  (F.map f ≫
    τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
Tactic: rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]
-- 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
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
a : M
f : ShiftedHom X Y a
F G : Functor.{v_1, v_2, u_1, u_2} C D
τ : F ⟶ G
inst_5 : F.CommShift M
inst_6 : G.CommShift M
inst_7 : NatTrans.CommShift τ M
rw :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
rw₁ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (f.map F ≫ Functor.map (shiftFunctor D a) (τ.app Y)) (τ.app X ≫ f.map G)
rw₂ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ f.map G)
rw₃ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    ((F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y) ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
rw₄ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (τ.app X ≫ G.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
rw₅ :
  Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
    (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y ≫ Functor.map (shiftFunctor D a) (τ.app Y))
    (F.map f ≫
      τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
⊢ Eq (α := ShiftedHom (F.obj X) (G.obj Y) a) (comp (f.map F) (mk₀ 0 ⋯ (τ.app Y)) ⋯)
    (comp (mk₀ 0 ⋯ (τ.app X)) (f.map G) ⋯)
have rw₆ : Eq (α := ShiftedHom (F.obj X) (G.obj Y) a)
  (F.map f ≫
    τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
  (F.map f ≫
    τ.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G a)) Y)
Tactic: rw [comp_mk₀, mk₀_comp, map, map, Category.assoc, ← τ.naturality_assoc,
    τ.shift_app_comm a]
-- 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
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 Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift M
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Z) c) ((f.comp g h).map F) (comp (f.map F) (g.map F) h)
have dsimp : Eq (α := ShiftedHom (F.obj X) (F.obj Z) c)
  (F.map (f ≫ Functor.map (shiftFunctor C a) g ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso F c)) Z)
  (CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj Y))
    (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y)
    (Functor.map (shiftFunctor D a) (F.map g ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F b)) Z) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (F.obj Z)))
Tactic: dsimp [comp, map]
-- 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
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 Z : C
a b c : M
f : ShiftedHom X Y a
g : ShiftedHom Y Z b
h : b + a = c
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.CommShift M
⊢ Eq (α := ShiftedHom (F.obj X) (F.obj Z) c)
    (F.map (f ≫ Functor.map (shiftFunctor C a) g ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F c)) Z)
    (CategoryStruct.comp (Y := Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a) (F.obj Y))
      (F.map f ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) Y)
      (Functor.map (shiftFunctor D a) (F.map g ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F b)) Z) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (F.obj Z)))
have simp : Eq (α := ShiftedHom (F.obj X) (F.obj Z) c)
  (F.map f ≫
    F.map (Functor.map (shiftFunctor C a) g) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso F c)) Z)
  (F.map f ≫
    F.map (Functor.map (shiftFunctor C a) g) ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D a)
          (F.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b) Z))
        (Functor.map (shiftFunctor D a) (NatTrans.app (Iso.hom (Functor.commShiftIso F b)) Z) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (F.obj Z)))
Tactic: simp only [Functor.map_comp, assoc, ← Functor.commShiftIso_hom_naturality_assoc]
-- 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
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
inst_6 : ∀ (a : M), Functor.Linear.{u_5, v_1, u_1, v_1, u_1} R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (r • β) h = r • α.comp β h
have rw : α ≫ Functor.map (shiftFunctor C a) (r • β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
Tactic: rw [comp, Functor.map_smul, comp, Linear.smul_comp, Linear.comp_smul]
-- 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
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
inst_6 : ∀ (a : M), Functor.Linear.{u_5, v_1, u_1, v_1, u_1} R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (r • β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
⊢ α.comp (r • β) h = r • α.comp β h
have rw₁ : α ≫
    HSMul.hSMul (β :=
        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))
        r (Functor.map (shiftFunctor C a) β) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  r • α.comp β h
Tactic: rw [comp, Functor.map_smul, comp, Linear.smul_comp, Linear.comp_smul]
-- 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
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
inst_6 : ∀ (a : M), Functor.Linear.{u_5, v_1, u_1, v_1, u_1} R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (r • β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
rw₁ :
  α ≫
      HSMul.hSMul (β :=
          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))
          r (Functor.map (shiftFunctor C a) β) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α.comp β h
⊢ α.comp (r • β) h = r • α.comp β h
have rw₂ : α ≫
    HSMul.hSMul (β :=
        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))
        r (Functor.map (shiftFunctor C a) β) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, Functor.map_smul, comp, Linear.smul_comp, Linear.comp_smul]
-- 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
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
inst_6 : ∀ (a : M), Functor.Linear.{u_5, v_1, u_1, v_1, u_1} R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (r • β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
rw₁ :
  α ≫
      HSMul.hSMul (β :=
          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))
          r (Functor.map (shiftFunctor C a) β) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α.comp β h
rw₂ :
  α ≫
      HSMul.hSMul (β :=
          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))
          r (Functor.map (shiftFunctor C a) β) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (r • β) h = r • α.comp β h
have rw₃ : α ≫ (r • Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) =
  r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, Functor.map_smul, comp, Linear.smul_comp, Linear.comp_smul]
-- 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
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
inst_6 : ∀ (a : M), Functor.Linear.{u_5, v_1, u_1, v_1, u_1} R (shiftFunctor C a)
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : α ≫ Functor.map (shiftFunctor C a) (r • β) ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
rw₁ :
  α ≫
      HSMul.hSMul (β :=
          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))
          r (Functor.map (shiftFunctor C a) β) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α.comp β h
rw₂ :
  α ≫
      HSMul.hSMul (β :=
          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))
          r (Functor.map (shiftFunctor C a) β) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
rw₃ :
  α ≫ (r • Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z) =
    r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
⊢ α.comp (r • β) h = r • α.comp β h
have rw₄ : r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, Functor.map_smul, comp, Linear.smul_comp, Linear.comp_smul]
-- 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
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (r • α).comp β h = r • α.comp β h
have rw : (r • α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
Tactic: rw [comp, comp, Linear.smul_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
R : Type u_5
inst_3 : Ring R
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Linear.{u_5, v_1, u_1} R C
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
rw : (r • α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z = r • α.comp β h
⊢ (r • α).comp β h = r • α.comp β h
have rw₁ : (r • α) ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z =
  r • α ≫ Functor.map (shiftFunctor C a) β ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z
Tactic: rw [comp, comp, Linear.smul_comp]