awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk v₁₂ u₁₂ w₁₂).mor₂ ≫ u₂₃ = 𝟙 X₁ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₂
have dsimp : u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
rw : u₁₂ ≫ u₂₃ = u₁₃
⊢ u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃
have rw₁ : u₁₃ = u₁₃
Tactic: rw [id_comp, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₁ = u₂₃ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃
have dsimp : w₁₂ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₁ = u₂₃ ≫ w₁₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ w₁₂ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₁ = u₂₃ ≫ w₁₃
have rw : u₂₃ ≫ w₁₃ = u₂₃ ≫ w₁₃
Tactic: rw [h.comm₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁ ≫ u₁₂ = h.m₃ ≫ (Triangle.mk v₂₃ u₂₃ w₂₃).mor₁
have dsimp : v₁₃ ≫ u₁₂ = h.m₃ ≫ v₂₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ v₁₃ ≫ u₁₂ = h.m₃ ≫ v₂₃
have rw : v₁₃ ≫ u₁₂ = v₁₃ ≫ u₁₂
Tactic: rw [h.comm₄]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₂ ≫ 𝟙 X₃ = u₁₂ ≫ (Triangle.mk v₂₃ u₂₃ w₂₃).mor₂
have dsimp : u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃
have rw : u₁₃ = u₁₂ ≫ u₂₃
Tactic: rw [comp_id, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
rw : u₁₃ = u₁₂ ≫ u₂₃
⊢ u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃
have rw₁ : u₁₃ = u₁₃
Tactic: rw [comp_id, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₃ = 𝟙 X₃ ≫ (Triangle.mk v₂₃ u₂₃ w₂₃).mor₃
have dsimp : w₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₃ = 𝟙 X₃ ≫ w₂₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ w₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₃ = 𝟙 X₃ ≫ w₂₃
have rw : w₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₃ = w₂₃
Tactic: rw [id_comp, h.comm₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
h : Octahedron' comm h₁₂ h₂₃ h₁₃
rw : w₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₃ = w₂₃
⊢ w₁₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) h.m₃ = 𝟙 X₃ ≫ w₂₃
have rw₁ : w₂₃ = w₂₃
Tactic: rw [id_comp, h.comm₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃
have eq₁ : (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃ ≫ o.m₁ = u₂₃ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃
Tactic: have eq₁ := o.comm₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃ ≫ o.m₁ = u₂₃ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃
have eq₂ : o.m₁ ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁) =
  -Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₂ u₁₂ w₁₂).mor₁
Tactic: have eq₂ := o.comm₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃ ≫ o.m₁ = u₂₃ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃
eq₂ :
  o.m₁ ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁) =
    -Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₂ u₁₂ w₁₂).mor₁
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃
have eq₃ : (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃ ≫ o.m₃ = (Triangle.mk v₂₃ u₂₃ w₂₃).mor₃
Tactic: have eq₃ := o.comm₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Triangulated (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} 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
inst_6 : IsTriangulated.{v_1, u_1} C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₂
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₂ u₁₂ w₁₂)
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₂₃
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₂₃ u₂₃ w₂₃)
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Z₁₃
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk v₁₃ u₁₃ w₁₃)
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ :=
  Iso.inv (shiftShiftNeg Z₁₂ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₁ ≫ Iso.hom (shiftShiftNeg Z₁₃ 1)
m₃ : Z₁₃ ⟶ Z₂₃ :=
  Iso.inv (shiftShiftNeg Z₁₃ 1) ≫ Functor.map (shiftFunctor C (A := ℤ) (-1)) o.m₃ ≫ Iso.hom (shiftShiftNeg Z₂₃ 1)
eq₁ : (Triangle.mk v₁₂ u₁₂ w₁₂).mor₃ ≫ o.m₁ = u₂₃ ≫ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃
eq₂ :
  o.m₁ ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁) =
    -Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₂ u₁₂ w₁₂).mor₁
eq₃ : (Triangle.mk v₁₃ u₁₃ w₁₃).mor₃ ≫ o.m₃ = (Triangle.mk v₂₃ u₂₃ w₂₃).mor₃
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃
have eq₄ : (-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1) u₁₂ =
  o.m₃ ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk v₂₃ u₂₃ w₂₃).mor₁)
Tactic: have eq₄ := o.comm₄