awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
⊢ P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
have zero : P.extensionProductIter n = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
Tactic: rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
zero : P.extensionProductIter n = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
⊢ P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
have zero₁ : P.extensionProductIter n = (P.extensionProductIter n').extensionProduct P
Tactic: rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
zero : P.extensionProductIter n = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
zero₁ : P.extensionProductIter n = (P.extensionProductIter n').extensionProduct P
⊢ P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
have zero₂ : P.extensionProductIter (n' + 1) = (P.extensionProductIter n').extensionProduct P
Tactic: rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
zero : P.extensionProductIter n = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
zero₁ : P.extensionProductIter n = (P.extensionProductIter n').extensionProduct P
zero₂ : P.extensionProductIter (n' + 1) = (P.extensionProductIter n').extensionProduct P
⊢ P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
have zero₃ : (P.extensionProductIter n').extensionProduct P = (P.extensionProductIter n').extensionProduct P
Tactic: rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
⊢ P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
have succ : P.extensionProductIter (n + m + 1) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
Tactic: rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
succ :
  P.extensionProductIter (n + m + 1) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
⊢ P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
have succ₁ : (P.extensionProductIter (n + m)).extensionProduct P =
  (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
Tactic: rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
succ :
  P.extensionProductIter (n + m + 1) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
succ₁ :
  (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
⊢ P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
have succ₂ : (P.extensionProductIter (n + m)).extensionProduct P =
  (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P)
Tactic: rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
succ :
  P.extensionProductIter (n + m + 1) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
succ₁ :
  (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
succ₂ :
  (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P)
⊢ P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
have succ₃ : ((P.extensionProductIter n').extensionProduct (P.extensionProductIter m)).extensionProduct P =
  (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P)
Tactic: rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
succ :
  P.extensionProductIter (n + m + 1) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
succ₁ :
  (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
succ₂ :
  (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P)
succ₃ :
  ((P.extensionProductIter n').extensionProduct (P.extensionProductIter m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P)
⊢ P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
have succ₄ : (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P) =
  (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P)
Tactic: rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n m n' : ℕ
h : n = n' + 1
⊢ P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
have zero : P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
Tactic: induction m with
  | zero => rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']
  | succ m hm =>
    rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
n m n' : ℕ
h : n = n' + 1
zero : P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)
⊢ P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
have succ : ∀ (m : ℕ)
  (hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)),
  P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
Tactic: induction m with
  | zero => rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']
  | succ m hm =>
    rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
have zero : P.extensionProductIter m = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
Tactic: rw [zero_add, extensionProductIter_zero, h, extensionProductIter_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
zero : P.extensionProductIter m = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
have zero₁ : P.extensionProductIter m = P.extensionProduct (P.extensionProductIter m')
Tactic: rw [zero_add, extensionProductIter_zero, h, extensionProductIter_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
zero : P.extensionProductIter m = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
zero₁ : P.extensionProductIter m = P.extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
have zero₂ : P.extensionProductIter (m' + 1) = P.extensionProduct (P.extensionProductIter m')
Tactic: rw [zero_add, extensionProductIter_zero, h, extensionProductIter_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
zero : P.extensionProductIter m = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
zero₁ : P.extensionProductIter m = P.extensionProduct (P.extensionProductIter m')
zero₂ : P.extensionProductIter (m' + 1) = P.extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
have zero₃ : P.extensionProduct (P.extensionProductIter m') = P.extensionProduct (P.extensionProductIter m')
Tactic: rw [zero_add, extensionProductIter_zero, h, extensionProductIter_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + 1 + m) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
have succ : P.extensionProductIter (n + (1 + m)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
Tactic: rw [add_assoc, add_comm 1 m, ← add_assoc, extensionProductIter_succ,
    extensionProductIter_succ, hn, extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
succ :
  P.extensionProductIter (n + (1 + m)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + 1 + m) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
have succ₁ : P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
Tactic: rw [add_assoc, add_comm 1 m, ← add_assoc, extensionProductIter_succ,
    extensionProductIter_succ, hn, extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
succ :
  P.extensionProductIter (n + (1 + m)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₁ :
  P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + 1 + m) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
have succ₂ : P.extensionProductIter (n + m + 1) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
Tactic: rw [add_assoc, add_comm 1 m, ← add_assoc, extensionProductIter_succ,
    extensionProductIter_succ, hn, extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
succ :
  P.extensionProductIter (n + (1 + m)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₁ :
  P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₂ :
  P.extensionProductIter (n + m + 1) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + 1 + m) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
have succ₃ : P.extensionProduct (P.extensionProductIter (n + m)) =
  (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
Tactic: rw [add_assoc, add_comm 1 m, ← add_assoc, extensionProductIter_succ,
    extensionProductIter_succ, hn, extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
succ :
  P.extensionProductIter (n + (1 + m)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₁ :
  P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₂ :
  P.extensionProductIter (n + m + 1) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₃ :
  P.extensionProduct (P.extensionProductIter (n + m)) =
    (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + 1 + m) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
have succ₄ : P.extensionProduct (P.extensionProductIter (n + m)) =
  (P.extensionProduct (P.extensionProductIter n)).extensionProduct (P.extensionProductIter m')
Tactic: rw [add_assoc, add_comm 1 m, ← add_assoc, extensionProductIter_succ,
    extensionProductIter_succ, hn, extensionProduct_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
m m' : ℕ
h : m = m' + 1
n : ℕ
hn : P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
succ :
  P.extensionProductIter (n + (1 + m)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₁ :
  P.extensionProductIter (n + (m + 1)) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₂ :
  P.extensionProductIter (n + m + 1) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₃ :
  P.extensionProduct (P.extensionProductIter (n + m)) =
    (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
succ₄ :
  P.extensionProduct (P.extensionProductIter (n + m)) =
    (P.extensionProduct (P.extensionProductIter n)).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + 1 + m) = (P.extensionProductIter (n + 1)).extensionProduct (P.extensionProductIter m')
have succ₅ : P.extensionProduct ((P.extensionProductIter n).extensionProduct (P.extensionProductIter m')) =
  (P.extensionProduct (P.extensionProductIter n)).extensionProduct (P.extensionProductIter m')
Tactic: rw [add_assoc, add_comm 1 m, ← add_assoc, extensionProductIter_succ,
    extensionProductIter_succ, hn, extensionProduct_assoc]