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
hPQ : P ≤ Q
n : ℕ
h : P.extensionProductIter n ≤ Q.extensionProductIter n
succ : P.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProductIter (n + 1)
succ₁ : P.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
succ₂ : Q.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
succ₃ succ₄ : Q.extensionProduct (Q.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
⊢ P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)

Tactic:
grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]

Premises used: CategoryTheory.ObjectProperty.monotone_extensionProduct_right, CategoryTheory.ObjectProperty.monotone_extensionProduct_left, 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 Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
n : ℕ
zero : P.extensionProductIter 0 ≤ Q.extensionProductIter 0
succ :
  ∀ (n : ℕ) (h : P.extensionProductIter n ≤ Q.extensionProductIter n),
    P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)
⊢ P.extensionProductIter n ≤ Q.extensionProductIter n

Tactic:
induction n with
  | zero => exact hPQ
  | succ n h => grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]

Premises used: CategoryTheory.ObjectProperty.monotone_extensionProduct_left, 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 : P.ContainsZero
n m : ℕ
h : n ≤ m
induction : P.extensionProductIter n ≤ P.extensionProductIter n
succ :
  ∀ (n_1 : ℕ),
    n ≤ n_1 →
      P.extensionProductIter n ≤ P.extensionProductIter n_1 →
        P.extensionProductIter n ≤ P.extensionProductIter (n_1 + 1)
⊢ P.extensionProductIter n ≤ P.extensionProductIter m

Tactic:
induction m, h using Nat.le_induction
-- 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 : P.ContainsZero
n m : ℕ
⊢ P.extensionProductIter n ≤ P.extensionProductIter n

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 : P.ContainsZero
n m : ℕ
⊢ P.extensionProductIter n ≤ P.extensionProductIter n

Tactic:
case base => 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_1 : P.ContainsZero
n m_1 m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter n ≤ P.extensionProductIter (m + 1)

Tactic:
le_trans h ?_

Premises used: le_trans
-- 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_1 : P.ContainsZero
n m_1 m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
refine : P.extensionProductIter m ≤ P.extensionProductIter (m + 1)
⊢ P.extensionProductIter n ≤ P.extensionProductIter (m + 1)

Tactic:
refine le_trans h ?_

Premises used: le_trans
-- 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_1 : P.ContainsZero
n m_1 m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
rw : P.extensionProductIter m ≤ P.extensionProduct (P.extensionProductIter m)
⊢ P.extensionProductIter m ≤ P.extensionProductIter (m + 1)

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
P : ObjectProperty.{v_1, u_1} C
n_1 : P.ContainsZero
n m_1 m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter m ≤ P.extensionProduct (P.extensionProductIter m)

Tactic:
le_extensionProduct_right P

Premises used: CategoryTheory.ObjectProperty.le_extensionProduct_right
-- 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_1 : P.ContainsZero
n m_1 m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter m ≤ P.extensionProduct (P.extensionProductIter m)

Tactic:
exact le_extensionProduct_right P

Premises used: CategoryTheory.ObjectProperty.le_extensionProduct_right
-- 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 : P.ContainsZero
n : ℕ
⊢ P ≤ P.extensionProductIter n

Tactic:
P.monotone'_extensionProductIter (Nat.zero_le n)

Premises used: Nat.zero_le, CategoryTheory.ObjectProperty.extensionProductIter, Nat.iterate, CategoryTheory.ObjectProperty.monotone'_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
n : ℕ
cases : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ 0) ⊥
succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ (n + 1)) ⊥
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ n) ⊥

Tactic:
cases n
-- 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
rw rw₁ : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ 0) ⊥

Tactic:
rw [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
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ 0) ⊥

Tactic:
case zero => rw [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
n : ℕ
rw : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProduct ⊥ (extensionProductIter ⊥ n)) ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ (n + 1)) ⊥

Tactic:
rw [extensionProductIter_succ, extensionProduct_bot_left]

Premises used: CategoryTheory.ObjectProperty.extensionProduct_bot_left, 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
n : ℕ
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊤ n) ⊤

Tactic:
eq_top_iff.mpr (le_extensionProductIter _ n)

