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
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
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
⊢ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHomOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ Eq (α := ShiftedHom Y Z c)
    (comp ((Equiv.symm (opEquiv a) : (a_1 : ShiftedHom (Opposite.op X) (Opposite.op Y) a) → ShiftedHom Y X a) f) z h)
    ((Equiv.symm (opEquiv a) :
          (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C b).obj Z)) (Opposite.op Y) a) →
            ShiftedHom Y ((shiftFunctor C b).obj Z) a)
        (Quiver.Hom.op z ≫ f) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
have rw : Eq (α := ShiftedHom Y Z c)
  (CategoryStruct.comp (Y :=
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C a) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C a))
          (Opposite.op Y)))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)))
      (Functor.map (shiftFunctor C a) (Quiver.Hom.unop f)) ≫
    Functor.map (shiftFunctor C a) z ≫ NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
  (CategoryStruct.comp (Y :=
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C a) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C a))
          (Opposite.op Y)))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C a))) (Opposite.op Y)))
      (Functor.map (shiftFunctor C a) (Quiver.Hom.unop (Quiver.Hom.op z ≫ f))) ≫
    NatTrans.app (Iso.inv (shiftFunctorAdd' C b a c h)) Z)
Tactic: rw [ShiftedHom.opEquiv_symm_apply, ShiftedHom.opEquiv_symm_apply,
    ShiftedHom.comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHomOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ (Equiv.symm (opEquiv' n m q hq) :
        (a : Opposite.op ((shiftFunctor C m).obj Z) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Z q)
      (Quiver.Hom.op g ≫
          CategoryStruct.comp (Y :=
            Functor.obj.{v_1, v_1, u_1, u_1}
              (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙
                Equivalence.functor (opShiftFunctorEquivalence C n))
              (Opposite.op Y))
            (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y))
            (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op f)) :
        Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) Z) ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (Opposite.op X)) =
    f.comp g ⋯
have rw : CategoryStruct.comp (Y :=
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C n))
          (Opposite.op X)))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)))
      (Functor.map (shiftFunctor C n)
        (Quiver.Hom.unop
          (Quiver.Hom.op g ≫
            CategoryStruct.comp (Y :=
              Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙
                  Equivalence.functor (opShiftFunctorEquivalence C n))
                (Opposite.op Y))
              (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y))
              (Functor.map (shiftFunctor Cᵒᵖ n) (Quiver.Hom.op f))))) ≫
    NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q sorry)) Z =
  f.comp g sorry
Tactic: rw [opEquiv'_symm_apply, opEquiv_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHomOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y Z : C
n m : ℤ
f : ShiftedHom X Y n
g : ShiftedHom Y Z m
q : ℤ
hq : n + m = q
⊢ Eq (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C q) Z) ⟶ Opposite.op X)
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫
        CategoryStruct.comp (Y :=
          Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                  (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))))
          (Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop
                  (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op Y)))) :
            Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y) ⟶
              Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n)
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n)
                      (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y))))))
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C n)))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y)) ≫
              Quiver.Hom.op f :
            Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C n) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C n))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) Y)) ⟶
              Opposite.op X))
    (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q ⋯)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫ Quiver.Hom.op f)
have a : Eq.{v_1 + 1} (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C q) Z) ⟶ Opposite.op X)
  (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q sorry)) Z) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫ Quiver.Hom.op f :
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C q) Z) ⟶ Opposite.op X)
  (Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C m n q sorry)) Z) ≫
    Quiver.Hom.op (Functor.map (shiftFunctor C n) g) ≫ Quiver.Hom.op f)
