awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) ((lift r F hF).obj ((functor r).obj X)))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      F.map (𝟙 (Functor.obj.{v, v, u, u} (𝟭 C) X)) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((lift r F hF).obj ((functor r).obj X)))
have w : Eq (α :=
  (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
    Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
    F.map (𝟙 X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
    NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
Tactic: dsimp [lift_obj_functor_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      F.map (𝟙 X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
have w : Eq (α :=
  (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
    Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
    𝟙 (F.obj X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
    NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
Tactic: rw [F.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
w :
  Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      𝟙 (F.obj X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
⊢ Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      F.map (𝟙 X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
have w₁ : Eq (α :=
  (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
    Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
    NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
  ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
    NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
Tactic: rw [F.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
⊢ Eq (α := shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ≅ lift r F hF ⋙ shiftFunctor D (a + b))
    (LiftCommShift.iso F r hF (a + b))
    (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))
have w : Eq (α := shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ lift r F hF ⋙ shiftFunctor D (a + b))
  (Iso.hom (LiftCommShift.iso F r hF (a + b)))
  (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
⊢ Eq (α := shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ lift r F hF ⋙ shiftFunctor D (a + b))
    (Iso.hom (LiftCommShift.iso F r hF (a + b)))
    (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)))
have w : Eq (α := functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b))
  ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b))))
  ((functor r).whiskerLeft
    (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
⊢ Eq (α :=
    functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF ⟶ functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b))
    ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b))))
    ((functor r).whiskerLeft
      (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))
have w : ∀ (X : C),
  Eq (α :=
    (functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF).obj X ⟶
      (functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b)))) X)
    (NatTrans.app
      ((functor r).whiskerLeft
        (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ Eq (α :=
    (functor r ⋙ shiftFunctor (Quotient r) (a + b) ⋙ lift r F hF).obj X ⟶
      (functor r ⋙ lift r F hF ⋙ shiftFunctor D (a + b)).obj X)
    (NatTrans.app ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF (a + b)))) X)
    (NatTrans.app
      ((functor r).whiskerLeft
        (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b))))
      X)
have w : Eq (α :=
  (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) (a + b)) ((functor r).obj X)) ⟶
    Functor.obj.{v', v', u', u'} (shiftFunctor D (a + b)) ((lift r F hF).obj ((functor r).obj X)))
  (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF (a + b))) ((functor r).obj X))
  (NatTrans.app (Iso.hom (Functor.CommShift.isoAdd (LiftCommShift.iso F r hF a) (LiftCommShift.iso F r hF b)))
    ((functor r).obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
⊢ Eq (α := shiftFunctor C a ⋙ functor r ⋙ lift r F hF ⟶ F ⋙ shiftFunctor D a)
    (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a) ≫
      Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a))
    (Functor.whiskerLeft (shiftFunctor C a) (lift.isLift r F hF).hom ≫ Iso.hom (Functor.commShiftIso F a))
have w : ∀ (X : C),
  Eq (α := (shiftFunctor C a ⋙ functor r ⋙ lift r F hF).obj X ⟶ (F ⋙ shiftFunctor D a).obj X)
    (NatTrans.app
      (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a) ≫
        Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a))
      X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) (lift.isLift r F hF).hom ≫ Iso.hom (Functor.commShiftIso F a))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ Eq (α := (shiftFunctor C a ⋙ functor r ⋙ lift r F hF).obj X ⟶ (F ⋙ shiftFunctor D a).obj X)
    (NatTrans.app
      (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a) ≫
        Functor.whiskerRight (lift.isLift r F hF).hom (shiftFunctor D a))
      X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) (lift.isLift r F hF).hom ≫ Iso.hom (Functor.commShiftIso F a))
      X)