Premises used: Iff.mpr, eq_top_iff, CategoryTheory.ObjectProperty.le_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
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.IsStableUnderShift ℤ
⊢ (P.extensionProductIter 0).IsStableUnderShift ℤ

Tactic:
assumption
-- 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.IsStableUnderShift ℤ
n : ℕ
h : (P.extensionProductIter n).IsStableUnderShift ℤ
succ : (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ
⊢ (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ

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.IsStableUnderShift ℤ
n : ℕ
h : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ

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.IsStableUnderShift ℤ
n : ℕ
zero : (P.extensionProductIter 0).IsStableUnderShift ℤ
succ :
  ∀ (n : ℕ) (h : (P.extensionProductIter n).IsStableUnderShift ℤ), (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ
⊢ (P.extensionProductIter n).IsStableUnderShift ℤ

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

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
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
zero : P ≤ Q.isoClosure
⊢ P.extensionProductIter 0 ≤ Q.isoClosure

Tactic:
rw [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
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P ≤ Q.isoClosure

Tactic:
h.trans Q.le_isoClosure

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, LE.le.trans
-- 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
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P ≤ Q.isoClosure

Tactic:
exact h.trans Q.le_isoClosure

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, LE.le.trans
-- 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
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
H : P.extensionProductIter n ≤ Q.isoClosure
succ : P.extensionProduct (P.extensionProductIter n) ≤ Q.isoClosure
⊢ P.extensionProductIter (n + 1) ≤ Q.isoClosure

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
P Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
H : P.extensionProductIter n ≤ Q.isoClosure
⊢ P.extensionProduct (P.extensionProductIter n) ≤ Q.isoClosure

Tactic:
extensionProduct_le_of_isTriangulatedClosed₂ (h.trans Q.le_isoClosure) H

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.extensionProduct_le_of_isTriangulatedClosed₂, LE.le.trans
-- 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
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
H : P.extensionProductIter n ≤ Q.isoClosure
⊢ P.extensionProduct (P.extensionProductIter n) ≤ Q.isoClosure

Tactic:
exact extensionProduct_le_of_isTriangulatedClosed₂ (h.trans Q.le_isoClosure) H

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.extensionProduct_le_of_isTriangulatedClosed₂, LE.le.trans
-- 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
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
zero : P.extensionProductIter 0 ≤ Q.isoClosure
succ : ∀ (n : ℕ) (H : P.extensionProductIter n ≤ Q.isoClosure), P.extensionProductIter (n + 1) ≤ Q.isoClosure
⊢ P.extensionProductIter n ≤ Q.isoClosure

Tactic:
induction n with
  | zero =>
    rw [extensionProductIter_zero]
    exact h.trans Q.le_isoClosure
  | succ n H =>
    rw [extensionProductIter_succ]
    exact extensionProduct_le_of_isTriangulatedClosed₂ (h.trans Q.le_isoClosure) H

Premises used: CategoryTheory.ObjectProperty.le_isoClosure, CategoryTheory.ObjectProperty.extensionProductIter_succ, LE.le.trans, 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
inst_6 : Q.IsTriangulatedClosed₂
inst_7 : Q.IsClosedUnderIsomorphisms
h : P ≤ Q
n : ℕ
⊢ P.extensionProductIter n ≤ Q

Tactic:
Q.isoClosure_eq_self ▸ P.extensionProductIter_le_of_isTriangulatedClosed₂' h n

Premises used: CategoryTheory.ObjectProperty.extensionProductIter_le_of_isTriangulatedClosed₂', Eq.rec, CategoryTheory.ObjectProperty.isoClosure_eq_self
-- 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.IsStableUnderShift ℤ
⊢ (P.extensionProductIter 0).IsStableUnderShift ℤ

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.IsStableUnderShift ℤ
n : ℕ
H : (P.extensionProductIter n).IsStableUnderShift ℤ
succ : (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ
⊢ (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ

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.IsStableUnderShift ℤ
n : ℕ
H : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ

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.IsStableUnderShift ℤ
n : ℕ
zero : (P.extensionProductIter 0).IsStableUnderShift ℤ
succ :
  ∀ (n : ℕ) (H : (P.extensionProductIter n).IsStableUnderShift ℤ), (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ
⊢ (P.extensionProductIter n).IsStableUnderShift ℤ

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