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
a : ℤ
hab_1 : ⊥ ⟶ WithBotTop.coe a
hab : True
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a))
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a))
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have bot : t.truncGEπ a ≫ t.truncGEδLT a =
  CategoryStruct.comp (Y := 0 ⋙ shiftFunctor C (A := ℤ) 1) 0 (Functor.whiskerRight 0 (shiftFunctor C (A := ℤ) 1))
Tactic: dsimp [eTruncGE, eTruncLT]
-- 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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊤
hab : True
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊤)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊤)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have bot : Eq (α := Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) (𝟭 C ⋙ shiftFunctor C (A := ℤ) 1))
  (CategoryStruct.comp (Y := 0) 0 0)
  (CategoryStruct.comp (Y := 0 ⋙ shiftFunctor C (A := ℤ) 1) 0 (Functor.whiskerRight 0 (shiftFunctor C (A := ℤ) 1)))
Tactic: dsimp [eTruncGE, eTruncLT]
-- 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
b : EInt
a : ℤ
hab_1 : WithBotTop.coe a ⟶ b
hab : WithBotTop.coe a ≤ b
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have coe : ∀ (hab : WithBotTop.coe a ⟶ ⊥) (hab_2 : WithBotTop.coe a ≤ ⊥),
  Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊥)
    (t.eTruncGE.map hab ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
Tactic: induction b using WithBotTop.rec
Cleared hypotheses: b, hab_1, hab
-- 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
b : EInt
a : ℤ
hab_1 : WithBotTop.coe a ⟶ b
hab : WithBotTop.coe a ≤ b
coe :
  ∀ (hab : WithBotTop.coe a ⟶ ⊥) (hab_2 : WithBotTop.coe a ≤ ⊥),
    Eq (α :=
      t.eTruncGE.obj (WithBotTop.coe a) ⟶
        (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊥)
      (t.eTruncGE.map hab ≫
        WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
          t.eTruncGE.obj x ⟶
            (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
          0 t.truncGEδLT 0 ⊥)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
          t.eTruncGE.obj x ⟶
            (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
          0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
        (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have coe₁ : ∀ (a_1 : ℤ) (hab : WithBotTop.coe a ⟶ WithBotTop.coe a_1) (hab_2 : WithBotTop.coe a ≤ WithBotTop.coe a_1),
  Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a_1))
    (t.eTruncGE.map hab ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a_1))
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
Tactic: induction b using WithBotTop.rec
Cleared hypotheses: b, hab_1, hab
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
a a_1 : ℤ
hab_1 : WithBotTop.coe a ⟶ WithBotTop.coe a_1
hab : WithBotTop.coe a ≤ WithBotTop.coe a_1
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a_1))
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a_1))
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have hab₁ : a ≤ a_1
Tactic: simp at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
a : ℤ
hab_1 : WithBotTop.coe a ⟶ ⊤
hab : WithBotTop.coe a ≤ ⊤
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊤)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊤)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have hab₁ : True
Tactic: simp at hab
Cleared hypotheses: hab
-- 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
a a_1 : ℤ
hab_1 : WithBotTop.coe a ⟶ WithBotTop.coe a_1
hab : a ≤ a_1
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a_1))
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a_1))
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have coe : t.natTransTruncGEOfLE a a_1 sorry ≫ t.truncGEδLT a_1 =
  t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a a_1 sorry) (shiftFunctor C (A := ℤ) 1)
Tactic: dsimp [eTruncGE, eTruncLT]
-- 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
a : ℤ
hab_1 : WithBotTop.coe a ⟶ ⊤
hab : True
⊢ Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊤)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊤)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have coe : CategoryStruct.comp (Y := 0) 0 0 = t.truncGEδLT a ≫ Functor.whiskerRight (t.truncLTι a) (shiftFunctor C (A := ℤ) 1)
Tactic: dsimp [eTruncGE, eTruncLT]
-- 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
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.map f).app X ≫ (t.eTruncLTι j).app X = (t.eTruncLTι i).app X
have simp : (t.eTruncLT.map (f ≫ homOfLE sorry)).app X = (t.eTruncLTι i).app X
Tactic: simp only [← NatTrans.comp_app, ← Functor.map_comp]
-- 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
i : EInt
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)
have bot : (t.eTruncLT.obj ⊥).map (NatTrans.app (t.eTruncLTι ⊥) X) = NatTrans.app (t.eTruncLTι ⊥) ((t.eTruncLT.obj ⊥).obj X)
Tactic: induction i using WithBotTop.rec with simp [truncLT_map_truncLTι_app]
Cleared hypotheses: i
-- 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
i : EInt
X : C
bot : (t.eTruncLT.obj ⊥).map (NatTrans.app (t.eTruncLTι ⊥) X) = NatTrans.app (t.eTruncLTι ⊥) ((t.eTruncLT.obj ⊥).obj X)
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)
have coe : ∀ (a : ℤ),
  (t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) X) =
    NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) ((t.eTruncLT.obj (WithBotTop.coe a)).obj X)
Tactic: induction i using WithBotTop.rec with simp [truncLT_map_truncLTι_app]
Cleared hypotheses: i
-- 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
i : EInt
X : C
bot : (t.eTruncLT.obj ⊥).map (NatTrans.app (t.eTruncLTι ⊥) X) = NatTrans.app (t.eTruncLTι ⊥) ((t.eTruncLT.obj ⊥).obj X)
coe :
  ∀ (a : ℤ),
    (t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) X) =
      NatTrans.app (t.eTruncLTι (WithBotTop.coe a)) ((t.eTruncLT.obj (WithBotTop.coe a)).obj X)
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι i).app X) = (t.eTruncLTι i).app ((t.eTruncLT.obj i).obj X)
have top : Eq (α :=
  (t.eTruncLT.obj ⊤).obj ((t.eTruncLT.obj ⊤).obj X) ⟶ (t.eTruncLT.obj ⊤).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))
  ((t.eTruncLT.obj ⊤).map (NatTrans.app (t.eTruncLTι ⊤) X)) (NatTrans.app (t.eTruncLTι ⊤) ((t.eTruncLT.obj ⊤).obj X))
