awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫ NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
have rw₂ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
  (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 sorry)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
    Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X
Tactic: rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
    id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫ NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₂ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
have rw₃ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 sorry)) X ≫
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X
Tactic: rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
    id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫ NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₂ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₃ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
have rw₄ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 sorry)) X ≫
    Quiver.Hom.op
        (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
          NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X
Tactic: rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
    id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫ NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₂ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
        Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₃ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
rw₄ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X) ≫
            NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
have rw₅ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 sorry)) X ≫
    Quiver.Hom.op (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 0) (Opposite.unop X))) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X
Tactic: rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
    id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₁ = (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1 : (a : ℤ) → ℤ) a₁
have dsimp : b₁ = -a₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₂ = (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1 : (a : ℤ) → ℤ) a₂
have dsimp : b₂ = -a₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₃ = (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1 : (a : ℤ) → ℤ) a₃
have dsimp : b₃ = -a₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ Eq.{v_1 + 1} (α :=
    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₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))
have erw : 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₁ ⋙ shiftFunctor Cᵒᵖ a₂) X)
  (NatTrans.app
      (Iso.hom
        (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
          (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₃ b₃ sorry))
      X ≫
    NatTrans.app (Iso.hom (shiftFunctorAdd' (OppositeShift.{v_1, u_1, 0} C ℤ) b₁ b₂ b₃ sorry)) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1}
          (shiftFunctor
            (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
              (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
            a₂)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
        (NatTrans.app
          (Iso.inv
            (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
              (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₂ b₂ sorry))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (OppositeShift.{v_1, u_1, 0} C ℤ) b₁) X))
        (Functor.map
          (shiftFunctor
            (PullbackShift.{v_1, u_1, 0, 0} (OppositeShift.{v_1, u_1, 0} C ℤ)
              (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1))
            a₂)
          (NatTrans.app
            (Iso.inv
              (pullbackShiftIso (OppositeShift.{v_1, u_1, 0} C ℤ)
                (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1) a₁ b₁ sorry))
            X)))
  (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
          (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
        Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.inv (shiftFunctorOpIso C a₁ b₁ h₁)) X))
Tactic: erw [@pullbackShiftFunctorAdd'_hom_app (OppositeShift C ℤ) _ _ _ _ _ _ _ X
    a₁ a₂ a₃ h b₁ b₂ b₃ (by dsimp; lia) (by dsimp; lia) (by dsimp; lia)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₁ ⋙ shiftFunctor Cᵒᵖ a₂) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h)) X)
    (Functor.map (shiftFunctor Cᵒᵖ a₂) (NatTrans.app (Iso.hom (shiftFunctorOpIso C a₁ b₁ h₁)) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorOpIso C a₂ b₂ h₂))
          (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X)
have rw : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
          (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
        Functor.map (shiftFunctor Cᵒᵖ a₂) (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X)) ≫
          NatTrans.app (Iso.hom (shiftFunctorOpIso C a₂ b₂ h₂))
              (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X) ≫
            Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
              NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
Tactic: rw [← cancel_epi ((shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorAdd'_op_hom_app X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃,
    assoc, assoc, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₂ b₂ h₂))
            (Opposite.op ((shiftFunctor C b₁ : Functor.{v_1, v_1, u_1, u_1} C C).1 (Opposite.unop X))) ≫
          Functor.map (shiftFunctor Cᵒᵖ a₂) (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X)) ≫
            NatTrans.app (Iso.hom (shiftFunctorOpIso C a₂ b₂ h₂))
                (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C b₁)) X) ≫
              Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
                NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
have erw : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
    Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
Tactic: erw [Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
have rw : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
    Quiver.Hom.op
        (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ sorry)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
Tactic: rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
have rw₁ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
    Quiver.Hom.op (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) (Opposite.unop X))) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
Tactic: rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) (Opposite.unop X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
have rw₂ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
    𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) (Opposite.unop X))) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
Tactic: rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op
          (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X) ≫
            NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
rw₁ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) (Opposite.unop X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
rw₂ :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      𝟙 (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) (Opposite.unop X))) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
    NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
        Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) (Opposite.unop X)) ≫
          NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
have rw₃ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ a₃) X) =
  NatTrans.app (Iso.hom (shiftFunctorOpIso C a₃ b₃ h₃)) X ≫ NatTrans.app (Iso.inv (shiftFunctorOpIso C a₃ b₃ h₃)) X
Tactic: rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]