awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
a b : ℤ
h : a + 1 = b
x : C
⊢ ((t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (Iso.hom (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁))) (shiftFunctor C (A := ℤ) 1)).app
      x =
    ((t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁).app x
have w : ((t.truncGTIsoTruncGE a (a + 1) sorry).hom.app x ≫ (t.truncGEδLE a (a + 1) sorry).app x) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 ((t.truncLE a).obj x)) =
  (t.truncGTIsoTruncGE a b h).hom.app x ≫ (t.truncGEδLE a b h).app x
Tactic: dsimp [truncGTδLE]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
a b : ℤ
h : a + 1 = b
x : C
⊢ ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x ≫ (t.truncGEδLE a (a + 1) ⋯).app x) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 ((t.truncLE a).obj x)) =
    (t.truncGTIsoTruncGE a b h).hom.app x ≫ (t.truncGEδLE a b h).app x
have w : ((t.truncGTIsoTruncGE a (a + 1) sorry).hom.app x ≫ (t.truncGEδLE a (a + 1) sorry).app x) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 ((t.truncLE a).obj x)) =
  (t.truncGTIsoTruncGE a (a + 1) sorry).hom.app x ≫ (t.truncGEδLE a (a + 1) sorry).app x
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
X : C
⊢ t.IsGE X n₁ ↔ IsIso ((t.truncGTπ n₀).app X)
have rw : IsIso ((t.truncGEπ n₁).app X) ↔ IsIso ((t.truncGTπ n₀).app X)
Tactic: rw [t.isGE_iff_isIso_truncGEπ_app n₁ X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
n : ℤ
X : C
⊢ t.IsLE X n ↔ IsZero.{v_1, u_1} ((t.truncGT n).obj X)
have rw : IsIso ((t.truncLEι n).app X) ↔ IsZero.{v_1, u_1} ((t.truncGT n).obj X)
Tactic: rw [t.isLE_iff_isIso_truncLEι_app n X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsGE X n₁ ↔ IsZero.{v_1, u_1} ((t.truncLE n₀).obj X)
have rw : IsIso ((t.truncGEπ n₁).app X) ↔ IsZero.{v_1, u_1} ((t.truncLE n₀).obj X)
Tactic: rw [t.isGE_iff_isIso_truncGEπ_app n₁ X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (hypothesis)
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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst_6 : t.IsLE Y n
⊢ f₁ = f₂
have this : t.IsLE Y (n + 1 - 1)
Tactic: have : t.IsLE Y (n + 1 - 1) := by simpa
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLE n).obj X
h : f₁ ≫ (t.truncLEι n).app X = f₂ ≫ (t.truncLEι n).app X
inst_6 : t.IsLE Y n
this : t.IsLE Y (n + 1 - 1)
⊢ f₁ = f₂
have rw : f₁ ≫ (t.truncLEIsoTruncLT n (n + 1) sorry).hom.app X = f₂ ≫ (t.truncLEIsoTruncLT n (n + 1) sorry).hom.app X
Tactic: rw [← cancel_mono ((t.truncLEIsoTruncLT n (n + 1) rfl).hom.app _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X Y : C
f : X ⟶ Y
n : ℤ
inst_6 : t.IsLE X n
⊢ t.IsGE ((t.triangleLEGT n).obj Y).obj₃ (n + 1)
have dsimp : t.IsGE ((t.truncGT n).obj Y) (n + 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst_6 : t.IsGE Y n₁
⊢ t.IsLE ((t.triangleLEGT n₀).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.TruncLEGT (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
X Y : C
f : X ⟶ Y
a b : ℤ
h : a + 1 = b
⊢ IsIso ((t.truncLE a).map f) ↔
    ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) ((t.truncLE a).obj X))
      (_ :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk ((t.truncLEι a).app X ≫ f) g h)),
      t.IsGE Z b
have subst : IsIso ((t.truncLE a).map f) ↔
  ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) ((t.truncLE a).obj X)) (_
    :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk ((t.truncLEι a).app X ≫ f) g h)),
    t.IsGE Z (a + 1)
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X : C
a b : ℤ
inst_6 : t.IsLE X b
⊢ t.IsLE ((t.truncLE a).obj X) b
have dsimp : t.IsLE ((t.truncLT (a + 1)).obj X) b
Tactic: dsimp [truncLE]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X : C
a b : ℤ
inst_6 : t.IsGE X a
⊢ t.IsGE ((t.truncGT b).obj X) a
have dsimp : t.IsGE ((t.truncGE (b + 1)).obj X) a
Tactic: dsimp [truncGT]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X : C
a b : ℤ
⊢ t.IsGE ((t.truncGELE a b).obj X) a
have dsimp : t.IsGE ((t.truncGE a).obj ((t.truncLE b).obj X)) a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (hypothesis)
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
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.IsGE T.obj₃ n₁
⊢ IsIso ((t.truncLE n₀).map T.mor₁)
have h₄ : t.IsGE T.obj₃ (n₀ + 1)
Tactic: subst h
Cleared hypotheses: n₁, h, h₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X : C
a b : ℤ
inst_7 : t.IsGE X a
⊢ t.IsGE ((t.truncLE b).obj X) a
have dsimp : t.IsGE ((t.truncLT (b + 1)).obj X) a
Tactic: dsimp [truncLE]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X : C
a b : ℤ
inst_7 : t.IsLE X b
⊢ t.IsLE ((t.truncGT a).obj X) b
have dsimp : t.IsLE ((t.truncGE (a + 1)).obj X) b
Tactic: dsimp [truncGT]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (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
X : C
a b : ℤ
⊢ t.IsLE ((t.truncGELE a b).obj X) b
have dsimp : t.IsLE ((t.truncGE a).obj ((t.truncLE b).obj X)) b
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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
this : ∀ (f : T ⟶ T'), f.hom₂ = 0 → f = 0
⊢ f₁ = f₂
have rw : f₁ - f₂ = 0
Tactic: rw [← sub_eq_zero]
-- 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
⊢ f₁ = f₂
have suffices : ∀ (f : T ⟶ T'), f.hom₂ = 0 → f = 0
Tactic: suffices ∀ (f : T ⟶ T'), f.hom₂ = 0 → f = 0 by rw [← sub_eq_zero]; cat_disch
-- 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f = 0
have h₂ : f.hom₁ = TriangleMorphism.hom₁ 0
Tactic: 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
h₂ : f.hom₁ = TriangleMorphism.hom₁ 0
⊢ f = 0
have h₃ : f.hom₂ = TriangleMorphism.hom₂ 0
Tactic: 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
h₂ : f.hom₁ = TriangleMorphism.hom₁ 0
h₃ : f.hom₂ = TriangleMorphism.hom₂ 0
⊢ f = 0
have h₄ : f.hom₃ = TriangleMorphism.hom₃ 0
Tactic: 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₁ = TriangleMorphism.hom₁ 0
have h₂ : ∀ (g : T.obj₁ ⟶ T'.invRotate.obj₁) (hg : f.hom₁ = g ≫ T'.invRotate.mor₁), f.hom₁ = TriangleMorphism.hom₁ 0
Tactic: obtain ⟨g, hg⟩ := Triangle.coyoneda_exact₂ _ (inv_rot_of_distTriang _ hT')
      f.hom₁ (by simp [← f.comm₁, hf])
-- 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
T T' : Triangle.{v, u} C
f₁ f₂ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0
have h₃ : ∀ (g : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T.obj₁ ⟶ T'.obj₃) (hg : f.hom₃ = T.mor₃ ≫ g),
  f.hom₃ = TriangleMorphism.hom₃ 0
Tactic: obtain ⟨g, hg⟩ := T.yoneda_exact₃ hT f.hom₃ (by cat_disch)
-- 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
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
φ : T.obj₂ ⟶ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
⊢ ∃ (f : T ⟶ T'), f.hom₂ = φ
have obtain : ∀ (a : T.obj₁ ⟶ T'.obj₁) (comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁), ∃ (f : T ⟶ T'), f.hom₂ = φ
Tactic: obtain ⟨a, comm₁⟩ := T'.coyoneda_exact₂ hT' (T.mor₁ ≫ φ) (t.zero _ 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
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
φ : T.obj₂ ⟶ T'.obj₂
a_1 b : ℤ
h₀ : t.IsLE T.obj₁ a_1
h₁' : t.IsGE T'.obj₃ b
h : a_1 < b
a : T.obj₁ ⟶ T'.obj₁
comm₁ : T.mor₁ ≫ φ = a ≫ T'.mor₁
⊢ ∃ (f : T ⟶ T'), f.hom₂ = φ
have obtain : ∀ (c : T.obj₃ ⟶ T'.obj₃) (comm₂ : T.mor₂ ≫ c = φ ≫ T'.mor₂)
  (comm₃ : T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T'.mor₃), ∃ (f : T ⟶ T'), f.hom₂ = φ
Tactic: obtain ⟨c, comm₂, comm₃⟩ := complete_distinguished_triangle_morphism _ _ hT hT' a φ 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
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
e : T.obj₂ ≅ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T.obj₃ b
h₀' : t.IsLE T'.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
⊢ ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom
have obtain : ∀ (hom : T ⟶ T') (hhom : hom.hom₂ = e.hom), ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom
Tactic: obtain ⟨hom, hhom⟩ := triangle_map_exists t hT hT' e.hom _ _ h₀ 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
T T' : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _) T'
e : T.obj₂ ≅ T'.obj₂
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T.obj₃ b
h₀' : t.IsLE T'.obj₁ a
h₁' : t.IsGE T'.obj₃ b
h : a < b
hom : T ⟶ T'
hhom : hom.hom₂ = e.hom
⊢ ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom
have obtain : ∀ (inv : T' ⟶ T), inv.hom₂ = e.inv → ∃ (e' : T ≅ T'), e'.hom.hom₂ = e.hom
Tactic: obtain ⟨inv, _⟩ := triangle_map_exists t hT' hT e.inv _ _ h₀' 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 Y : C
φ : X ⟶ Y
H : ∃ (f : triangle t n X ⟶ triangle t n Y), f.hom₂ = φ
⊢ (triangle t n X).mor₁ ≫ φ =
    H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₁ ≫ (triangle t n Y).mor₁
have rw : (triangle t n X).mor₁ ≫ φ =
  (triangle t n X).mor₁ ≫ H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).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
H : ∃ (f : triangle t n X ⟶ triangle t n Y), f.hom₂ = φ
rw :
  (triangle t n X).mor₁ ≫ φ =
    (triangle t n X).mor₁ ≫ H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₂
⊢ (triangle t n X).mor₁ ≫ φ =
    H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₁ ≫ (triangle t n Y).mor₁
have rw₁ : (triangle t n X).mor₁ ≫ φ = (triangle t n X).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
H : ∃ (f : triangle t n X ⟶ triangle t n Y), f.hom₂ = φ
⊢ (triangle t n X).mor₂ ≫ H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₃ =
    φ ≫ (triangle t n Y).mor₂
have rw : H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₂ ≫ (triangle t n Y).mor₂ =
  φ ≫ (triangle t n Y).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
H : ∃ (f : triangle t n X ⟶ triangle t n Y), f.hom₂ = φ
rw :
  H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₂ ≫ (triangle t n Y).mor₂ =
    φ ≫ (triangle t n Y).mor₂
⊢ (triangle t n X).mor₂ ≫ H.choose (p := fun (f : triangle t n X ⟶ triangle t n Y) ↦ f.hom₂ = φ).hom₃ =
    φ ≫ (triangle t n Y).mor₂
have rw₁ : φ ≫ (triangle t n Y).mor₂ = φ ≫ (triangle t n Y).mor₂
Tactic: rw [H.choose.comm₂, H.choose_spec]