have w : Eq (α :=
  (lift r F hF).obj ((functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ⟶
    Functor.obj.{v', v', u', u'} (shiftFunctor D a) (F.obj X))
  (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a)) X ≫
    Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
  (𝟙 (F.obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ Eq (α :=
    (lift r F hF).obj ((functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor D a) (F.obj X))
    (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r ⋙ lift r F hF) a)) X ≫
      Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
    (𝟙 (F.obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
have w : Eq (α :=
  (lift r F hF).obj ((functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ⟶
    Functor.obj.{v', v', u', u'} (shiftFunctor D a) (F.obj X))
  (((lift r F hF).map (𝟙 ((shiftFunctor C a ⋙ functor r).obj X)) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X) ≫
    Functor.map (shiftFunctor D a) (𝟙 (F.obj X)))
  (𝟙 (F.obj (Functor.obj.{v, v, u, u} (shiftFunctor C a) X)) ≫ NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X)
Tactic: rw [Functor.commShiftIso_comp_hom_app, liftCommShift_commShiftIso,
      LiftCommShift.iso_hom_app, ← Functor.map_comp_assoc, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
sequence : M → Functor.{v_1, v_2, u_1, u_2} C A
isoZero : sequence 0 ≅ F
shiftIso : (n a a' : M) → (ha' : n + a = a') → shiftFunctor C n ⋙ sequence a ≅ sequence a'
shiftIso_zero :
  ∀ (a : M), shiftIso 0 a a ⋯ = isoWhiskerRight (shiftFunctorZero C M) (sequence a) ≪≫ (sequence a).leftUnitor
n m a a' a'' : M
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.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
sequence : M → Functor.{v_1, v_2, u_1, u_2} C A
isoZero : sequence 0 ≅ F
shiftIso : (n a a' : M) → (ha' : n + a = a') → shiftFunctor C n ⋙ sequence a ≅ sequence a'
shiftIso_zero :
  ∀ (a : M), shiftIso 0 a a ⋯ = isoWhiskerRight (shiftFunctorZero C M) (sequence a) ≪≫ (sequence a).leftUnitor
n m a a' a'' : M
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.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
a : M
⊢ Iso.symm (associator (shiftFunctor.{v_1, u_1, u_3} C (A := M) 0) (shiftFunctor C a) F) ≪≫
      isoWhiskerRight (Iso.symm (shiftFunctorAdd' C 0 a a ⋯)) F =
    isoWhiskerRight (shiftFunctorZero C M) (shiftFunctor C a ⋙ F) ≪≫ (shiftFunctor C a ⋙ F).leftUnitor
have rw : Eq (α := shiftFunctor.{v_1, u_1, u_3} C (A := M) 0 ⋙ shiftFunctor C a ⋙ F ≅ shiftFunctor C a ⋙ F)
  (Iso.symm (associator (shiftFunctor.{v_1, u_1, u_3} C (A := M) 0) (shiftFunctor C a) F) ≪≫
    isoWhiskerRight
      (Iso.symm
        (Iso.symm (leftUnitor (shiftFunctor C a)) ≪≫
          isoWhiskerRight (Iso.symm (shiftFunctorZero C M)) (shiftFunctor C a)))
      F)
  (isoWhiskerRight (shiftFunctorZero C M) (shiftFunctor C a ⋙ F) ≪≫ (shiftFunctor C a ⋙ F).leftUnitor)
Tactic: rw [shiftFunctorAdd'_zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ Iso.symm (associator (shiftFunctor C (m + n)) (shiftFunctor C a) F) ≪≫
      isoWhiskerRight (Iso.symm (shiftFunctorAdd' C (m + n) a a'' ⋯)) F =
    isoWhiskerRight (shiftFunctorAdd C m n) (shiftFunctor C a ⋙ F) ≪≫
      associator (shiftFunctor C m) (shiftFunctor C n) (shiftFunctor C a ⋙ F) ≪≫
        isoWhiskerLeft (shiftFunctor C m)
            (Iso.symm (associator (shiftFunctor C n) (shiftFunctor C a) F) ≪≫
              isoWhiskerRight (Iso.symm (shiftFunctorAdd' C n a a' ha')) F) ≪≫
          Iso.symm (associator (shiftFunctor C m) (shiftFunctor C a') F) ≪≫
            isoWhiskerRight (Iso.symm (shiftFunctorAdd' C m a' a'' ha'')) F
have w : ∀ (X : C),
  NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor C (m + n)) (shiftFunctor C a) F) ≪≫
          isoWhiskerRight (Iso.symm (shiftFunctorAdd' C (m + n) a a'' sorry)) F))
      X =
    (isoWhiskerRight (shiftFunctorAdd C m n) (shiftFunctor C a ⋙ F) ≪≫
            associator (shiftFunctor C m) (shiftFunctor C n) (shiftFunctor C a ⋙ F) ≪≫
              isoWhiskerLeft (shiftFunctor C m)
                  (Iso.symm (associator (shiftFunctor C n) (shiftFunctor C a) F) ≪≫
                    isoWhiskerRight (Iso.symm (shiftFunctorAdd' C n a a' ha')) F) ≪≫
                Iso.symm (associator (shiftFunctor C m) (shiftFunctor C a') F) ≪≫
                  isoWhiskerRight (Iso.symm (shiftFunctorAdd' C m a' a'' ha'')) F).hom.app
      X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ NatTrans.app
      (Iso.hom
        (Iso.symm (associator (shiftFunctor C (m + n)) (shiftFunctor C a) F) ≪≫
          isoWhiskerRight (Iso.symm (shiftFunctorAdd' C (m + n) a a'' ⋯)) F))
      X =
    (isoWhiskerRight (shiftFunctorAdd C m n) (shiftFunctor C a ⋙ F) ≪≫
            associator (shiftFunctor C m) (shiftFunctor C n) (shiftFunctor C a ⋙ F) ≪≫
              isoWhiskerLeft (shiftFunctor C m)
                  (Iso.symm (associator (shiftFunctor C n) (shiftFunctor C a) F) ≪≫
                    isoWhiskerRight (Iso.symm (shiftFunctorAdd' C n a a' ha')) F) ≪≫
                Iso.symm (associator (shiftFunctor C m) (shiftFunctor C a') F) ≪≫
                  isoWhiskerRight (Iso.symm (shiftFunctorAdd' C m a' a'' ha'')) F).hom.app
      X
have w : 𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X))) ≫
    F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' sorry)) X) =
  F.map (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X)) ≫
    𝟙
        (F.obj
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
      (𝟙
            (F.obj
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
          F.map
            (NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
        𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
          F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ 𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X))) ≫
      F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X) =
    F.map (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X)) ≫
      𝟙
          (F.obj
            (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
              (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
        (𝟙
              (F.obj
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a)
                  (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X)))) ≫
            F.map
              (NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha'))
                (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
          𝟙 (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a') (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X))) ≫
            F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X)
have w : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X)) ⟶
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') X))
  (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' sorry)) X))
  (F.map
    (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X))
Tactic: simp only [id_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.ShiftSequence (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
F : Functor.{v_1, v_2, u_1, u_2} C A
M : Type u_3
inst_2 : AddMonoid M
inst_3 : HasShift.{v_1, u_1, u_3} C M
G : Type u_4
inst_4 : AddGroup G
inst_5 : HasShift.{v_1, u_1, u_4} C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X)) ⟶
      F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') X))
    (F.map (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' ⋯)) X))
    (F.map
      (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X))
have w : Eq.{v_1 + 1} (α :=
  obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m + n)) X) ⟶
    obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a'') X)
  (NatTrans.app (Iso.inv (shiftFunctorAdd' C (m + n) a a'' sorry)) X)
  (map (shiftFunctor C a) (NatTrans.app (Iso.hom (shiftFunctorAdd C m n)) X) ≫
    NatTrans.app (Iso.inv (shiftFunctorAdd' C n a a' ha')) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m) X) ≫
      NatTrans.app (Iso.inv (shiftFunctorAdd' C m a' a'' ha'')) X)
Tactic: congr