awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₁ = 𝟙 A.obj₁
rw₁ : TriangleMorphism.hom₁ (𝟙 A) = 𝟙 A.obj₁
⊢ e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 A.obj₁
have rw₂ : Eq.{v + 1} (α := A.obj₁ ⟶ A.obj₁) (𝟙 A.obj₁) (𝟙 A.obj₁)
Tactic: rw [← comp_hom₁, e.hom_inv_id, id_hom₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
⊢ e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂
have rw : (e.hom ≫ e.inv).hom₂ = 𝟙 A.obj₂
Tactic: rw [← comp_hom₂, e.hom_inv_id, id_hom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₂ = 𝟙 A.obj₂
⊢ e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂
have rw₁ : TriangleMorphism.hom₂ (𝟙 A) = 𝟙 A.obj₂
Tactic: rw [← comp_hom₂, e.hom_inv_id, id_hom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₂ = 𝟙 A.obj₂
rw₁ : TriangleMorphism.hom₂ (𝟙 A) = 𝟙 A.obj₂
⊢ e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂
have rw₂ : Eq.{v + 1} (α := A.obj₂ ⟶ A.obj₂) (𝟙 A.obj₂) (𝟙 A.obj₂)
Tactic: rw [← comp_hom₂, e.hom_inv_id, id_hom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
⊢ e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃
have rw : (e.hom ≫ e.inv).hom₃ = 𝟙 A.obj₃
Tactic: rw [← comp_hom₃, e.hom_inv_id, id_hom₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₃ = 𝟙 A.obj₃
⊢ e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃
have rw₁ : TriangleMorphism.hom₃ (𝟙 A) = 𝟙 A.obj₃
Tactic: rw [← comp_hom₃, e.hom_inv_id, id_hom₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.hom ≫ e.inv).hom₃ = 𝟙 A.obj₃
rw₁ : TriangleMorphism.hom₃ (𝟙 A) = 𝟙 A.obj₃
⊢ e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃
have rw₂ : Eq.{v + 1} (α := A.obj₃ ⟶ A.obj₃) (𝟙 A.obj₃) (𝟙 A.obj₃)
Tactic: rw [← comp_hom₃, e.hom_inv_id, id_hom₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
⊢ e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁
have rw : (e.inv ≫ e.hom).hom₁ = 𝟙 B.obj₁
Tactic: rw [← comp_hom₁, e.inv_hom_id, id_hom₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₁ = 𝟙 B.obj₁
⊢ e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁
have rw₁ : TriangleMorphism.hom₁ (𝟙 B) = 𝟙 B.obj₁
Tactic: rw [← comp_hom₁, e.inv_hom_id, id_hom₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₁ = 𝟙 B.obj₁
rw₁ : TriangleMorphism.hom₁ (𝟙 B) = 𝟙 B.obj₁
⊢ e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁
have rw₂ : Eq.{v + 1} (α := B.obj₁ ⟶ B.obj₁) (𝟙 B.obj₁) (𝟙 B.obj₁)
Tactic: rw [← comp_hom₁, e.inv_hom_id, id_hom₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂
have rw : (e.inv ≫ e.hom).hom₂ = 𝟙 B.obj₂
Tactic: rw [← comp_hom₂, e.inv_hom_id, id_hom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₂ = 𝟙 B.obj₂
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂
have rw₁ : TriangleMorphism.hom₂ (𝟙 B) = 𝟙 B.obj₂
Tactic: rw [← comp_hom₂, e.inv_hom_id, id_hom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₂ = 𝟙 B.obj₂
rw₁ : TriangleMorphism.hom₂ (𝟙 B) = 𝟙 B.obj₂
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂
have rw₂ : Eq.{v + 1} (α := B.obj₂ ⟶ B.obj₂) (𝟙 B.obj₂) (𝟙 B.obj₂)
Tactic: rw [← comp_hom₂, e.inv_hom_id, id_hom₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
⊢ e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃
have rw : (e.inv ≫ e.hom).hom₃ = 𝟙 B.obj₃
Tactic: rw [← comp_hom₃, e.inv_hom_id, id_hom₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₃ = 𝟙 B.obj₃
⊢ e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃
have rw₁ : TriangleMorphism.hom₃ (𝟙 B) = 𝟙 B.obj₃
Tactic: rw [← comp_hom₃, e.inv_hom_id, id_hom₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
e : A ≅ B
rw : (e.inv ≫ e.hom).hom₃ = 𝟙 B.obj₃
rw₁ : TriangleMorphism.hom₃ (𝟙 B) = 𝟙 B.obj₃
⊢ e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃
have rw₂ : Eq.{v + 1} (α := B.obj₃ ⟶ B.obj₃) (𝟙 B.obj₃) (𝟙 B.obj₃)
Tactic: rw [← comp_hom₃, e.inv_hom_id, id_hom₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
h : A = B
⊢ A.obj₁ = B.obj₁
have subst : A.obj₁ = A.obj₁
Tactic: subst h
Cleared hypotheses: B, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
h : A = B
⊢ TriangleMorphism.hom₁ (eqToHom h) = eqToHom ⋯
have subst : TriangleMorphism.hom₁ (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: B, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
h : A = B
⊢ A.obj₂ = B.obj₂
have subst : A.obj₂ = A.obj₂
Tactic: subst h
Cleared hypotheses: B, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
h : A = B
⊢ TriangleMorphism.hom₂ (eqToHom h) = eqToHom ⋯
have subst : TriangleMorphism.hom₂ (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: B, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
h : A = B
⊢ A.obj₃ = B.obj₃
have subst : A.obj₃ = A.obj₃
Tactic: subst h
Cleared hypotheses: B, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
A B : Triangle.{v, u} C
h : A = B
⊢ TriangleMorphism.hom₃ (eqToHom h) = eqToHom ⋯
have subst : TriangleMorphism.hom₃ (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: B, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g h : T₁ ⟶ T₂
⊢ f + g + h = f + (g + h)
have h₁ : (f + g + h).hom₁ = (f + (g + h)).hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g h : T₁ ⟶ T₂
h₁ : (f + g + h).hom₁ = (f + (g + h)).hom₁
⊢ f + g + h = f + (g + h)
have h₂ : (f + g + h).hom₂ = (f + (g + h)).hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g h : T₁ ⟶ T₂
h₁ : (f + g + h).hom₁ = (f + (g + h)).hom₁
h₂ : (f + g + h).hom₂ = (f + (g + h)).hom₂
⊢ f + g + h = f + (g + h)
have h₃ : (f + g + h).hom₃ = (f + (g + h)).hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ 0 + f = f
have h₁ : (0 + f).hom₁ = f.hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (0 + f).hom₁ = f.hom₁
⊢ 0 + f = f
have h₂ : (0 + f).hom₂ = f.hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (0 + f).hom₁ = f.hom₁
h₂ : (0 + f).hom₂ = f.hom₂
⊢ 0 + f = f
have h₃ : (0 + f).hom₃ = f.hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ f + 0 = f
have h₁ : (f + 0).hom₁ = f.hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (f + 0).hom₁ = f.hom₁
⊢ f + 0 = f
have h₂ : (f + 0).hom₂ = f.hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (f + 0).hom₁ = f.hom₁
h₂ : (f + 0).hom₂ = f.hom₂
⊢ f + 0 = f
have h₃ : (f + 0).hom₃ = f.hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ (n + 1) • f = n • f + f
have h₁ : ((n + 1) • f).hom₁ = (n • f + f).hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : ((n + 1) • f).hom₁ = (n • f + f).hom₁
⊢ (n + 1) • f = n • f + f
have h₂ : ((n + 1) • f).hom₂ = (n • f + f).hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : ((n + 1) • f).hom₁ = (n • f + f).hom₁
h₂ : ((n + 1) • f).hom₂ = (n • f + f).hom₂
⊢ (n + 1) • f = n • f + f
have h₃ : ((n + 1) • f).hom₃ = (n • f + f).hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ f - g = f + -g
have h₁ : (f - g).hom₁ = (f + -g).hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
h₁ : (f - g).hom₁ = (f + -g).hom₁
⊢ f - g = f + -g
have h₂ : (f - g).hom₂ = (f + -g).hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
h₁ : (f - g).hom₁ = (f + -g).hom₁
h₂ : (f - g).hom₂ = (f + -g).hom₂
⊢ f - g = f + -g
have h₃ : (f - g).hom₃ = (f + -g).hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f = HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f
have h₁ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₁
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f = HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f
have h₂ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₁
h₂ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₂
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f = HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f
have h₃ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₃ = (HSMul.hSMul (α := ℤ) (↑n : ℤ) f + f).hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
⊢ Int.negSucc n • f = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f
have h₁ : (Int.negSucc n • f).hom₁ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : (Int.negSucc n • f).hom₁ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁
⊢ Int.negSucc n • f = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f
have h₂ : (Int.negSucc n • f).hom₂ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
n : ℕ
f : T₁ ⟶ T₂
h₁ : (Int.negSucc n • f).hom₁ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₁
h₂ : (Int.negSucc n • f).hom₂ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₂
⊢ Int.negSucc n • f = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f
have h₃ : (Int.negSucc n • f).hom₃ = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) f).hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
⊢ -f + f = 0
have h₁ : (-f + f).hom₁ = TriangleMorphism.hom₁ 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (-f + f).hom₁ = TriangleMorphism.hom₁ 0
⊢ -f + f = 0
have h₂ : (-f + f).hom₂ = TriangleMorphism.hom₂ 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f : T₁ ⟶ T₂
h₁ : (-f + f).hom₁ = TriangleMorphism.hom₁ 0
h₂ : (-f + f).hom₂ = TriangleMorphism.hom₂ 0
⊢ -f + f = 0
have h₃ : (-f + f).hom₃ = TriangleMorphism.hom₃ 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
⊢ f + g = g + f
have h₁ : (f + g).hom₁ = (g + f).hom₁
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
h₁ : (f + g).hom₁ = (g + f).hom₁
⊢ f + g = g + f
have h₂ : (f + g).hom₂ = (g + f).hom₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
f g : T₁ ⟶ T₂
h₁ : (f + g).hom₁ = (g + f).hom₁
h₂ : (f + g).hom₂ = (g + f).hom₂
⊢ f + g = g + f
have h₃ : (f + g).hom₃ = (g + f).hom₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
T' : Triangle.{v, u} C
φ : (j : J) → T' ⟶ T j
⊢ T'.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁) =
    (Pi.lift fun (j : J) ↦ (φ j).hom₃) ≫ (productTriangle T).mor₃
have dsimp : Eq (α := T'.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
  (T'.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁))
  (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) (Pi.lift fun (j : J) ↦ (φ j).hom₃)
    (CategoryStruct.comp (Y :=
      piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
      (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
      (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
T' : Triangle.{v, u} C
φ : (j : J) → T' ⟶ T j
⊢ Eq (α := T'.obj₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
    (T'.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁))
    (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) (Pi.lift fun (j : J) ↦ (φ j).hom₃)
      (CategoryStruct.comp (Y :=
        piObj.{u_1, v, u} fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁)
        (Limits.Pi.map fun (j : J) ↦ (T j).mor₃)
        (inv (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))))
have rw : Eq (α := T'.obj₃ ⟶ piObj.{u_1, v, u} fun (b : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T b).obj₁)
  (T'.mor₃ ≫
    CategoryStruct.comp (Y :=
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₁))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (Pi.lift fun (j : J) ↦ (φ j).hom₁))
      (piComparison (shiftFunctor C (A := ℤ) 1) fun (j : J) ↦ (T j).obj₁))
  (CategoryStruct.comp (Y := piObj.{u_1, v, u} fun (j : J) ↦ (T j).obj₃) (Pi.lift fun (j : J) ↦ (φ j).hom₃)
    (Limits.Pi.map fun (j : J) ↦ (T j).mor₃))
Tactic: rw [← cancel_mono (piComparison _ _), assoc, assoc, assoc, IsIso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m = (fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s
have h₁ : m.hom₁ = TriangleMorphism.hom₁ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
T : J → Triangle.{v, u} C
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₁
inst_3 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₂
inst_4 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ (T j).obj₃
inst_5 : HasProduct.{u_1, v, u} (C := C) fun (j : J) ↦ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) (T j).obj₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
h₁ : m.hom₁ = TriangleMorphism.hom₁ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
⊢ m = (fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s
have h₂ : m.hom₂ = TriangleMorphism.hom₂ ((fun (s : Fan T) ↦ (lift T s.proj : s.pt ⟶ productTriangle T)) s)
Tactic: ext1