awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C 0) T).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₁)) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorZero C ℤ) T.obj₃) ≫ (Functor.obj (𝟭 (Triangle.{v, u} C)) T).mor₃
have dsimp : HSMul.hSMul (α := ℤˣ) (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₁))
      1
      (Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorComm C 1 0)) T.obj₁ :
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (A := ℤ) 0) T.obj₁)) ≫
    Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
      (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorZero C ℤ)) T.obj₁) =
  NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorZero C ℤ)) T.obj₃ ≫ T.mor₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b n : ℤ
h : a + b = n
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C n) T).mor₁ ≫ Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₂) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₁) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₁
have subst : (Functor.obj (shiftFunctor C (a + b)) T).mor₁ ≫
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry) T.obj₂) =
  Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry) T.obj₁) ≫
    (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₁
Tactic: subst h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C (a + b)) T).mor₁ ≫
      Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₂) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₁) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₁
have dsimp : HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂)
      (a + b).negOnePow (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₁) ≫
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₂ =
  NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₁ ≫
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂))
      b.negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C b)
        (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)
          a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₁)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
⊢ HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂)
        (a + b).negOnePow (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₁) ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₁ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂))
        b.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C b)
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)
            a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₁)))
have rw : HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂))
    (a + b).negOnePow
    (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₁ ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₂) =
  NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₁ ≫
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂))
      b.negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C b)
        (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)
          a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₁)))
Tactic: rw [Linear.units_smul_comp, NatTrans.naturality, Linear.comp_units_smul, Functor.comp_map,
          Functor.map_units_smul, Linear.comp_units_smul, smul_smul, Int.negOnePow_add, mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b n : ℤ
h : a + b = n
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C n) T).mor₂ ≫ Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₃) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₂) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₂
have subst : (Functor.obj (shiftFunctor C (a + b)) T).mor₂ ≫
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry) T.obj₃) =
  Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry) T.obj₂) ≫
    (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₂
Tactic: subst h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C (a + b)) T).mor₂ ≫
      Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₃) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯) T.obj₂) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₂
have dsimp : HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃)
      (a + b).negOnePow (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₂) ≫
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₃ =
  NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₂ ≫
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂) ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      b.negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C b)
        (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)
          a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b : ℤ
T : Triangle.{v, u} C
⊢ HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₃)
        (a + b).negOnePow (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₂) ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₃ =
    NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯)) T.obj₂ ≫
      HSMul.hSMul (β :=
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂) ⟶
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
            (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
        b.negOnePow
        (Functor.map (CategoryTheory.shiftFunctor C b)
          (HSMul.hSMul (β :=
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂ ⟶
              Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)
            a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)))
have rw : HSMul.hSMul (β :=
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b)) T.obj₂ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
    (a + b).negOnePow
    (Functor.map (CategoryTheory.shiftFunctor C (a + b)) T.mor₂ ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₃) =
  NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₂ ≫
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂) ⟶
        Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃))
      b.negOnePow
      (Functor.map (CategoryTheory.shiftFunctor C b)
        (HSMul.hSMul (β :=
          Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂ ⟶
            Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₃)
          a.negOnePow (Functor.map (CategoryTheory.shiftFunctor C a) T.mor₂)))
Tactic: rw [Linear.units_smul_comp, NatTrans.naturality, Linear.comp_units_smul, Functor.comp_map,
          Functor.map_units_smul, Linear.comp_units_smul, smul_smul, Int.negOnePow_add, mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b n : ℤ
h : a + b = n
T : Triangle.{v, u} C
⊢ (Functor.obj (shiftFunctor C n) T).mor₃ ≫
      Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₁)) =
    Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b n h) T.obj₃) ≫
      (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₃
have subst : (Functor.obj (shiftFunctor C (a + b)) T).mor₃ ≫
    Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1)
      (Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry) T.obj₁)) =
  Iso.hom (Iso.app (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry) T.obj₃) ≫
    (Functor.obj (shiftFunctor C a ⋙ shiftFunctor C b) T).mor₃
