awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _)
    (Triangle.mk
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
      (NatTrans.app
        {
          app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
            X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
              X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                Functor.map (shiftFunctor C (A := ℤ) 1)
                  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
          naturality := ⋯ }
        (mk₂ f g)))
have refine : Triangle.mk
    ((F.mapComposableArrows 1 ⋙ X.ω₁).map
      (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
    ((F.mapComposableArrows 1 ⋙ X.ω₁).map
      (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
    (NatTrans.app
      {
        app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
          X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
            X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
              Functor.map (shiftFunctor C (A := ℤ) 1)
                (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE sorry))).inv),
        naturality := sorry }
      (mk₂ f g)) ≅
  X.triangle (F.map f) (F.map g)
Tactic: refine isomorphic_distinguished _ (X.triangle_distinguished (F.map f) (F.map g)) _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Eq (α := X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ f)) ⟶ X.ω₁.obj (mk₁ (F.map f ≫ F.map g)))
    (CategoryStruct.comp (Y := X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))))
      (X.ω₁.map (Functor.map (F.mapComposableArrows 1) (homMk₁ (𝟙 w) g ⋯)))
      (X.ω₁.map (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) ⋯))))
    (X.ω₁.map (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) ⋯).hom ≫
      X.ω₁.map (twoδ₂Toδ₁ (F.map f) (F.map g) (F.map f ≫ F.map g) ⋯))
have refine_1 : Eq (α := X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ f)) ⟶ X.ω₁.obj (mk₁ (F.map f ≫ F.map g)))
  (X.ω₁.map
    (CategoryStruct.comp (Y := Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g)))
      (Functor.map (F.mapComposableArrows 1) (homMk₁ (𝟙 w) g sorry))
      (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) sorry))))
  (X.ω₁.map
    ((isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) sorry).hom ≫ twoδ₂Toδ₁ (F.map f) (F.map g) (F.map f ≫ F.map g) sorry))
Tactic: simp only [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Eq (α := X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ f)) ⟶ X.ω₁.obj (mk₁ (F.map f ≫ F.map g)))
    (X.ω₁.map
      (CategoryStruct.comp (Y := Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g)))
        (Functor.map (F.mapComposableArrows 1) (homMk₁ (𝟙 w) g ⋯))
        (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) ⋯))))
    (X.ω₁.map
      ((isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) ⋯).hom ≫
        twoδ₂Toδ₁ (F.map f) (F.map g) (F.map f ≫ F.map g) ⋯))
have refine_1 : Eq (α := Functor.obj (F.mapComposableArrows 1) (mk₁ f) ⟶ mk₁ (F.map f ≫ F.map g))
  (CategoryStruct.comp (Y := Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g)))
    (Functor.map (F.mapComposableArrows 1) (homMk₁ (𝟙 w) g sorry))
    (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) sorry)))
  ((isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) sorry).hom ≫ twoδ₂Toδ₁ (F.map f) (F.map g) (F.map f ≫ F.map g) sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Eq (α := X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
    (X.ω₁.map (Functor.map (F.mapComposableArrows 1) (homMk₁ f (𝟙 w_2) ⋯)) ≫
        X.ω₁.map (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) ⋯).hom :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
    (X.ω₁.map (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) ⋯)) ≫
        X.ω₁.map (twoδ₁Toδ₀ (F.map f) (F.map g) (F.map f ≫ F.map g) ⋯) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
have refine_2 : Eq (α := X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
  (X.ω₁.map
      (Functor.map (F.mapComposableArrows 1) (homMk₁ f (𝟙 w_2) sorry) ≫
        (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) sorry).hom) :
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
  (X.ω₁.map
      (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) sorry) ≫
        twoδ₁Toδ₀ (F.map f) (F.map g) (F.map f ≫ F.map g) sorry) :
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
Tactic: simp only [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Eq (α := X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
    (X.ω₁.map
        (Functor.map (F.mapComposableArrows 1) (homMk₁ f (𝟙 w_2) ⋯) ≫
          (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) ⋯).hom) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
    (X.ω₁.map
        (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) ⋯) ≫
          twoδ₁Toδ₀ (F.map f) (F.map g) (F.map f ≫ F.map g) ⋯) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g))) ⟶ X.ω₁.obj (mk₁ (F.map g)))
