awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangle (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ (Functor.obj (inverse C ⋙ functor C) T).mor₃ ≫
      Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₁)) =
    Iso.hom (Iso.refl (Functor.obj (inverse C ⋙ functor C) T).obj₃) ≫ (Functor.obj (𝟭 (Triangle.{v_1, u_1} Cᵒᵖ)) T).mor₃
have refine_3 : CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) T.obj₃ :
          Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) T.obj₃ ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
              T.obj₃)
        (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) T.mor₃.unop) ≫
              NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T.obj₁) :
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))) ⟶
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁) :
      T.obj₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
    (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (𝟙 T.obj₁) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁ ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁) =
  𝟙 T.obj₃ ≫ T.mor₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangle (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
T : Triangle.{v_1, u_1} Cᵒᵖ
⊢ CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
            (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))))
          (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C 1))) T.obj₃ :
            Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) T.obj₃ ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (Functor.op (shiftFunctor C (A := ℤ) 1) ⋙ shiftFunctor Cᵒᵖ (A := ℤ) 1)
                T.obj₃)
          (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
              (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) T.mor₃.unop) ≫
                NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T.obj₁) :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T.obj₃))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁) :
        T.obj₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁)
      (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) (𝟙 T.obj₁) :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁ ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T.obj₁) =
    𝟙 T.obj₃ ≫ T.mor₃
have refine_3 : T.mor₃ ≫
    𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) T.obj₁)) =
  T.mor₃
Tactic: rw [Functor.map_id, comp_id, id_comp, Functor.map_comp,
        ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc,
        opShiftFunctorEquivalence_counitIso_inv_app_shift, ← Functor.map_comp,
        Iso.hom_inv_id_app, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ Nonempty.{v_1 + 1} (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
have refine_1 : o.m₃.op ≫ w₁₃ = w₁₂
Tactic: refine ⟨o.m₃.op, o.m₁.op, congr($(o.comm₄).op), ?_, congr($(o.comm₁).op), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
refine_1 : o.m₃.op ≫ w₁₃ = w₁₂
⊢ Nonempty.{v_1 + 1} (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
have refine_2 : w₁₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂ = o.m₁.op ≫ w₂₃
Tactic: refine ⟨o.m₃.op, o.m₁.op, congr($(o.comm₄).op), ?_, congr($(o.comm₁).op), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
refine_1 : o.m₃.op ≫ w₁₃ = w₁₂
refine_2 : w₁₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂ = o.m₁.op ≫ w₂₃
⊢ Nonempty.{v_1 + 1} (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
have refine_3 : Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
  (@Pretriangulated.distinguishedTriangles _ _ sorry _ (instPreadditiveOpposite C) sorry _)
  (Triangle.mk o.m₃.op o.m₁.op (w₂₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) v₁₂))
Tactic: refine ⟨o.m₃.op, o.m₁.op, congr($(o.comm₄).op), ?_, congr($(o.comm₁).op), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ o.m₃.op ≫ w₁₃ = w₁₂
have eq₃ : Eq (α :=
  Opposite.op
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop (Triangle.mk u₁₂ v₁₂ w₁₂).obj₃)) ⟶
    Opposite.op (Opposite.unop (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁))
  (Quiver.Hom.op
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1))
            (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃.unop) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) o.m₃))
  (Quiver.Hom.op
    (CategoryStruct.comp (Y :=
      Opposite.unop
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1))
          (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁))
      (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃.unop)))
Tactic: have eq₃ := congr($(o.comm₃).op)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₃ :
  Eq.{v_1 + 1} (α :=
    Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₂)) ⟶ X₁)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) o.m₃) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₃.unop) ≫
        NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₁)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₂.unop) ≫
      NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₁)
⊢ o.m₃.op ≫ w₁₃ = w₁₂
have eq₄ : Eq (α :=
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₂)) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1}
      (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₁)
  (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₁₃.unop ≫ o.m₃)))
  (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₂.unop))
Tactic: rw [← Category.assoc, ← op_comp, ← Functor.map_comp,
        NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso] at eq₃