Tactic: induction i using WithBotTop.rec with simp [truncLT_map_truncLTι_app]
Cleared hypotheses: i
-- 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
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncGEπ i).app X ≫ (t.eTruncGE.map f).app X = (t.eTruncGEπ j).app X
have simp : (t.eTruncGE.map (homOfLE sorry ≫ f)).app X = (t.eTruncGEπ j).app X
Tactic: simp only [← NatTrans.comp_app, ← Functor.map_comp]
-- 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
i : EInt
X : C
⊢ (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)
have bot : Eq (α :=
  (t.eTruncGE.obj ⊥).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶ (t.eTruncGE.obj ⊥).obj ((t.eTruncGE.obj ⊥).obj X))
  ((t.eTruncGE.obj ⊥).map (NatTrans.app (t.eTruncGEπ ⊥) X)) (NatTrans.app (t.eTruncGEπ ⊥) ((t.eTruncGE.obj ⊥).obj X))
Tactic: induction i using WithBotTop.rec with simp [truncGE_map_truncGEπ_app]
Cleared hypotheses: i
-- 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
i : EInt
X : C
bot :
  Eq (α :=
    (t.eTruncGE.obj ⊥).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (t.eTruncGE.obj ⊥).obj ((t.eTruncGE.obj ⊥).obj X))
    ((t.eTruncGE.obj ⊥).map (NatTrans.app (t.eTruncGEπ ⊥) X)) (NatTrans.app (t.eTruncGEπ ⊥) ((t.eTruncGE.obj ⊥).obj X))
⊢ (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)
have coe : ∀ (a : ℤ),
  (t.eTruncGE.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) X) =
    NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) ((t.eTruncGE.obj (WithBotTop.coe a)).obj X)
Tactic: induction i using WithBotTop.rec with simp [truncGE_map_truncGEπ_app]
Cleared hypotheses: i
-- 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
i : EInt
X : C
bot :
  Eq (α :=
    (t.eTruncGE.obj ⊥).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X) ⟶
      (t.eTruncGE.obj ⊥).obj ((t.eTruncGE.obj ⊥).obj X))
    ((t.eTruncGE.obj ⊥).map (NatTrans.app (t.eTruncGEπ ⊥) X)) (NatTrans.app (t.eTruncGEπ ⊥) ((t.eTruncGE.obj ⊥).obj X))
coe :
  ∀ (a : ℤ),
    (t.eTruncGE.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) X) =
      NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) ((t.eTruncGE.obj (WithBotTop.coe a)).obj X)
⊢ (t.eTruncGE.obj i).map ((t.eTruncGEπ i).app X) = (t.eTruncGEπ i).app ((t.eTruncGE.obj i).obj X)
have top : (t.eTruncGE.obj ⊤).map (NatTrans.app (t.eTruncGEπ ⊤) X) = NatTrans.app (t.eTruncGEπ ⊤) ((t.eTruncGE.obj ⊤).obj X)
Tactic: induction i using WithBotTop.rec with simp [truncGE_map_truncGEπ_app]
Cleared hypotheses: i
-- 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
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι j).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)
have dsimp : (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE sorry)).app X) ≫ (t.eTruncLT.map f).app X =
  (t.eTruncLT.map (homOfLE sorry)).app ((t.eTruncLT.obj j).obj X)
Tactic: dsimp [eTruncLTι]
-- 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
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (homOfLE ⋯)).app ((t.eTruncLT.obj j).obj X)
have rw : (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE sorry)).app X) ≫ (t.eTruncLT.map f).app X =
  NatTrans.app (t.eTruncLT.map (f ≫ homOfLE sorry)) ((t.eTruncLT.obj j).obj X)
Tactic: rw [show homOfLE le_top = f ≫ homOfLE le_top by rfl]
-- 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
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj j).obj X)
have bot : ∀ (f : i ⟶ ⊥),
  Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊥).obj X) ⟶ (t.eTruncLT.obj ⊥).obj X)
    ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE sorry)) X) ≫ (t.eTruncLT.map f).app X)
    (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE sorry)) ((t.eTruncLT.obj ⊥).obj X))
Tactic: induction j using WithBotTop.rec with simp [truncLT_map_truncLTι_app]
Cleared hypotheses: j, f
-- 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
i j : EInt
f : i ⟶ j
X : C
bot :
  ∀ (f : i ⟶ ⊥),
    Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊥).obj X) ⟶ (t.eTruncLT.obj ⊥).obj X)
      ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
      (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj ⊥).obj X))
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj j).obj X)
have coe : ∀ (a : ℤ) (f : i ⟶ WithBotTop.coe a),
  Eq (α :=
    (t.eTruncLT.obj i).obj ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) ⟶ (t.eTruncLT.obj (WithBotTop.coe a)).obj X)
    ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE sorry)) X) ≫ (t.eTruncLT.map f).app X)
    (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE sorry)) ((t.eTruncLT.obj (WithBotTop.coe a)).obj X))
Tactic: induction j using WithBotTop.rec with simp [truncLT_map_truncLTι_app]
Cleared hypotheses: j, f