awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) A
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f₁ f₂ f₃)
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁))
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
φ : Triangle.mk f₁ f₂ f₃ ⟶ Triangle.mk f₁ f₂ f₃ :=
  (Triangle.mk f₁ f₂ f₃).homMk (Triangle.mk f₁ f₂ f₃) (𝟙 A) (a₂ ≫ b₂) (𝟙 B) ⋯ ⋯ ⋯
this : IsIso (a₂ ≫ b₂)
⊢ Retract X X'

Tactic:
exact ⟨a₂, b₂ ≫ inv (a₂ ≫ b₂), by grind⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
a : (P.retractClosure.extensionProduct Q.retractClosure).retractClosure ≤ (P.extensionProduct Q).retractClosure
a₁ : (P.extensionProduct Q).retractClosure ≤ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure
⊢ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure = (P.extensionProduct Q).retractClosure

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
a : P.retractClosure.extensionProduct Q.retractClosure ≤ (P.extensionProduct Q).retractClosure
⊢ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure ≤ (P.extensionProduct Q).retractClosure

Tactic:
rw [retractClosure_le_iff]

Premises used: CategoryTheory.ObjectProperty.retractClosure_le_iff
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
⊢ P.retractClosure.extensionProduct Q.retractClosure ≤ (P.extensionProduct Q).retractClosure

Tactic:
extensionProduct_retractClosure_retractClosure_le P Q

Premises used: CategoryTheory.ObjectProperty.extensionProduct_retractClosure_retractClosure_le
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
⊢ P.retractClosure.extensionProduct Q.retractClosure ≤ (P.extensionProduct Q).retractClosure

Tactic:
exact extensionProduct_retractClosure_retractClosure_le P Q

Premises used: CategoryTheory.ObjectProperty.extensionProduct_retractClosure_retractClosure_le
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
a : P.extensionProduct Q ≤ P.retractClosure.extensionProduct Q.retractClosure
⊢ (P.extensionProduct Q).retractClosure ≤ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure

Tactic:
apply monotone_retractClosure

Premises used: CategoryTheory.ObjectProperty.monotone_retractClosure
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
a : P.extensionProduct Q.retractClosure ≤ P.retractClosure.extensionProduct Q.retractClosure
a₁ a₂ : P.retractClosure.extensionProduct Q.retractClosure ≤ P.retractClosure.extensionProduct Q.retractClosure
⊢ P.extensionProduct Q ≤ P.retractClosure.extensionProduct Q.retractClosure

Tactic:
grw [monotone_extensionProduct_right _ (le_retractClosure Q),
      monotone_extensionProduct_left _ (le_retractClosure P)]

Premises used: CategoryTheory.ObjectProperty.monotone_extensionProduct_right, CategoryTheory.ObjectProperty.monotone_extensionProduct_left, CategoryTheory.ObjectProperty.le_retractClosure
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
⊢ P.extensionProductIter 0 = P

Tactic:
rfl

Premises used: CategoryTheory.ObjectProperty.extensionProductIter, Nat.iterate, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
n : ℕ
⊢ P.extensionProductIter (n + 1) = P.extensionProduct (P.extensionProductIter n)

Tactic:
Function.iterate_succ_apply' _ _ _

Premises used: Function.iterate_succ_apply', CategoryTheory.ObjectProperty.extensionProductIter
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
⊢ P.extensionProductIter (HAdd.hAdd (α := ℕ) 0 1) = (P.extensionProductIter 0).extensionProduct P

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 : ℕ
h : P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P
succ : P.extensionProduct (P.extensionProductIter (n + 1)) = (P.extensionProductIter (n + 1)).extensionProduct P
succ₁ :
  P.extensionProduct ((P.extensionProductIter n).extensionProduct P) =
    ((P.extensionProductIter n).extensionProduct P).extensionProduct P
succ₂ :
  (P.extensionProduct (P.extensionProductIter n)).extensionProduct P =
    ((P.extensionProductIter n).extensionProduct P).extensionProduct P
succ₃ :
  (P.extensionProductIter (n + 1)).extensionProduct P =
    ((P.extensionProductIter n).extensionProduct P).extensionProduct P
succ₄ succ₅ : (P.extensionProductIter (n + 1)).extensionProduct P = (P.extensionProductIter (n + 1)).extensionProduct P
⊢ P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P

Tactic:
rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← h]

Premises used: CategoryTheory.ObjectProperty.extensionProduct_assoc, CategoryTheory.ObjectProperty.extensionProductIter_succ
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 : ℕ
zero : P.extensionProductIter (HAdd.hAdd (α := ℕ) 0 1) = (P.extensionProductIter 0).extensionProduct P
succ :
  ∀ (n : ℕ) (h : P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P),
    P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P
⊢ P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P

