awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (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
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : G.CommShift A
this : F.CommShift A := adj.leftAdjointCommShift A
a : A
X : C
⊢ Eq (α := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a ⋙ 𝟭 C) X ⟶ ((F ⋙ G) ⋙ shiftFunctor C a).obj X)
    (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a) ≫ Functor.whiskerRight adj.unit (shiftFunctor C a)) X)
    (NatTrans.app (Functor.whiskerLeft (shiftFunctor C a) adj.unit ≫ Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X)
have w : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
  (NatTrans.app (Iso.hom (Functor.commShiftIso (𝟭 C) a)) X ≫ Functor.map (shiftFunctor C a) (adj.unit.app X) :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
  (adj.unit.app (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso (F ⋙ G) a)) X :
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) (G.obj (F.obj X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Adjunction (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
E : Equivalence.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddGroup A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
inst_5 : E.inverse.CommShift A
this : E.functor.CommShift A := E.commShiftFunctor A
⊢ E.CommShift A
have this₁ : E.symm.CommShift A
Tactic: have := E.symm.commShift_of_functor A
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
m₁ m₂ m₃ : A
X : C
⊢ (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X
have rw : (F (m₁ + (m₂ + m₃))).obj X = (F (m₁ + (m₂ + m₃))).obj X
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
n : A
X : C
⊢ (F (0 + n)).obj X = (F n).obj (obj.{v, v, u, u} (𝟭 C) X)
have dsimp : (F (0 + n)).obj X = (F n).obj X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
n : A
X : C
⊢ (F (0 + n)).obj X = (F n).obj X
have rw : (F n).obj X = (F n).obj X
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), NatTrans.app (Iso.hom (add 0 n)) X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
⊢ (F (n + 0)).obj X = obj.{v, v, u, u} (𝟭 C) ((F n).obj X)
have dsimp : (F (n + 0)).obj X = (F n).obj X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
F : A → Functor.{v, v, u, u} C C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    NatTrans.app (Iso.hom (add (m₁ + m₂) m₃)) X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ NatTrans.app (Iso.hom (add m₁ (m₂ + m₃))) X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), NatTrans.app (Iso.hom (add 0 n)) X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
⊢ (F (n + 0)).obj X = (F n).obj X
have rw : (F n).obj X = (F n).obj X
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F (m₁ + (m₂ + m₃))).obj X = (h.F (m₁ + m₂ + m₃)).obj X
have rw : (h.F (m₁ + (m₂ + m₃))).obj X = (h.F (m₁ + (m₂ + m₃))).obj X
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ NatTrans.app (Iso.inv (h.add (m₁ + m₂) m₃)) X =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ NatTrans.app (Iso.inv (h.add m₁ (m₂ + m₃))) X ≫ eqToHom ⋯
have rw : Eq.{v + 1} (α := (h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X) ⟶ (h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X))
  (𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X))) (𝟙 ((h.F m₂ ⋙ h.F m₃).obj ((h.F m₁).obj X)))
Tactic: rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)),
    Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
    Iso.inv_hom_id_app, Functor.map_id, h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl,
    Category.id_comp, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ (h.F n).obj (obj.{v, v, u, u} (𝟭 C) X) = (h.F (0 + n)).obj X