Tactic: subst h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
T : Triangle.{v, u} C
⊢ (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₁)) =
    Iso.hom (Iso.refl (Functor.obj (invRotate C ⋙ invRotate C ⋙ invRotate C) T).obj₃) ≫
      (Functor.obj (Triangle.shiftFunctor C (-1)) T).mor₃
have dsimp : ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C 1 (-1) 0 sorry)) T.obj₁ ≫
            NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) T.obj₁) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) T.obj₁ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C (-1) 1 0 sorry)) T.obj₁) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁)) =
  𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃) ≫
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁))
      (Int.negOnePow (-1))
      (Functor.map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorComm C 1 (-1))) T.obj₁ :
        Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₃ ⟶
          Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
            (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T.obj₁))
Tactic: dsimp [shiftFunctorCompIsoId]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
      Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T) =
    eqToHom ⋯ ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)
have h₁ : TriangleMorphism.hom₁
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) sorry)) T ≫
      Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) sorry)) T)) =
  (eqToHom sorry ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) sorry)) T ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) sorry)) (Functor.obj (shiftFunctor C a) T)).hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
h₁ :
  TriangleMorphism.hom₁
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₁
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
      Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T) =
    eqToHom ⋯ ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)
have h₂ : TriangleMorphism.hom₂
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) sorry)) T ≫
      Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) sorry)) T)) =
  (eqToHom sorry ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) sorry)) T ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) sorry)) (Functor.obj (shiftFunctor C a) T)).hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
h₁ :
  TriangleMorphism.hom₁
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₁
h₂ :
  TriangleMorphism.hom₂
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₂
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
      Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T) =
    eqToHom ⋯ ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)
have h₃ : TriangleMorphism.hom₃
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) sorry)) T ≫
      Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) sorry)) T)) =
  (eqToHom sorry ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) sorry)) T ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) sorry)) (Functor.obj (shiftFunctor C a) T)).hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
⊢ TriangleMorphism.hom₁
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₁
have h₁ : Eq.{v + 1} (α :=
  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
      (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
  (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) sorry)) T.obj₁ ≫
      Functor.map (CategoryTheory.shiftFunctor C c)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₁) :
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
  (TriangleMorphism.hom₁ (eqToHom sorry) ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a (b + c) (a + (b + c)) sorry)) T.obj₁ ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C b c (b + c) sorry))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁) :
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₁ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₁)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TriangleShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (CategoryTheory.shiftFunctor C n)
a b c : ℤ
T : Triangle.{v, u} C
⊢ TriangleMorphism.hom₂
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯)) T ≫
        Functor.map (shiftFunctor C c) (NatTrans.app (Iso.hom (shiftFunctorAdd' C a b (a + b) ⋯)) T)) =
    (eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯)) T ≫
          NatTrans.app (Iso.hom (shiftFunctorAdd' C b c (b + c) ⋯)) (Functor.obj (shiftFunctor C a) T)).hom₂
have h₂ : Eq.{v + 1} (α :=
  Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
      (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
  (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C (a + b) c (a + b + c) sorry)) T.obj₂ ≫
      Functor.map (CategoryTheory.shiftFunctor C c)
        (NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a b (a + b) sorry)) T.obj₂) :
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
  (TriangleMorphism.hom₂ (eqToHom sorry) ≫
      NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C a (b + c) (a + (b + c)) sorry)) T.obj₂ ≫
        NatTrans.app (Iso.hom (CategoryTheory.shiftFunctorAdd' C b c (b + c) sorry))
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂) :
    Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C (a + b + c)) T.obj₂ ⟶
      Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C c)
        (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C b)
          (Functor.obj.{v, v, u, u} (CategoryTheory.shiftFunctor C a) T.obj₂)))
Tactic: dsimp