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
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
⊢ t.IsLE ((triangleFunctor t n).obj A).obj₁ (n - 1)
have dsimp : t.IsLE (triangle t n A).obj₁ (n - 1)
Tactic: dsimp [triangleFunctor]
-- 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
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
⊢ t.IsGE ((triangleFunctor t n).obj A).obj₃ n
have dsimp : t.IsGE (triangle t n A).obj₃ n
Tactic: dsimp [triangleFunctor]
-- 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
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ (f : triangle t a A ⟶ triangle t b A), f.hom₂ = 𝟙 (triangle t a A).obj₂
⊢ (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ =
    H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₁ ≫
      (triangle t b A).mor₁
have rw : (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ =
  (triangle t a A).mor₁ ≫
    H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₂
Tactic: rw [← H.choose.comm₁, H.choose_spec]
-- 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
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ (f : triangle t a A ⟶ triangle t b A), f.hom₂ = 𝟙 (triangle t a A).obj₂
rw :
  (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ =
    (triangle t a A).mor₁ ≫
      H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₂
⊢ (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ =
    H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₁ ≫
      (triangle t b A).mor₁
have rw₁ : (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ = (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂
Tactic: rw [← H.choose.comm₁, H.choose_spec]
-- 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
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ (f : triangle t a A ⟶ triangle t b A), f.hom₂ = 𝟙 (triangle t a A).obj₂
⊢ (triangle t a A).mor₂ ≫
      H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₃ =
    𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
have rw : H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₂ ≫
    (triangle t b A).mor₂ =
  𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
Tactic: rw [H.choose.comm₂, H.choose_spec]
-- 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
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ (f : triangle t a A ⟶ triangle t b A), f.hom₂ = 𝟙 (triangle t a A).obj₂
rw :
  H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₂ ≫
      (triangle t b A).mor₂ =
    𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
⊢ (triangle t a A).mor₂ ≫
      H.choose (p := fun (f : triangle t a A ⟶ triangle t b A) ↦ f.hom₂ = 𝟙 (triangle t a A).obj₂).hom₃ =
    𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
have rw₁ : 𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂ = 𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
Tactic: rw [H.choose.comm₂, H.choose_spec]
-- 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
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc = triangleFunctorNatTransOfLE t a c ⋯
have app : (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app =
  (triangleFunctorNatTransOfLE t a c sorry).app
Tactic: apply NatTrans.ext
-- 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
a b c : ℤ
hab : a ≤ b
hbc : b ≤ c
⊢ (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app =
    (triangleFunctorNatTransOfLE t a c ⋯).app
have app : ∀ (X : C),
  (triangleFunctorNatTransOfLE t a b hab ≫ triangleFunctorNatTransOfLE t b c hbc).app X =
    (triangleFunctorNatTransOfLE t a c sorry).app X
Tactic: ext1 X
-- 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
a : ℤ
⊢ triangleFunctorNatTransOfLE t a a ⋯ = 𝟙 (triangleFunctor t a)
have app : (triangleFunctorNatTransOfLE t a a sorry).app = NatTrans.app (𝟙 (triangleFunctor t a))
Tactic: apply NatTrans.ext
-- 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
a : ℤ
⊢ (triangleFunctorNatTransOfLE t a a ⋯).app = NatTrans.app (𝟙 (triangleFunctor t a))
have app : ∀ (X : C), (triangleFunctorNatTransOfLE t a a sorry).app X = NatTrans.app (𝟙 (triangleFunctor t a)) X
Tactic: ext1 X
-- 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
n : ℤ
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ (t.truncLT n).map (x_2 + x_3) = (t.truncLT n).map x_2 + (t.truncLT n).map x_3
have dsimp : Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
  HAdd.hAdd (α :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1) (β :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1)
    (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2) :
      Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x) ⟶
        Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x_1))
    (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_3))
Tactic: dsimp only [truncLT, Functor.comp_map]
-- 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
n : ℤ
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1)
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_3))
have rw : Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2 + (TruncAux.triangleFunctor t n).map x_3) =
  HAdd.hAdd (α :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1) (β :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₁).obj x_1)
    (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_2) :
      Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x) ⟶
        Functor.obj Triangle.π₁ ((TruncAux.triangleFunctor t n).obj x_1))
    (Functor.map Triangle.π₁ ((TruncAux.triangleFunctor t n).map x_3))
Tactic: rw [Functor.map_add]
-- 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
n : ℤ
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ (t.truncGE n).map (x_2 + x_3) = (t.truncGE n).map x_2 + (t.truncGE n).map x_3
have dsimp : Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
  HAdd.hAdd (α :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1) (β :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1)
    (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2) :
      Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x) ⟶
        Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x_1))
    (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_3))
Tactic: dsimp only [truncGE, Functor.comp_map]
-- 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
n : ℤ
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map (x_2 + x_3)) =
    HAdd.hAdd (α :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1) (β :=
      (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1)
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2) :
        Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x) ⟶
          Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x_1))
      (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_3))
have rw : Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2 + (TruncAux.triangleFunctor t n).map x_3) =
  HAdd.hAdd (α :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1) (β :=
    (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x ⟶ (TruncAux.triangleFunctor t n ⋙ Triangle.π₃).obj x_1)
    (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_2) :
      Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x) ⟶
        Functor.obj Triangle.π₃ ((TruncAux.triangleFunctor t n).obj x_1))
    (Functor.map Triangle.π₃ ((TruncAux.triangleFunctor t n).map x_3))
