awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ t.IsLE ((t.truncLT n₁).obj Y) n₀
have rw : t.IsLE ((t.truncLT (n₀ + 1)).obj Y) n₀
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ t.IsGE ((t.triangleLTGE n₁).obj Y).obj₃ n₁
have dsimp : t.IsGE ((t.truncGE n₁).obj Y) n₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ t.IsGE (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h).obj₃ n₁
have dsimp : t.IsGE ((t.truncGE n₁).obj Z) n₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
⊢ IsIso ((t.truncGE n₁).map g)
have refine_2 : ∀ (e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
  (he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)), IsIso ((t.truncGE n₁).map g)
Tactic: obtain ⟨e, he⟩ :=
      t.triangle_iso_exists (t.triangleLTGE_distinguished n₁ Y) mem (Iso.refl _) n₀ n₁
        (by dsimp; rw [← hn]; infer_instance) (by dsimp; infer_instance)
        (by dsimp; infer_instance) (by dsimp; infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)
this : (t.truncGE n₁).map g = e.hom.hom₃
⊢ IsIso ((t.truncGE n₁).map g)
have rw : IsIso e.hom.hom₃
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
h_1 :
  ∃ (X : C) (f : X ⟶ Y) (h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)),
    t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h)
h_2 : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = Iso.hom (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂)
⊢ IsIso ((t.truncGE n₁).map g)
have refine_2 : (t.truncGE n₁).map g = e.hom.hom₃
Tactic: suffices ((t.truncGE n₁).map g) = e.hom.hom₃ by rw [this]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
X : C
a b : ℤ
inst_6 : t.IsLE X b
⊢ t.IsLE ((t.truncLT a).obj X) b
have pos : ∀ (h : a ≤ b + 1), t.IsLE ((t.truncLT a).obj X) b
Tactic: by_cases h : a ≤ b + 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
X : C
a b : ℤ
inst_6 : t.IsLE X b
pos : ∀ (h : a ≤ b + 1), t.IsLE ((t.truncLT a).obj X) b
⊢ t.IsLE ((t.truncLT a).obj X) b
have neg : ∀ (h : ¬a ≤ b + 1), t.IsLE ((t.truncLT a).obj X) b
Tactic: by_cases h : a ≤ b + 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
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
X : C
a b : ℤ
inst_6 : t.IsLE X b
h : ¬a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b
have this : IsIso ((t.truncLTι a).app X)
Tactic: have := (t.isLE_iff_isIso_truncLTι_app (a - 1) a (by lia) X).1 (t.isLE_of_le _ b _ (by lia))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
X : C
a b : ℤ
inst_6 : t.IsGE X a
⊢ t.IsGE ((t.truncGE b).obj X) a
have pos : ∀ (h : a ≤ b), t.IsGE ((t.truncGE b).obj X) a
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
X : C
a b : ℤ
inst_6 : t.IsGE X a
pos : ∀ (h : a ≤ b), t.IsGE ((t.truncGE b).obj X) a
⊢ t.IsGE ((t.truncGE b).obj X) a
have neg : ∀ (h : ¬a ≤ b), t.IsGE ((t.truncGE b).obj X) a
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
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
X : C
a b : ℤ
inst_6 : t.IsGE X a
h : ¬a ≤ b
⊢ t.IsGE ((t.truncGE b).obj X) a
have this : t.IsGE X b
Tactic: have : t.IsGE X b := t.isGE_of_ge X b a (by lia)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
X : C
a b : ℤ
⊢ t.IsGE ((t.truncGELT a b).obj X) a
have dsimp : t.IsGE ((t.truncGE a).obj ((t.truncLT b).obj X)) a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
X : C
a b : ℤ
⊢ t.IsLE ((t.truncLTGE a b).obj X) (b - 1)
have dsimp : t.IsLE ((t.truncLT b).obj ((t.truncGE a).obj X)) (b - 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
⊢ IsIso ((t.truncLT n).map T.mor₁)
have rw : ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)) (_
  :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
  t.IsGE Z n
Tactic: rw [isIso_truncLT_map_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
⊢ ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
    t.IsGE Z n
have obtain : ∀ (Z : C) (g : T.obj₂ ⟶ Z) (k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
  (mem :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)),
  ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
    t.IsGE Z n
Tactic: obtain ⟨Z, g, k, mem⟩ := distinguished_cocone_triangle ((t.truncLTι n).app T.obj₁ ≫ T.mor₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
⊢ ∃ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁))
    (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g h)),
    t.IsGE Z n
have refine : t.IsGE Z n
Tactic: refine ⟨_, _, _, mem, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) ((t.truncLT n).obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k)
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
⊢ t.IsGE (Triangle.mk H.m₁ H.m₃ (T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncGEπ n).app T.obj₁))).obj₁ n
have dsimp : t.IsGE ((t.truncGE n).obj T.obj₁) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
⊢ IsIso ((t.truncGE n₁).map T.mor₂)
have rw : ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
  t.IsLE X n₀
Tactic: rw [isIso_truncGE_map_iff _ _ _ _ h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
⊢ ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_
    :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
    t.IsLE X n₀
have obtain : ∀ (X : C) (f : X ⟶ T.obj₂) (k : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
  (mem :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) k)),
  ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_
    :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
    t.IsLE X n₀
Tactic: obtain ⟨X, f, k, mem⟩ := distinguished_cocone_triangle₁ (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) k)
⊢ ∃ (X : C) (f : X ⟶ T.obj₂) (h : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_
    :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) h)),
    t.IsLE X n₀
have refine : t.IsLE X n₀
Tactic: refine ⟨_, _, _, mem, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE n₁).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) k)
⊢ t.IsLE X n₀
have subst : ∀ (k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
  (mem :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)),
  t.IsLE X n₀
Tactic: subst h
Cleared hypotheses: n₁, h, k, mem
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)
⊢ t.IsLE X n₀
have have : ∀ (H : Octahedron sorry sorry sorry sorry), t.IsLE X n₀
Tactic: have H := someOctahedron rfl (rot_of_distTriang _ hT)
    (rot_of_distTriang _ (t.triangleLTGE_distinguished (n₀ + 1) T.obj₃))
    (rot_of_distTriang _ mem)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
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
inst_6 : IsTriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f (T.mor₂ ≫ NatTrans.app (t.truncGEπ (n₀ + 1)) T.obj₃) k)
H : Octahedron ⋯ ⋯ ⋯ ⋯
⊢ t.IsLE X n₀
have this : t.IsLE (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (n₀ - 1)
Tactic: have : t.IsLE (X⟦(1 : ℤ)⟧) (n₀ - 1) :=
    t.isLE₂ _ H.mem (n₀ - 1) (t.isLE_shift T.obj₁ n₀ 1 (n₀ - 1) (by lia))
      (t.isLE_shift ((t.truncLT (n₀ + 1)).obj T.obj₃) n₀ 1 (n₀-1) (by lia))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (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
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
⊢ t.IsGE ((t.truncLT b).obj X) a
have rw : IsZero.{v, u} ((t.truncLT a).obj ((t.truncLT b).obj X))
Tactic: rw [t.isGE_iff_isZero_truncLT_obj]