Cleared hypotheses: eq₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ w₁₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂ = o.m₁.op ≫ w₂₃
have eq₂ : Eq (α :=
  Opposite.op
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop (Triangle.mk u₁₃ v₁₃ w₁₃).obj₃)) ⟶
    Opposite.op (Opposite.unop (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
  (Quiver.Hom.op
    (CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1))
            (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃.unop) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) o.m₁))
  (Quiver.Hom.op
    ((Triangle.mk u₁₂ v₁₂ w₁₂).mor₁.unop ≫
      CategoryStruct.comp (Y :=
        Opposite.unop
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1))
            (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
        (Quiver.Hom.unop
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃.unop)))
Tactic: have eq₂ := congr($(o.comm₂).op)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  Eq (α := Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₃)) ⟶ X₂)
    (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) o.m₁) ≫
      Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₂₃.unop) ≫
        NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₂)
    ((Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) w₁₃.unop) ≫
        NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) X₁) ≫
      u₁₂)
⊢ w₁₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂ = o.m₁.op ≫ w₂₃
have eq₃ : Eq (α :=
  Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop Z₁₃)) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1}
      (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙ Equivalence.inverse (opShiftFunctorEquivalence C 1)) X₂)
  (Quiver.Hom.op (Functor.map (shiftFunctor C (A := ℤ) 1) (w₂₃.unop ≫ o.m₁)))
  (Quiver.Hom.op
    (Functor.map (shiftFunctor C (A := ℤ) 1)
      (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) u₁₂) ≫ w₁₃.unop)))
Tactic: rw [← Category.assoc, ← op_comp, ← Functor.map_comp, Category.assoc,
        ← opShiftFunctorEquivalence_unitIso_inv_naturality, ← Category.assoc,
        NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso, ← op_comp,
        ← Functor.map_comp] at eq₂
Cleared hypotheses: eq₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _) (Triangle.mk u₁₃ v₁₃ w₁₃)
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
    (@Pretriangulated.distinguishedTriangles _ _ ⋯ _ (instPreadditiveOpposite C) ⋯ _)
    (Triangle.mk o.m₃.op o.m₁.op (w₂₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) v₁₂))
have this : Membership.mem (γ := Set (Triangle.{v_1, u_1} Cᵒᵖ))
  (@Pretriangulated.distinguishedTriangles _ _ sorry _ (instPreadditiveOpposite C) sorry _)
  (Functor.obj (Equivalence.functor (triangleOpEquivalence C))
    (Opposite.op
      (Triangle.mk o.m₁ o.m₃
        ((Triangle.mk u₁₂ v₁₂ w₁₂).mor₂.unop ≫
          CategoryStruct.comp (Y :=
            Opposite.unop
              (Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C 1))
                (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
            (Quiver.Hom.unop
              (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
                (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁))
            (Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃.unop)))))
Tactic: have := op_distinguished _ o.mem
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
M : Type u_1
inst_2 : AddGroup M
inst_3 : HasShift.{v, u, u_1} C M
inst_4 : HasZeroMorphisms.{v, u} C
inst_5 : P.IsStableUnderShift M
n : M
Y : C
hY : P.rightOrthogonal Y
X : C
f : X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y
hX : P X
⊢ f = 0
have obtain : ∀ (g : Functor.obj.{v, v, u, u} (Equivalence.functor (Equivalence.symm (shiftEquiv C n))) X ⟶ Y),
  Eq (α := X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y)
    ((Adjunction.homEquiv (Equivalence.toAdjunction (Equivalence.symm (shiftEquiv C n))) X Y :
          (a : (shiftEquiv C n).symm.functor.obj X ⟶ Y) → X ⟶ (shiftEquiv C n).symm.inverse.obj Y)
        g :
      X ⟶ Functor.obj.{v, v, u, u} (Equivalence.inverse (Equivalence.symm (shiftEquiv C n))) Y)
    (0 : X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C n) Y)
Tactic: obtain ⟨g, rfl⟩ := ((shiftEquiv C n).symm.toAdjunction.homEquiv _ _).surjective f
Cleared hypotheses: f