Tactic: rw [Functor.map_add]
-- 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 : ℤ
hn : a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) (a - 1)
have dsimp : t.IsLE (TruncAux.triangle t a X).obj₁ (a - 1)
Tactic: dsimp [truncLT]
-- 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 : ℤ
hn : a ≤ b + 1
⊢ t.IsLE ((t.truncLT a).obj X) b
have this : t.IsLE ((t.truncLT a).obj X) (a - 1)
Tactic: have : t.IsLE ((t.truncLT a).obj X) (a - 1) := by dsimp [truncLT]; 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 : ℤ
hn : b ≤ a
⊢ t.IsGE ((t.truncGE a).obj X) a
have dsimp : t.IsGE (TruncAux.triangle t a X).obj₃ a
Tactic: dsimp [truncGE]
-- 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 : ℤ
hn : b ≤ a
⊢ t.IsGE ((t.truncGE a).obj X) b
have this : t.IsGE ((t.truncGE a).obj X) a
Tactic: have : t.IsGE ((t.truncGE a).obj X) a := by dsimp [truncGE]; 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
n : ℤ
⊢ t.IsLE ((t.triangleLTGE n).obj X).obj₁ (n - 1)
have dsimp : t.IsLE ((t.truncLT n).obj X) (n - 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
X : C
n : ℤ
⊢ t.IsGE ((t.triangleLTGE 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.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
a b : ℤ
h : a ≤ b
⊢ t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C (A := ℤ) 1) =
    t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b
have w : ∀ (X : C),
  (t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C (A := ℤ) 1)).app X =
    (t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b).app X
Tactic: ext X
-- 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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsLE X n₀ ↔ IsIso ((t.truncLTι n₁).app X)
have subst : t.IsLE X n₀ ↔ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
Tactic: subst h
Cleared hypotheses: n₁, 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
n₀ : ℤ
X : C
⊢ t.IsLE X n₀ ↔ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
have refine : t.IsLE X n₀ → IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
Tactic: refine ⟨fun _ ↦ ?_,
    fun _ ↦ t.isLE_of_iso (asIso (((t.truncLTι (n₀ + 1))).app X)) n₀⟩
-- 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
n₀ : ℤ
X : C
h : t.IsLE X n₀
⊢ t.IsLE ((t.triangleLTGE (n₀ + 1)).obj X).obj₁ n₀
have dsimp : t.IsLE ((t.truncLT (n₀ + 1)).obj X) 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
n₀ : ℤ
X : C
h : t.IsLE X n₀
⊢ t.IsGE ((t.triangleLTGE (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.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
n₀ : ℤ
X : C
h : t.IsLE X n₀
⊢ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
have obtain : ∀ (e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X) (he : e.hom.hom₂ = Iso.hom (Iso.refl X)),
  IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
Tactic: obtain ⟨e, he⟩ := t.triangle_iso_exists
    (contractible_distinguished X) (t.triangleLTGE_distinguished (n₀ + 1) X)
    (Iso.refl X) n₀ (n₀ + 1)
    (by dsimp; 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
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
⊢ e.inv.hom₂ = 𝟙 X
have rw : TriangleMorphism.hom₂ (𝟙 ((t.triangleLTGE (n₀ + 1)).obj X)) = 𝟙 X ≫ Iso.hom (Iso.refl X)
Tactic: rw [← cancel_mono e.hom.hom₂, ← comp_hom₂, e.inv_hom_id, he]
-- 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
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
⊢ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
have he' : e.inv.hom₂ = 𝟙 X
Tactic: have he' : e.inv.hom₂ = 𝟙 X := by
    rw [← cancel_mono e.hom.hom₂, ← comp_hom₂, e.inv_hom_id, he]
    simp
-- 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
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
he' : e.inv.hom₂ = 𝟙 X
⊢ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
have this : NatTrans.app (t.truncLTι (n₀ + 1)) X = e.inv.hom₁
Tactic: have : (t.truncLTι (n₀ + 1)).app X = e.inv.hom₁ := by
    simpa [he'] using e.inv.comm₁
-- 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
n₀ : ℤ
X : C
h : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = Iso.hom (Iso.refl X)
he' : e.inv.hom₂ = 𝟙 X
this : NatTrans.app (t.truncLTι (n₀ + 1)) X = e.inv.hom₁
⊢ IsIso (X := (t.truncLT (n₀ + 1)).obj X) (NatTrans.app (t.truncLTι (n₀ + 1)) X)
have rw : IsIso e.inv.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
n : ℤ
X : C
⊢ t.IsGE X n ↔ IsIso ((t.truncGEπ n).app X)
have mp : t.IsGE X n → IsIso ((t.truncGEπ n).app X)
Tactic: constructor
-- 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
n : ℤ
X : C
mp : t.IsGE X n → IsIso ((t.truncGEπ n).app X)
⊢ t.IsGE X n ↔ IsIso ((t.truncGEπ n).app X)
have mpr : IsIso ((t.truncGEπ n).app X) → t.IsGE X n
Tactic: constructor
-- 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
n : ℤ
X : C
h : t.IsGE X n
⊢ t.IsLE ((t.triangleLTGE n).obj X).obj₁ (n - 1)
have dsimp : t.IsLE ((t.truncLT n).obj X) (n - 1)
Tactic: dsimp