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 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₁))
⊢ (P.extensionProduct Q).retractClosure X
have obtain : ∀ (a₂ : X ⟶ X')
  (ha₁₂ :
    (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ =
      a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₁)
  (ha₂₃ :
    (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ =
      a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₂),
  (P.extensionProduct Q).retractClosure X
Tactic: obtain ⟨a₂ : X ⟶ X', ha₁₂, ha₂₃⟩ :=
    complete_distinguished_triangle_morphism₂ _ _ hT hT' a₁ a₃ (by dsimp; grind)
-- 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
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₁₂ :
  (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ =
    a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₁
ha₂₃ :
  (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ =
    a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₂
⊢ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) b₁ =
    b₃ ≫ (Triangle.mk f₁ f₂ f₃).mor₃
have dsimp : (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b₁ = b₃ ≫ f₃
Tactic: dsimp
-- 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
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₁₂ :
  (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ =
    a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₁
ha₂₃ :
  (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ =
    a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₂
⊢ (P.extensionProduct Q).retractClosure X
have obtain : ∀ (b₂ : X' ⟶ X)
  (hb₁₂ :
    (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₁ ≫ b₂ =
      b₁ ≫ (Triangle.mk f₁ f₂ f₃).mor₁)
  (hb₂₃ :
    (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a₁)).mor₂ ≫ b₃ =
      b₂ ≫ (Triangle.mk f₁ f₂ f₃).mor₂),
  (P.extensionProduct Q).retractClosure X
Tactic: obtain ⟨b₂ : X' ⟶ X, hb₁₂, hb₂₃⟩ :=
    complete_distinguished_triangle_morphism₂ _ _ hT' hT b₁ b₃ (by dsimp; grind)
-- 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
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₂
⊢ (P.extensionProduct Q).retractClosure X
have refine : Retract X X'
Tactic: refine ⟨X', ⟨_, _, _, _, _, hT', hP, hQ⟩, ⟨?_⟩⟩
-- 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
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₃).mor₁ ≫ a₂ ≫ b₂ = 𝟙 A ≫ (Triangle.mk f₁ f₂ f₃).mor₁
have dsimp : f₁ ≫ a₂ ≫ b₂ = 𝟙 A ≫ f₁
Tactic: dsimp
-- 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
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₃).mor₂ ≫ 𝟙 B = (a₂ ≫ b₂) ≫ (Triangle.mk f₁ f₂ f₃).mor₂
have dsimp : f₂ ≫ 𝟙 B = (a₂ ≫ b₂) ≫ f₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (hypothesis)
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) ⋯ ⋯ ⋯
⊢ Retract X X'
have this : IsIso (a₂ ≫ b₂)
Tactic: haveI : IsIso (a₂ ≫ b₂) := isIso₂_of_isIso₁₃ φ hT hT (IsIso.id _) (IsIso.id _)
-- 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
⊢ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure = (P.extensionProduct Q).retractClosure
have a : (P.retractClosure.extensionProduct Q.retractClosure).retractClosure ≤ (P.extensionProduct Q).retractClosure
Tactic: apply le_antisymm
-- 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
a : (P.retractClosure.extensionProduct Q.retractClosure).retractClosure ≤ (P.extensionProduct Q).retractClosure
⊢ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure = (P.extensionProduct Q).retractClosure
have a₁ : (P.extensionProduct Q).retractClosure ≤ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure
Tactic: apply le_antisymm
-- 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
⊢ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure ≤ (P.extensionProduct Q).retractClosure
have a : P.retractClosure.extensionProduct Q.retractClosure ≤ (P.extensionProduct Q).retractClosure
Tactic: rw [retractClosure_le_iff]
-- 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
⊢ (P.extensionProduct Q).retractClosure ≤ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure
have a : P.extensionProduct Q ≤ P.retractClosure.extensionProduct Q.retractClosure
Tactic: apply monotone_retractClosure
-- 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
⊢ P.extensionProduct Q ≤ P.retractClosure.extensionProduct Q.retractClosure
have a : P.extensionProduct Q.retractClosure ≤ P.retractClosure.extensionProduct Q.retractClosure
Tactic: grw [monotone_extensionProduct_right _ (le_retractClosure Q),
      monotone_extensionProduct_left _ (le_retractClosure P)]
-- 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
a : P.extensionProduct Q.retractClosure ≤ P.retractClosure.extensionProduct Q.retractClosure
⊢ P.extensionProduct Q ≤ P.retractClosure.extensionProduct Q.retractClosure
have a₁ : P.retractClosure.extensionProduct Q.retractClosure ≤ P.retractClosure.extensionProduct Q.retractClosure
Tactic: grw [monotone_extensionProduct_right _ (le_retractClosure Q),
      monotone_extensionProduct_left _ (le_retractClosure P)]
-- 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 : ℕ
h : P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P
⊢ P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P
have succ : P.extensionProduct (P.extensionProductIter (n + 1)) = (P.extensionProductIter (n + 1)).extensionProduct P
Tactic: rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← 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 : 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
⊢ P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P
have succ₁ : P.extensionProduct ((P.extensionProductIter n).extensionProduct P) =
  ((P.extensionProductIter n).extensionProduct P).extensionProduct P
Tactic: rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← 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 : 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
⊢ P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P
have succ₂ : (P.extensionProduct (P.extensionProductIter n)).extensionProduct P =
  ((P.extensionProductIter n).extensionProduct P).extensionProduct P
Tactic: rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← 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 : 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
⊢ P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P
have succ₃ : (P.extensionProductIter (n + 1)).extensionProduct P = ((P.extensionProductIter n).extensionProduct P).extensionProduct P
Tactic: rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← 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 : 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
⊢ P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P
have succ₄ : (P.extensionProductIter (n + 1)).extensionProduct P = (P.extensionProductIter (n + 1)).extensionProduct P
Tactic: rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← 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 : IsTriangulated.{v_1, u_1} C
n : ℕ
⊢ P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P
have zero : P.extensionProductIter (HAdd.hAdd (α := ℕ) 0 1) = (P.extensionProductIter 0).extensionProduct P
Tactic: induction n with
  | zero => rfl
  | succ n h =>
    rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← 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 : IsTriangulated.{v_1, u_1} C
n : ℕ
zero : P.extensionProductIter (HAdd.hAdd (α := ℕ) 0 1) = (P.extensionProductIter 0).extensionProduct P
⊢ P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P
have succ : ∀ (n : ℕ) (h : P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P),
  P.extensionProductIter (n + 1 + 1) = (P.extensionProductIter (n + 1)).extensionProduct P
Tactic: induction n with
  | zero => rfl
  | succ n h =>
    rw [extensionProductIter_succ, h, ← extensionProduct_assoc, ← extensionProductIter_succ, ← 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.Nonempty
n : ℕ
h : (P.extensionProductIter n).Nonempty
⊢ (P.extensionProductIter (n + 1)).Nonempty
have succ : (P.extensionProduct (P.extensionProductIter n)).Nonempty
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.Nonempty
n : ℕ
⊢ (P.extensionProductIter n).Nonempty
have zero : (P.extensionProductIter 0).Nonempty
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.Nonempty
n : ℕ
zero : (P.extensionProductIter 0).Nonempty
⊢ (P.extensionProductIter n).Nonempty
have succ : ∀ (n : ℕ) (h : (P.extensionProductIter n).Nonempty), (P.extensionProductIter (n + 1)).Nonempty
Tactic: induction n with
  | zero => rwa [extensionProductIter_zero]
  | succ n h => rw [extensionProductIter_succ]; infer_instance
Cleared hypotheses: n