awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b_1 b : EInt
X_1 X : C
⊢ IsIso ((t.eTruncLTGELTSelfToGELT a b).app X)
have bot : IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj b).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊥ b) X)
Tactic: induction a using WithBotTop.rec with
  | bot => simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X)))
  | coe a =>
    induction b using WithBotTop.rec with
    | bot => simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)
    | coe b =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top => simpa using inferInstanceAs (IsIso (𝟙 _))
  | top =>
    exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _,
      IsZero.eq_of_src (by simp) _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b_1 b : EInt
X_1 X : C
bot :
  IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊥ b) X)
⊢ IsIso ((t.eTruncLTGELTSelfToGELT a b).app X)
have coe : ∀ (a : ℤ),
  IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) b) X)
Tactic: induction a using WithBotTop.rec with
  | bot => simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X)))
  | coe a =>
    induction b using WithBotTop.rec with
    | bot => simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)
    | coe b =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top => simpa using inferInstanceAs (IsIso (𝟙 _))
  | top =>
    exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _,
      IsZero.eq_of_src (by simp) _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b_1 b : EInt
X_1 X : C
bot :
  IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊥ b) X)
coe :
  ∀ (a : ℤ),
    IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj b).obj X)
      (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) b) X)
⊢ IsIso ((t.eTruncLTGELTSelfToGELT a b).app X)
have top : IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊤ ⋙ t.eTruncLT.obj b).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊤ b) X)
Tactic: induction a using WithBotTop.rec with
  | bot => simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X)))
  | coe a =>
    induction b using WithBotTop.rec with
    | bot => simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)
    | coe b =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top => simpa using inferInstanceAs (IsIso (𝟙 _))
  | top =>
    exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _,
      IsZero.eq_of_src (by simp) _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Heart (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
⊢ t.heart.ι.essImage = t.heart
have h : ∀ (X : C), t.heart.ι.essImage X ↔ t.heart X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Heart (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
H : Type u'
inst_6 : Category.{v', u'} H
inst_7 : Preadditive.{v', u'} H
inst_8 : Heart.{v', u', v, u} t H
X : H
⊢ t.heart (Functor.obj.{v', v, u', u} t.ιHeart X)
have rw : Functor.essImage.{v', v, u', u} (C := H) t.ιHeart (Functor.obj.{v', v, u', u} t.ιHeart X)
Tactic: rw [← t.essImage_ιHeart H]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
X Y : P.FullSubcategory
f : X ⟶ Y
hX : t.le 0 (X.obj (P := P))
hY : t.ge 1 (Y.obj (P := P))
⊢ P.ι.map f = P.ι.map 0
have rw : P.ι.map f = 0
Tactic: rw [Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P : ObjectProperty.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
inst_6 : P.IsTriangulated
h : P.HasInducedTStructure t
A : P.FullSubcategory
⊢ ∃ (X : P.FullSubcategory) (Y : P.FullSubcategory) (_ : t.le 0 (X.obj (P := P))) (_ : t.ge 1 (Y.obj (P := P))) (f :
    X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
      (@distinguishedTriangles _ _ ⋯ _ (Preadditive.fullSubcategory P) ⋯ _) (Triangle.mk f g h)
have obtain : ∀ (X Y : C) (hX : t.IsLE X 0) (hY : t.IsGE Y 1) (f : X ⟶ A.obj (P := P)) (g : A.obj (P := P) ⟶ Y)
  (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
  (hT :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f g h))
  (X' : C) (hX' : P X') (e : X ≅ X') (Y' : C) (hY' : P Y') (e' : Y ≅ Y'),
  ∃ (X : P.FullSubcategory) (Y : P.FullSubcategory) (_ : t.le 0 (X.obj (P := P))) (_ : t.ge 1 (Y.obj (P := P))) (f :
    X ⟶ A) (g : A ⟶ Y) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
      (@distinguishedTriangles _ _ sorry _ (Preadditive.fullSubcategory P) sorry _) (Triangle.mk f g h)
Tactic: obtain ⟨X, Y, hX, hY, f, g, h, hT, ⟨X', hX', ⟨e⟩⟩, ⟨Y', hY', ⟨e'⟩⟩⟩ :=
      h.exists_triangle_zero_one A.1 A.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsLE
    (Triangle.obj₁
      (Functor.obj (C := Triangle.{v_1, u_1} P.FullSubcategory)
        (P.ι.mapTriangle : Triangle.{v_1, u_1} P.FullSubcategory ⥤ Triangle.{v_1, u_1} C)
        (Functor.obj
            (TStructure.triangleLEGE (P.tStructure t) n₀ n₁ h :
              P.FullSubcategory ⥤ Triangle.{v_1, u_1} P.FullSubcategory)
            (FullSubcategory.mk (P := P) T.obj₂ h₂) :
          Triangle.{v_1, u_1} P.FullSubcategory)))
    n₀
have dsimp : t.IsLE (((TStructure.truncLE (P.tStructure t) n₀).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₀
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsLE (((TStructure.truncLE (P.tStructure t) n₀).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₀
have rw : TStructure.IsLE (P.tStructure t) ((TStructure.truncLE (P.tStructure t) n₀).obj (FullSubcategory.mk (P := P) T.obj₂ h₂))
  n₀
Tactic: rw [← P.tStructure_isLE_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsGE
    (Triangle.obj₃
      (Functor.obj (C := Triangle.{v_1, u_1} P.FullSubcategory)
        (P.ι.mapTriangle : Triangle.{v_1, u_1} P.FullSubcategory ⥤ Triangle.{v_1, u_1} C)
        (Functor.obj
            (TStructure.triangleLEGE (P.tStructure t) n₀ n₁ h :
              P.FullSubcategory ⥤ Triangle.{v_1, u_1} P.FullSubcategory)
            (FullSubcategory.mk (P := P) T.obj₂ h₂) :
          Triangle.{v_1, u_1} P.FullSubcategory)))
    n₁
have dsimp : t.IsGE (((TStructure.truncGE (P.tStructure t) n₁).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsGE (((TStructure.truncGE (P.tStructure t) n₁).obj (FullSubcategory.mk (P := P) T.obj₂ h₂)).obj (P := P)) n₁
have rw : TStructure.IsGE (P.tStructure t) ((TStructure.truncGE (P.tStructure t) n₁).obj (FullSubcategory.mk (P := P) T.obj₂ h₂))
  n₁
Tactic: rw [← P.tStructure_isGE_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_7 : P.IsClosedUnderIsomorphisms
inst_8 : P.HasInducedTStructure t
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ P T.obj₁ ∧ P T.obj₃
have obtain : ∀
  (e :
    T ≅
      Functor.obj (C := Triangle.{v_1, u_1} P.FullSubcategory)
        (P.ι.mapTriangle : Triangle.{v_1, u_1} P.FullSubcategory ⥤ Triangle.{v_1, u_1} C)
        (Functor.obj
            (TStructure.triangleLEGE (P.tStructure t) n₀ n₁ h :
              P.FullSubcategory ⥤ Triangle.{v_1, u_1} P.FullSubcategory)
            (FullSubcategory.mk (P := P) T.obj₂ h₂) :
          Triangle.{v_1, u_1} P.FullSubcategory)),
  e.hom.hom₂ = Iso.hom (Iso.refl T.obj₂) → P T.obj₁ ∧ P T.obj₃
Tactic: obtain ⟨e, _⟩ := t.triangle_iso_exists hT
    (P.ι.map_distinguished _ ((P.tStructure t).triangleLEGE_distinguished n₀ n₁ h ⟨_, h₂⟩))
    (Iso.refl _) n₀ n₁ inferInstance inferInstance
      (by dsimp; rw [← P.tStructure_isLE_iff]; infer_instance)
      (by dsimp; rw [← P.tStructure_isGE_iff]; infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsLE ((t.triangleLEGE n (n + 1) ⋯).obj X).obj₁ n
have dsimp : t.IsLE ((t.truncLE n).obj X) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsGE ((t.triangleLEGE n (n + 1) ⋯).obj X).obj₃ (n + 1)
have dsimp : t.IsGE ((t.truncGE (n + 1)).obj X) (n + 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsLE ((t.triangleLEGE (n - 1) n ⋯).obj X).obj₁ (n - 1)
have dsimp : t.IsLE ((t.truncLE (n - 1)).obj X) (n - 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Induced (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
P_1 : ObjectProperty.{v_1, u_1} C
t_1 : TStructure.{v_1, u_1} C
inst_6 : P_1.IsTriangulated
h : P_1.HasInducedTStructure t_1
P P' : ObjectProperty.{v_1, u_1} C
inst_7 : P.IsTriangulated
inst_8 : P'.IsTriangulated
t : TStructure.{v_1, u_1} C
inst_9 : P.HasInducedTStructure t
inst_10 : P'.HasInducedTStructure t
inst_11 : P.IsClosedUnderIsomorphisms
inst_12 : P'.IsClosedUnderIsomorphisms
X : C
hX : P X
hX' : P' X
n : ℤ
⊢ t.IsGE ((t.triangleLEGE (n - 1) n ⋯).obj X).obj₃ n
have dsimp : t.IsGE ((t.truncGE n).obj X) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
⊢ t.ω₁.map (homMk₁ (φ.app 1) (φ.app 2) ⋯) ≫ t.ω₁δ a' b' c' hab' hbc' =
    t.ω₁δ a b c hab hbc ≫ Functor.whiskerRight (t.ω₁.map (homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C (A := ℤ) 1)
have w : ∀ (x : C),
  NatTrans.app (t.ω₁.map (homMk₁ (φ.app 1) (φ.app 2) sorry) ≫ t.ω₁δ a' b' c' hab' hbc') x =
    NatTrans.app
      (t.ω₁δ a b c hab hbc ≫ Functor.whiskerRight (t.ω₁.map (homMk₁ (φ.app 0) (φ.app 1) sorry)) (shiftFunctor C (A := ℤ) 1))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
x : C
⊢ NatTrans.app (t.ω₁.map (homMk₁ (φ.app 1) (φ.app 2) ⋯) ≫ t.ω₁δ a' b' c' hab' hbc') x =
    NatTrans.app
      (t.ω₁δ a b c hab hbc ≫ Functor.whiskerRight (t.ω₁.map (homMk₁ (φ.app 0) (φ.app 1) ⋯)) (shiftFunctor C (A := ℤ) 1))
      x
have w : Eq (α :=
  (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
  (CategoryStruct.comp (Y := (t.eTruncGE.obj b').obj ((t.eTruncLT.obj c).obj x))
        (NatTrans.app (t.eTruncGE.map (φ.app 1)) ((t.eTruncLT.obj c).obj x))
        ((t.eTruncGE.obj b').map (NatTrans.app (t.eTruncLT.map (φ.app 2)) x)) ≫
      (t.ω₁δ a' b' c' hab' hbc').app x :
    (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
  ((t.ω₁δ a b c hab hbc).app x ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (CategoryStruct.comp (Y := (t.eTruncGE.obj a').obj ((t.eTruncLT.obj b).obj x))
          (NatTrans.app (t.eTruncGE.map (φ.app 0)) ((t.eTruncLT.obj b).obj x))
          ((t.eTruncGE.obj a').map (NatTrans.app (t.eTruncLT.map (φ.app 1)) x))) :
    (t.eTruncGE.obj b).obj ((t.eTruncLT.obj c).obj x) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        ((t.eTruncGE.obj a').obj ((t.eTruncLT.obj b').obj x)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.triangleω₁δ a b c hab hbc).obj X ≅ (t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)
have refine_1 : ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) =
  ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
        (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom ≫
    ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE sorry))).obj X)).mor₁
Tactic: refine Triangle.isoMk _ _ ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
    (t.eTruncLTGEIsoGELT a b).symm.app _) (Iso.refl _) ((t.eTruncGEIsoGEGE a b hab).app _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
refine_1 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) =
    ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
          (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₁
⊢ (t.triangleω₁δ a b c hab hbc).obj X ≅ (t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)
have refine_2 : ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫
    Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) =
  Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) ≫
    ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE sorry))).obj X)).mor₂
Tactic: refine Triangle.isoMk _ _ ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
    (t.eTruncLTGEIsoGELT a b).symm.app _) (Iso.refl _) ((t.eTruncGEIsoGEGE a b hab).app _) ?_ ?_ ?_