Tactic:
induction n with
  | zero => rfl
  | succ n h =>
    rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← h]

Premises used: CategoryTheory.ObjectProperty.extensionProduct_assoc, CategoryTheory.ObjectProperty.extensionProductIter_succ
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P Q R : ObjectProperty.{v_1, u_1} C
inst_14 zero zero₁ zero₂ zero₃ : P.Nonempty
⊢ (P.extensionProductIter 0).Nonempty

Tactic:
rwa [extensionProductIter_zero]

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P Q R : ObjectProperty.{v_1, u_1} C
inst_14 : P.Nonempty
n : ℕ
h : (P.extensionProductIter n).Nonempty
succ : (P.extensionProduct (P.extensionProductIter n)).Nonempty
⊢ (P.extensionProductIter (n + 1)).Nonempty

Tactic:
rw [extensionProductIter_succ]

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_succ
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P Q R : ObjectProperty.{v_1, u_1} C
inst_14 : P.Nonempty
n : ℕ
h : (P.extensionProductIter n).Nonempty
⊢ (P.extensionProduct (P.extensionProductIter n)).Nonempty

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P Q R : ObjectProperty.{v_1, u_1} C
inst_14 : P.Nonempty
n : ℕ
zero : (P.extensionProductIter 0).Nonempty
succ : ∀ (n : ℕ) (h : (P.extensionProductIter n).Nonempty), (P.extensionProductIter (n + 1)).Nonempty
⊢ (P.extensionProductIter n).Nonempty

Tactic:
induction n with
  | zero => rwa [extensionProductIter_zero]
  | succ n h => rw [extensionProductIter_succ]; infer_instance

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_succ, CategoryTheory.ObjectProperty.extensionProductIter_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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
zero₃ zero₄ : (P.extensionProductIter n').extensionProduct P = (P.extensionProductIter n').extensionProduct P
⊢ P.extensionProductIter (n + 0) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)

Tactic:
rw [add_zero, extensionProductIter_zero, h, extensionProductIter_succ']

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_succ', add_zero, CategoryTheory.ObjectProperty.extensionProductIter_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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)
succ₄ 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))

Tactic:
rw [← add_assoc, extensionProductIter_succ', extensionProductIter_succ', hm,
      extensionProduct_assoc]

Premises used: add_assoc, CategoryTheory.ObjectProperty.extensionProduct_assoc, CategoryTheory.ObjectProperty.extensionProductIter_succ'
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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)
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))
⊢ P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)

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]

Premises used: add_assoc, CategoryTheory.ObjectProperty.extensionProduct_assoc, CategoryTheory.ObjectProperty.extensionProductIter_succ', add_zero, CategoryTheory.ObjectProperty.extensionProductIter_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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')
zero₃ zero₄ : P.extensionProduct (P.extensionProductIter m') = P.extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')

Tactic:
rw [zero_add, extensionProductIter_zero, h, extensionProductIter_succ]

Premises used: zero_add, CategoryTheory.ObjectProperty.extensionProductIter_succ, CategoryTheory.ObjectProperty.extensionProductIter_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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')
succ₅ :
  P.extensionProduct ((P.extensionProductIter n).extensionProduct (P.extensionProductIter m')) =
    (P.extensionProduct (P.extensionProductIter n)).extensionProduct (P.extensionProductIter m')
succ₆ succ₇ :
  P.extensionProduct ((P.extensionProductIter n).extensionProduct (P.extensionProductIter m')) =
    P.extensionProduct ((P.extensionProductIter n).extensionProduct (P.extensionProductIter m'))
⊢ 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]

Premises used: add_assoc, CategoryTheory.ObjectProperty.extensionProduct_assoc, add_comm, CategoryTheory.ObjectProperty.extensionProductIter_succ, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 m' : ℕ
h : m = m' + 1
zero : P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
succ :
  ∀ (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')
⊢ P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')

Tactic:
induction n with
  | zero => rw [zero_add, extensionProductIter_zero, h, extensionProductIter_succ]
  | succ n hn => rw [add_assoc, add_comm 1 m, ← add_assoc, extensionProductIter_succ,
    extensionProductIter_succ, hn, extensionProduct_assoc]

Premises used: add_assoc, CategoryTheory.ObjectProperty.extensionProduct_assoc, zero_add, add_comm, CategoryTheory.ObjectProperty.extensionProductIter_succ, OfNat.ofNat, CategoryTheory.ObjectProperty.extensionProductIter_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
⊢ P.extensionProductIter 0 ≤ Q.extensionProductIter 0

Tactic:
hPQ

Premises used: CategoryTheory.ObjectProperty.extensionProductIter, Nat.iterate
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
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 Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
⊢ P.extensionProductIter 0 ≤ Q.extensionProductIter 0

Tactic:
exact hPQ