have refine_2 : Eq (α := Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g)) ⟶ mk₁ (F.map g))
  (Functor.map (F.mapComposableArrows 1) (homMk₁ f (𝟙 w_2) sorry) ≫
      (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) sorry).hom :
    Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g)) ⟶ mk₁ (F.map g))
  (Iso.hom (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_2)) sorry) ≫
      twoδ₁Toδ₀ (F.map f) (F.map g) (F.map f ≫ F.map g) sorry :
    Functor.obj (F.mapComposableArrows 1) (mk₁ (f ≫ g)) ⟶ mk₁ (F.map g))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
this :
  Eq (α :=
    X.ω₁.obj (mk₁ (F.map g)) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map g))) (X.ω₁.map (homMk₁ (𝟙 (F.obj w_1)) (𝟙 (F.obj w_2)) ⋯))
        (X.δ'.app (mk₂ (F.map f) (F.map g))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) ⋯))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
⊢ Eq (α :=
    X.ω₁.obj (mk₁ (F.map g)) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)))
        (Functor.map (shiftFunctor C (A := ℤ) 1)
          (X.ω₁.map
            ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) ⋯).hom))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso g).inv ≫ (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) ⋯).hom) ≫
        X.δ'.app (mk₂ (F.map f) (F.map g)) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
have h : X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) sorry).hom) =
  X.ω₁.map (homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) sorry)
Tactic: convert! this.symm using 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
this :
  Eq (α :=
    X.ω₁.obj (mk₁ (F.map g)) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map g))) (X.ω₁.map (homMk₁ (𝟙 (F.obj w_1)) (𝟙 (F.obj w_2)) ⋯))
        (X.δ'.app (mk₂ (F.map f) (F.map g))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) ⋯))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
h :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) ⋯).hom) =
    X.ω₁.map (homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) ⋯)
⊢ Eq (α :=
    X.ω₁.obj (mk₁ (F.map g)) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)))
        (Functor.map (shiftFunctor C (A := ℤ) 1)
          (X.ω₁.map
            ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) ⋯).hom))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso g).inv ≫ (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) ⋯).hom) ≫
        X.δ'.app (mk₂ (F.map f) (F.map g)) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
have h₁ : (F.mapComposableArrowsObjMk₁Iso g).inv ≫ (isoMk₁ (Iso.refl (F.obj w_1)) (Iso.refl (F.obj w_2)) sorry).hom =
  homMk₁ (𝟙 (F.obj w_1)) (𝟙 (F.obj w_2)) sorry
Tactic: convert! this.symm using 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
this :
  Eq (α :=
    X.ω₁.obj (mk₁ (F.map g)) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map g))) (X.ω₁.map (homMk₁ (𝟙 (F.obj w_1)) (𝟙 (F.obj w_2)) ⋯))
        (X.δ'.app (mk₂ (F.map f) (F.map g))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) (mk₂ f g)))
        (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) ⋯))) :
      X.ω₁.obj (mk₁ (F.map g)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map f))))
⊢ X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) ⋯).hom) =
    X.ω₁.map (homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) ⋯)
