awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
h₂ : Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) = e.hom.hom₂
⊢ T₁ ≅ T₂
have h₃ : T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃
Tactic: have h₃ := e.hom.comm₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
h₂ : Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) = e.hom.hom₂
h₃ : T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃
⊢ T₁ ≅ T₂
have h₄ : Eq (α :=
  Functor.obj.{v, v, u, u} (𝟭 C) T₁.obj₃ ⟶
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1) T₂.obj₃)
  (Functor.map (𝟭 C) e₃.hom ≫
    NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
  (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
    Functor.map (shiftFunctor C (A := ℤ) (-1) ⋙ shiftFunctor C (A := ℤ) 1) e₃.hom)
Tactic: have h₄ := (shiftFunctorCompIsoId C (-1 : ℤ) 1 (by simp)).inv.naturality e₃.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₁.3) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₂.3
h₄ :
  Eq (α :=
    T₁.obj₃ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (e₃.hom ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom))
⊢ T₁ ≅ T₂
have refine_1 : T₁.mor₁ ≫ Iso.hom (Functor.mapIso Triangle.π₃ e) = e₁.hom ≫ T₂.mor₁
Tactic: refine Triangle.isoMk _ _ e₁ (Triangle.π₃.mapIso e) e₃ ?_ ?_ comm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₁.3) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₂.3
h₄ :
  Eq (α :=
    T₁.obj₃ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (e₃.hom ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom))
refine_1 : T₁.mor₁ ≫ Iso.hom (Functor.mapIso Triangle.π₃ e) = e₁.hom ≫ T₂.mor₁
⊢ T₁ ≅ T₂
have refine_2 : T₁.mor₂ ≫ e₃.hom = Iso.hom (Functor.mapIso Triangle.π₃ e) ≫ T₂.mor₂
Tactic: refine Triangle.isoMk _ _ e₁ (Triangle.π₃.mapIso e) e₃ ?_ ?_ comm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Rotate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
⊢ X_1.rotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₂ =
    Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁ ≫ Y.rotate.mor₃
have dsimp : Eq (α :=
  Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X_1.obj₁ ⟶
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y.obj₂)
  ((-Functor.map (shiftFunctor C (A := ℤ) 1) X_1.mor₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₂)
  (Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁ ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) Y.mor₁))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Rotate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
⊢ X_1.invRotate.mor₁ ≫ f.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) f.hom₃ ≫ Y.invRotate.mor₁
have dsimp : Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
  ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) X_1.obj₁) ≫
      f.hom₁ :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
  (Functor.map (shiftFunctor C (A := ℤ) (-1)) f.hom₃ ≫
      (-Functor.map (shiftFunctor C (A := ℤ) (-1)) Y.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) Y.obj₁) :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Rotate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) f.hom₃ ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) Y.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
have simp : Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
  ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) X_1.obj₁) ≫
      f.hom₁ :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
  (-Functor.map (shiftFunctor C (A := ℤ) (-1)) (X_1.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) Y.obj₁ :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
Tactic: simp only [comp_neg, ← Functor.map_comp_assoc, ← f.comm₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Rotate (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (-Functor.map (shiftFunctor C (A := ℤ) (-1)) (X_1.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
have rw : Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
  ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) X_1.obj₁) ≫
      f.hom₁ :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
  (-(Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
          Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁)) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) Y.obj₁ :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
Tactic: rw [Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (hypothesis)
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} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
⊢ (functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁).map f ≫
      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) =
    (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)) ≫
      (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙ (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1).map f
have this : Eq (α :=
  (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).obj (Functor.obj (F.mapComposableArrows 2) D₁) ⟶
    (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).obj
      (Functor.obj (F.mapComposableArrows 2) D₂))
  ((functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).map (Functor.map (F.mapComposableArrows 2) f) ≫
    X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
  (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
    (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).map
      (Functor.map (F.mapComposableArrows 2) f))
Tactic: have := X.δ'.naturality ((F.mapComposableArrows 2).map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (hypothesis)
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} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
this :
  Eq (α :=
    (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).obj (Functor.obj (F.mapComposableArrows 2) D₁) ⟶
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).obj
        (Functor.obj (F.mapComposableArrows 2) D₂))
    ((functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).map (Functor.map (F.mapComposableArrows 2) f) ≫
      X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
    (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).map
        (Functor.map (F.mapComposableArrows 2) f))
⊢ (functorArrows ι' 1 2 2 _proof_2 _proof_4 ⋙ F.mapComposableArrows 1 ⋙ X.ω₁).map f ≫
      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) =
    (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)) ≫
      (functorArrows ι' 0 1 2 _proof_6 _proof_2 ⋙ (F.mapComposableArrows 1 ⋙ X.ω₁) ⋙ shiftFunctor C (A := ℤ) 1).map f
have this₁ : Eq (α :=
  X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE sorry)))) ⟶
    (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).obj
      (Functor.obj (F.mapComposableArrows 2) D₂))
  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE sorry))).hom ≫
    (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).map (Functor.map (F.mapComposableArrows 2) f) ≫
      X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE sorry))).hom ≫
    X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).map
        (Functor.map (F.mapComposableArrows 2) f))
Tactic: rw [← cancel_epi (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso _).hom)] at this
Cleared hypotheses: this
-- 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} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
this :
  Eq (α :=
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯)))))
        (X.ω₁.map
          ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂)) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₁.map (homOfLE ⋯))))))
          (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁))
          (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₁.map (homOfLE ⋯))))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (Functor.map (shiftFunctor C (A := ℤ) 1)
      (X.ω₁.map
        ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
          Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
            (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom)))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯)))
have h : (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE sorry))).inv ≫
    Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 0) (f.app 1) sorry) ≫
      (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE sorry))).hom =
  homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) sorry
Tactic: congr 2
-- 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_1 : Type u_3
inst_7 : Category.{v_3, u_3} D_1
inst_8 : HasZeroObject.{v_3, u_3} D_1
inst_9 : HasShift.{v_3, u_3, 0} D_1 ℤ
inst_10 : Preadditive.{v_3, u_3} D_1
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D_1 n)
inst_12 : Pretriangulated.{v_3, u_3} D_1
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} ι' ι
D : ComposableArrows.{u_5, u_4} ι' 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) D))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) D))
      (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 := ⋯ }
        D))
have obtain : ∀ (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 sorry))).inv),
          naturality := sorry }
        (mk₂ f g)))
Tactic: obtain ⟨_, _, _, f, g, rfl⟩ := ComposableArrows.mk₂_surjective D
Cleared hypotheses: D