have dsimp : (h.F n).obj X = (h.F (0 + n)).obj X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ (h.F n).obj X = (h.F (0 + n)).obj X
have rw : (h.F n).obj X = (h.F n).obj X
Tactic: rw [zero_add]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw : NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₂ : 𝟙 ((h.F (0 + n)).obj X) = (eqToHom sorry ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom sorry ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₄ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom sorry ≫ (h.F n).map (h.zero.inv.app X ≫ h.zero.hom.app X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₄ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X ≫ h.zero.hom.app X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₅ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom sorry ≫ (h.F n).map (𝟙 (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₄ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X ≫ h.zero.hom.app X) ≫ eqToHom ⋯
rw₅ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (𝟙 (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₆ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X))
  (eqToHom sorry ≫ 𝟙 ((h.F n).obj (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom sorry)
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₄ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X ≫ h.zero.hom.app X) ≫ eqToHom ⋯
rw₅ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (𝟙 (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯
rw₆ :
  Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X))
    (eqToHom ⋯ ≫ 𝟙 ((h.F n).obj (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯)
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₇ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (eqToHom sorry ≫ eqToHom sorry)
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₄ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X ≫ h.zero.hom.app X) ≫ eqToHom ⋯
rw₅ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (𝟙 (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯
rw₆ :
  Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X))
    (eqToHom ⋯ ≫ 𝟙 ((h.F n).obj (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯)
rw₇ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (eqToHom ⋯ ≫ eqToHom ⋯)
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₈ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (eqToHom sorry)
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add 0 n)) X ≫ NatTrans.app (Iso.inv (h.add 0 n)) X =
    NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (0 + n)).obj X) = NatTrans.app (Iso.hom (h.add 0 n)) X ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (0 + n)).obj X) = (eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X)) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X) ≫ (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
rw₄ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (h.zero.inv.app X ≫ h.zero.hom.app X) ≫ eqToHom ⋯
rw₅ : 𝟙 ((h.F (0 + n)).obj X) = eqToHom ⋯ ≫ (h.F n).map (𝟙 (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯
rw₆ :
  Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X))
    (eqToHom ⋯ ≫ 𝟙 ((h.F n).obj (obj.{v, v, u, u} (𝟭 C) X)) ≫ eqToHom ⋯)
rw₇ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (eqToHom ⋯ ≫ eqToHom ⋯)
rw₈ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (eqToHom ⋯)
⊢ NatTrans.app (Iso.inv (h.add 0 n)) X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯
have rw₉ : Eq.{v + 1} (α := (h.F (0 + n)).obj X ⟶ (h.F (0 + n)).obj X) (𝟙 ((h.F (0 + n)).obj X)) (𝟙 ((h.F (0 + n)).obj X))
Tactic: rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
    Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    Category.id_comp, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ obj.{v, v, u, u} (𝟭 C) ((h.F n).obj X) = (h.F (n + 0)).obj X
have dsimp : (h.F n).obj X = (h.F (n + 0)).obj X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ (h.F n).obj X = (h.F (n + 0)).obj X
have rw : (h.F n).obj X = (h.F n).obj X
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
have rw : NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
    NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
have rw₁ : 𝟙 ((h.F (n + 0)).obj X) = NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
    NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (n + 0)).obj X) = NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
have rw₂ : 𝟙 ((h.F (n + 0)).obj X) = (eqToHom sorry ≫ h.zero.inv.app ((h.F n).obj X)) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
    NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (n + 0)).obj X) = NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (n + 0)).obj X) = (eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X)) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
have rw₃ : 𝟙 ((h.F (n + 0)).obj X) = eqToHom sorry ≫ h.zero.inv.app ((h.F n).obj X) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom sorry
Tactic: rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Basic (goal)
Goal:
C : Type u
A : Type u_1
inst : Category.{v, u} C
inst_1 : AddMonoid A
h : ShiftMkCore.{v, u, u_1} C A
n : A
X : C
rw :
  NatTrans.app (Iso.hom (h.add n 0)) X ≫ NatTrans.app (Iso.inv (h.add n 0)) X =
    NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₁ : 𝟙 ((h.F (n + 0)).obj X) = NatTrans.app (Iso.hom (h.add n 0)) X ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₂ :
  𝟙 ((h.F (n + 0)).obj X) = (eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X)) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
rw₃ : 𝟙 ((h.F (n + 0)).obj X) = eqToHom ⋯ ≫ h.zero.inv.app ((h.F n).obj X) ≫ h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
⊢ NatTrans.app (Iso.inv (h.add n 0)) X = h.zero.hom.app ((h.F n).obj X) ≫ eqToHom ⋯
have rw₄ : Eq.{v + 1} (α := (h.F (n + 0)).obj X ⟶ (h.F (n + 0)).obj X) (𝟙 ((h.F (n + 0)).obj X)) (eqToHom sorry ≫ eqToHom sorry)
Tactic: rw [← cancel_epi ((h.add n 0).hom.app X), Iso.hom_inv_id_app, h.add_zero_hom_app,
    Category.assoc, Iso.inv_hom_id_app_assoc, eqToHom_trans, eqToHom_refl]