have h : (F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w)) (Iso.refl (F.obj w_1)) sorry).hom =
  homMk₁ (𝟙 (F.obj w)) (𝟙 (F.obj w_1)) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (hypothesis)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι_1
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
F : Functor.{v_1, v_3, u_1, u_3} C D
inst_13 : F.CommShift ℤ
inst_14 : F.IsTriangulated
ι : Type u_4
inst_15 : Category.{v_4, u_4} ι
X Y : Triangulated.SpectralObject.{v_1, u_1, v_4, u_4} C ι
α : X ⟶ Y
i j k : ι
f : i ⟶ j
g : j ⟶ k
⊢ Eq (α :=
    (Triangulated.SpectralObject.ω₁ (X.mapTriangulatedFunctor F)).obj (mk₁ g) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1)
        ((Triangulated.SpectralObject.ω₁ (Y.mapTriangulatedFunctor F)).obj (mk₁ f)))
    (Triangulated.SpectralObject.δ (X.mapTriangulatedFunctor F) f g ≫
      map (shiftFunctor D (A := ℤ) 1) ((whiskerRight α.hom F).app (mk₁ f)))
    ((whiskerRight α.hom F).app (mk₁ g) ≫ Triangulated.SpectralObject.δ (Y.mapTriangulatedFunctor F) f g)
have hf : Eq (α :=
  (shiftFunctor C (A := ℤ) 1 ⋙ F).obj (X.ω₁.obj (mk₁ f)) ⟶ (F ⋙ shiftFunctor D (A := ℤ) 1).obj (Y.ω₁.obj (mk₁ f)))
  ((shiftFunctor C (A := ℤ) 1 ⋙ F).map (α.hom.app (mk₁ f)) ≫
    NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
  (NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
    (F ⋙ shiftFunctor D (A := ℤ) 1).map (α.hom.app (mk₁ f)))
Tactic: have hf := (F.commShiftIso (1 : ℤ)).hom.naturality (α.hom.app (mk₁ f))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι_1
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
F : Functor.{v_1, v_3, u_1, u_3} C D
inst_13 : F.CommShift ℤ
inst_14 : F.IsTriangulated
ι : Type u_4
inst_15 : Category.{v_4, u_4} ι
X Y : Triangulated.SpectralObject.{v_1, u_1, v_4, u_4} C ι
α : X ⟶ Y
i j k : ι
f : i ⟶ j
g : j ⟶ k
hf :
  Eq (α :=
    (shiftFunctor C (A := ℤ) 1 ⋙ F).obj (X.ω₁.obj (mk₁ f)) ⟶ (F ⋙ shiftFunctor D (A := ℤ) 1).obj (Y.ω₁.obj (mk₁ f)))
    ((shiftFunctor C (A := ℤ) 1 ⋙ F).map (α.hom.app (mk₁ f)) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
      (F ⋙ shiftFunctor D (A := ℤ) 1).map (α.hom.app (mk₁ f)))
⊢ Eq (α :=
    (Triangulated.SpectralObject.ω₁ (X.mapTriangulatedFunctor F)).obj (mk₁ g) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1)
        ((Triangulated.SpectralObject.ω₁ (Y.mapTriangulatedFunctor F)).obj (mk₁ f)))
    (Triangulated.SpectralObject.δ (X.mapTriangulatedFunctor F) f g ≫
      map (shiftFunctor D (A := ℤ) 1) ((whiskerRight α.hom F).app (mk₁ f)))
    ((whiskerRight α.hom F).app (mk₁ g) ≫ Triangulated.SpectralObject.δ (Y.mapTriangulatedFunctor F) f g)
have dsimp : Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
  ((F.map (X.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f))) ≫
    map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
  (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
Tactic: dsimp at hf ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι_1
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
F : Functor.{v_1, v_3, u_1, u_3} C D
inst_13 : F.CommShift ℤ
inst_14 : F.IsTriangulated
ι : Type u_4
inst_15 : Category.{v_4, u_4} ι
X Y : Triangulated.SpectralObject.{v_1, u_1, v_4, u_4} C ι
α : X ⟶ Y
i j k : ι
f : i ⟶ j
g : j ⟶ k
hf :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ f))) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
⊢ Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    ((F.map (X.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f))) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
have rw : Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
  (F.map (X.δ f g) ≫
    NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
  (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
Tactic: rw [Category.assoc, ← hf, ← F.map_comp_assoc, α.comm, F.map_comp_assoc]