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
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')
⊢ 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]
-- 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 m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
have zero : P.extensionProductIter (0 + m) = (P.extensionProductIter 0).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]
Cleared hypotheses: n
-- 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 m' : ℕ
h : m = m' + 1
zero : P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
⊢ P.extensionProductIter (n + m) = (P.extensionProductIter n).extensionProduct (P.extensionProductIter m')
have 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')
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]
Cleared hypotheses: n
-- 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 Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
n : ℕ
h : P.extensionProductIter n ≤ Q.extensionProductIter n
⊢ P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)
have succ : P.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProductIter (n + 1)
Tactic: grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]
-- 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 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)
⊢ P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)
have succ₁ : P.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
Tactic: grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]
-- 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 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)
⊢ P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)
have succ₂ : Q.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
Tactic: grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]
-- 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 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)
⊢ P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)
have succ₃ : Q.extensionProduct (Q.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
Tactic: grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]
-- 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 Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
n : ℕ
⊢ P.extensionProductIter n ≤ Q.extensionProductIter n
have zero : P.extensionProductIter 0 ≤ Q.extensionProductIter 0
Tactic: induction n with
  | zero => exact hPQ
  | succ n h => grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]
Cleared hypotheses: n
-- 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 Q : ObjectProperty.{v_1, u_1} C
hPQ : P ≤ Q
n : ℕ
zero : P.extensionProductIter 0 ≤ Q.extensionProductIter 0
⊢ P.extensionProductIter n ≤ Q.extensionProductIter n
have succ : ∀ (n : ℕ) (h : P.extensionProductIter n ≤ Q.extensionProductIter n),
  P.extensionProductIter (n + 1) ≤ Q.extensionProductIter (n + 1)
Tactic: induction n with
  | zero => exact hPQ
  | succ n h => grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]
Cleared hypotheses: n
-- 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 : P.ContainsZero
n m : ℕ
h : n ≤ m
⊢ P.extensionProductIter n ≤ P.extensionProductIter m
have induction : P.extensionProductIter n ≤ P.extensionProductIter n
Tactic: induction m, h using Nat.le_induction
Cleared hypotheses: h
-- 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 : P.ContainsZero
n m : ℕ
h : n ≤ m
induction : P.extensionProductIter n ≤ P.extensionProductIter n
⊢ P.extensionProductIter n ≤ P.extensionProductIter m
have succ : ∀ (n_1 : ℕ),
  n ≤ n_1 →
    P.extensionProductIter n ≤ P.extensionProductIter n_1 → P.extensionProductIter n ≤ P.extensionProductIter (n_1 + 1)
Tactic: induction m, h using Nat.le_induction
Cleared hypotheses: h
-- 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
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)
have refine : P.extensionProductIter m ≤ P.extensionProductIter (m + 1)
Tactic: refine le_trans h ?_
-- 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
n_1 : P.ContainsZero
n m_1 m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter m ≤ P.extensionProductIter (m + 1)
have rw : P.extensionProductIter m ≤ P.extensionProduct (P.extensionProductIter m)
Tactic: rw [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
n : ℕ
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ n) ⊥
have cases : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ 0) ⊥
Tactic: cases n
Cleared hypotheses: n
-- 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
n : ℕ
cases : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ 0) ⊥
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ n) ⊥
have succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ (n + 1)) ⊥
Tactic: cases n
Cleared hypotheses: n
-- 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
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ 0) ⊥
have rw : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
Tactic: rw [extensionProductIter_zero]
-- 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
n : ℕ
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ (n + 1)) ⊥
have rw : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProduct ⊥ (extensionProductIter ⊥ n)) ⊥
Tactic: rw [extensionProductIter_succ, extensionProduct_bot_left]
-- 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
n : ℕ
rw : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProduct ⊥ (extensionProductIter ⊥ n)) ⊥
⊢ Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) (extensionProductIter ⊥ (n + 1)) ⊥
have rw₁ : Eq.{u_1 + 1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
Tactic: rw [extensionProductIter_succ, extensionProduct_bot_left]
-- 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
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.extensionProductIter (n + 1)).IsStableUnderShift ℤ
have succ : (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ
Tactic: rw [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
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 : ℕ
⊢ (P.extensionProductIter n).IsStableUnderShift ℤ
have zero : (P.extensionProductIter 0).IsStableUnderShift ℤ
Tactic: induction n with
  | zero => assumption
  | succ n h =>
    rw [extensionProductIter_succ]
    infer_instance
Cleared hypotheses: n
-- 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
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 ℤ
⊢ (P.extensionProductIter n).IsStableUnderShift ℤ
have succ : ∀ (n : ℕ) (h : (P.extensionProductIter n).IsStableUnderShift ℤ), (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ
Tactic: induction n with
  | zero => assumption
  | succ n h =>
    rw [extensionProductIter_succ]
    infer_instance
Cleared hypotheses: n
-- 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 Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
⊢ P.extensionProductIter 0 ≤ Q.isoClosure
have zero : P ≤ Q.isoClosure
Tactic: rw [extensionProductIter_zero]
-- 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 Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
H : P.extensionProductIter n ≤ Q.isoClosure
⊢ P.extensionProductIter (n + 1) ≤ Q.isoClosure
have succ : P.extensionProduct (P.extensionProductIter n) ≤ Q.isoClosure
Tactic: rw [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 Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
⊢ P.extensionProductIter n ≤ Q.isoClosure
have zero : P.extensionProductIter 0 ≤ 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
Cleared hypotheses: n
-- 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 Q : ObjectProperty.{v_1, u_1} C
inst_6 : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
zero : P.extensionProductIter 0 ≤ Q.isoClosure
⊢ P.extensionProductIter n ≤ Q.isoClosure
have succ : ∀ (n : ℕ) (H : P.extensionProductIter n ≤ Q.isoClosure), P.extensionProductIter (n + 1) ≤ 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
Cleared hypotheses: n
-- 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
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.extensionProductIter (n + 1)).IsStableUnderShift ℤ
have succ : (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ
Tactic: rw [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
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 : ℕ
⊢ (P.extensionProductIter n).IsStableUnderShift ℤ
have zero : (P.extensionProductIter 0).IsStableUnderShift ℤ
Tactic: induction n with
  | zero => rwa [extensionProductIter_zero]
  | succ n H => rw [extensionProductIter_succ]; infer_instance
Cleared hypotheses: n
-- 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
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 ℤ
⊢ (P.extensionProductIter n).IsStableUnderShift ℤ
have succ : ∀ (n : ℕ) (H : (P.extensionProductIter n).IsStableUnderShift ℤ), (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ
Tactic: induction n with
  | zero => rwa [extensionProductIter_zero]
  | succ n H => rw [extensionProductIter_succ]; infer_instance
Cleared hypotheses: n