Tactic: erw [(opShiftFunctorEquivalence C n).inverse_counitInv_comp_assoc (Opposite.op Y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHomOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
n a : ℤ
x y :
  Opposite.op (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ᵒᵖ n) (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (Equiv.symm (opEquiv' n a a' h) :
        (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Y a')
      (x + y) =
    HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
      ((Equiv.symm (opEquiv' n a a' h) :
            (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Y a')
          x :
        ShiftedHom X Y a')
      ((Equiv.symm (opEquiv' n a a' h) :
            (a : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) → ShiftedHom X Y a')
          y :
        ShiftedHom X Y a')
have dsimp : (Equiv.symm (opEquiv n) :
        (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
          X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
      (x + y) ≫
    NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y =
  HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
    ((Equiv.symm (opEquiv n) :
            (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
              X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
          x ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
    ((Equiv.symm (opEquiv n) :
            (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
              X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
          y ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
Tactic: dsimp [opEquiv']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftedHomOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X Y : C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
n a : ℤ
x y :
  Opposite.op (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ᵒᵖ n) (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ (Equiv.symm (opEquiv n) :
          (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
            X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
        (x + y) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y =
    HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            x ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
      ((Equiv.symm (opEquiv n) :
              (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
                X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
            y ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' ⋯)) Y :
        X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
have rw : HAdd.hAdd (α := ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n) (β :=
      ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n)
      ((Equiv.symm (opEquiv n) :
            (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n) →
              ShiftedHom X ((shiftFunctor C a).obj Y) n)
          x :
        ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n)
      ((Equiv.symm (opEquiv n) :
            (a_1 : ShiftedHom (Opposite.op ((shiftFunctor C a).obj Y)) (Opposite.op X) n) →
              ShiftedHom X ((shiftFunctor C a).obj Y) n)
          y :
        ShiftedHom X (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) Y) n) ≫
    NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y =
  HAdd.hAdd (α := ShiftedHom X Y a') (β := ShiftedHom X Y a')
    ((Equiv.symm (opEquiv n) :
            (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
              X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
          x ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
    ((Equiv.symm (opEquiv n) :
            (a_1 : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) →
              X ⟶ (shiftFunctor C n).obj ((shiftFunctor C a).obj Y))
          y ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C a n a' sorry)) Y :
      X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') Y)
Tactic: rw [opEquiv_symm_add, Preadditive.add_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
functor : (a : A) → Functor.{v_1, v_2, u_1, u_2} C D
shiftIso : (n a a' : A) → (ha' : n + a = a') → functor a' ⋙ shiftFunctor D n ≅ functor a
shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (shiftFunctorZero D A)
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ m + n + a = a''
have rw : m + (n + a) = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
functor : (a : A) → Functor.{v_1, v_2, u_1, u_2} C D
shiftIso : (n a a' : A) → (ha' : n + a = a') → functor a' ⋙ shiftFunctor D n ≅ functor a
shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (shiftFunctorZero D A)
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + (n + a) = a''
rw₁ : m + a' = a''
⊢ m + n + a = a''
have rw₂ : a'' = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = a''
have rw : m + (n + a) = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + (n + a) = a''
rw₁ : m + a' = a''
⊢ m + n + a = a''
have rw₂ : a'' = a''
Tactic: rw [add_assoc, ha', ha'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''
have rw : m + n + a = a''
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + n + a = a''
⊢ mn + a = a''
have rw₁ : m + n + a = m + a'
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
⊢ mn + a = a''
have rw₂ : m + n + a = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
rw₂ : m + n + a = m + (n + a)
⊢ mn + a = a''
have rw₃ : m + (n + a) = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso mn a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (shiftFunctorAdd' D m n mn hnm) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
have subst : F.shiftIso (m + n) a a'' sorry =
  (F.functor a'').isoWhiskerLeft (shiftFunctorAdd' D m n (m + n) sorry) ≪≫
    ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
      isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
Tactic: subst hnm
Cleared hypotheses: mn, hnm
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso (m + n) a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (shiftFunctorAdd' D m n (m + n) ⋯) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
have rw : F.shiftIso (m + n) a a'' sorry =
  (F.functor a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
    ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
      isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_5
inst_2 : AddMonoid A
inst_3 : HasShift.{v_2, u_2, u_5} D A
F : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
rw :
  F.shiftIso (m + n) a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
⊢ F.shiftIso (m + n) a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (shiftFunctorAdd' D m n (m + n) ⋯) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
have rw₁ : (F.functor a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
    ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
      isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha' =
  (F.functor a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
    ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
      isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'
Tactic: rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ mn + a = a''
have rw : m + n + a = a''
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = a''
⊢ mn + a = a''
have rw₁ : m + n + a = m + a'
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.SingleFunctors (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Category.{v_4, u_4} E'
A : Type u_5
inst_4 : AddMonoid A
inst_5 : HasShift.{v_2, u_2, u_5} D A
inst_6 : HasShift.{v_3, u_3, u_5} E A
inst_7 : HasShift.{v_4, u_4, u_5} E' A
F G H : SingleFunctors.{v_1, u_1, v_2, u_2, u_5} C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
rw : m + n + a = a''
rw₁ : m + n + a = m + a'
⊢ mn + a = a''
have rw₂ : m + n + a = m + (n + a)
Tactic: rw [← hnm, ← ha'', ← ha', add_assoc]