awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
⊢ F.IsTriangulated ↔ (F ⋙ G).IsTriangulated
have refine : (F ⋙ G).IsTriangulated →
  ∀ (T : Triangle.{v_1, u_1} C)
    (hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_6 _ inst_9 inst_12 _) T),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_7 _ inst_10 inst_13 _)
      (obj F.mapTriangle T)
Tactic: refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun T hT ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
inst_6 : HasZeroObject.{v_1, u_1} C
inst_7 : HasZeroObject.{v_2, u_2} D
inst_8 : HasZeroObject.{v_3, u_3} E
inst_9 : Preadditive.{v_1, u_1} C
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : Preadditive.{v_3, u_3} E
inst_12 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_13 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_15 : Pretriangulated.{v_1, u_1} C
inst_16 : Pretriangulated.{v_2, u_2} D
inst_17 : Pretriangulated.{v_3, u_3} E
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_3, u_2, u_3} D E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_18 : F.CommShift ℤ
inst_19 : G.CommShift ℤ
inst_20 : H.CommShift ℤ
inst_21 : NatTrans.CommShift e.hom ℤ
inst_22 : G.IsTriangulated
inst_23 : G.Full
inst_24 : G.Faithful
h : (F ⋙ G).IsTriangulated
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_6 _ inst_9 inst_12 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_7 _ inst_10 inst_13 _)
    (obj F.mapTriangle T)
have rw : Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _)
  (obj (C := Triangle.{v_2, u_2} D) G.mapTriangle (obj F.mapTriangle T))
Tactic: rw [← G.map_distinguished_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : HasZeroObject.{v_2, u_2} D
inst_7 : Preadditive.{v_1, u_1} C
inst_8 : Preadditive.{v_2, u_2} D
inst_9 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_10 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_1, u_1} C
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : F.IsTriangulated
inst_14 : F.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _) T
X Y : C
f : X ⟶ Y
e₁ : F.obj X ≅ T.obj₁
e₂ : F.obj Y ≅ T.obj₂
w : F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁
⊢ ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T'),
    Nonempty.{v_2 + 1} (obj F.mapTriangle T' ≅ T)
have obtain : ∀ (W : C) (g : Y ⟶ W) (h : W ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
  (H :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
      (Triangle.mk f g h)),
  ∃ (T' : Triangle.{v_1, u_1} C) (_ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T'),
    Nonempty.{v_2 + 1} (obj F.mapTriangle T' ≅ T)
Tactic: obtain ⟨W, g, h, H⟩ := distinguished_cocone_triangle f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : (F ⋙ G).IsTriangulated
inst_21 : F.IsTriangulated
inst_22 : F.mapArrow.EssSurj
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_12 inst_15 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_10 _ inst_13 inst_16 _)
    (obj G.mapTriangle T)
have obtain : ∀ (T' : Triangle.{v_1, u_1} C)
  (hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_8 _ inst_11 inst_14 _) T')
  (e : obj F.mapTriangle T' ≅ T),
  Membership.mem (γ := Set (Triangle.{v_3, u_3} E)) (@distinguishedTriangles _ _ inst_10 _ inst_13 inst_16 _)
    (obj G.mapTriangle T)
Tactic: obtain ⟨T', hT', ⟨e⟩⟩ := F.mem_mapTriangle_essImage_of_distinguished T hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : HasZeroObject.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : HasZeroObject.{v_3, u_3} E
inst_11 : Preadditive.{v_1, u_1} C
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : Preadditive.{v_3, u_3} E
inst_14 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_15 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_16 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_17 : Pretriangulated.{v_1, u_1} C
inst_18 : Pretriangulated.{v_2, u_2} D
inst_19 : Pretriangulated.{v_3, u_3} E
H : Functor.{v_1, v_3, u_1, u_3} C E
e : F ⋙ G ≅ H
inst_20 : H.CommShift ℤ
inst_21 : H.IsTriangulated
inst_22 : F.IsTriangulated
inst_23 : F.mapArrow.EssSurj
inst_24 : NatTrans.CommShift e.hom ℤ
⊢ G.IsTriangulated
have this : (F ⋙ G).IsTriangulated
Tactic: have := (isTriangulated_iff_of_iso e).2 inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
⊢ F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁ ≫ F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁ = F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁
have dsimp : F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
⊢ F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
have rw : F.map (u₁₂ ≫ u₂₃) = F.map u₁₃
Tactic: rw [← F.map_comp, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
h : Octahedron comm h₁₂ h₂₃ h₁₃
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
rw : F.map (u₁₂ ≫ u₂₃) = F.map u₁₃
⊢ F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
have rw₁ : F.map u₁₃ = F.map u₁₃
Tactic: rw [← F.map_comp, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (F.mapComposableArrows 2)
inst_15 : IsTriangulated.{v_1, u_1} C
⊢ IsTriangulated.{v_2, u_2} D
have octahedron_axiom : ∀ {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : D} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃} (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X₁}
  (h₁₂ :
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
      (Triangle.mk u₁₂ v₁₂ w₁₂))
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X₂}
  (h₂₃ :
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
      (Triangle.mk u₂₃ v₂₃ w₂₃))
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X₁}
  (h₁₃ :
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
      (Triangle.mk u₁₃ v₁₃ w₁₃)),
  Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
Tactic: apply IsTriangulated.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (F.mapComposableArrows 2)
inst_15 : IsTriangulated.{v_1, u_1} C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
have octahedron_axiom : ∀ (α : ComposableArrows.{v_1, u_1} C 2) (e : Functor.obj (F.mapComposableArrows 2) α ≅ ComposableArrows.mk₂ u₁₂ u₂₃),
  Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
Tactic: obtain ⟨α, ⟨e⟩⟩ : ∃ (α : ComposableArrows C 2),
      Nonempty ((F.mapComposableArrows 2).obj α ≅ ComposableArrows.mk₂ u₁₂ u₂₃) :=
    ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (F.mapComposableArrows 2)
inst_15 : IsTriangulated.{v_1, u_1} C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
α : ComposableArrows.{v_1, u_1} C 2
e : Functor.obj (F.mapComposableArrows 2) α ≅ ComposableArrows.mk₂ u₁₂ u₂₃
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
have octahedron_axiom : ∀ (X₁ X₂ X₃ : C) (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃),
  Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
Tactic: obtain ⟨X₁, X₂, X₃, f, g, rfl⟩ := ComposableArrows.mk₂_surjective α
Cleared hypotheses: α, e
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (F.mapComposableArrows 2)
inst_15 : IsTriangulated.{v_1, u_1} C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
have octahedron_axiom : ∀ (w : C) (w_1 : X₂ ⟶ w) (w_2 : w ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁)
  (h₁₂' :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
      (Triangle.mk f w_1 w_2)),
  Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
Tactic: obtain ⟨_, _, _, h₁₂'⟩ := distinguished_cocone_triangle f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasZeroObject.{v_2, u_2} D
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (F.mapComposableArrows 2)
inst_15 : IsTriangulated.{v_1, u_1} C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
u₂₃ : Y₂ ⟶ Y₃
u₁₃ : Y₁ ⟶ Y₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Y₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₂ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
v₂₃ : Y₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₂
h₂₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
v₁₃ : Y₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) Y₁
h₁₃ :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk u₁₃ v₁₃ w₁₃)
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
e : Functor.obj (F.mapComposableArrows 2) (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ u₁₂ u₂₃
w : C
w_1 : X₂ ⟶ w
w_2 : w ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
h₁₂' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
    (Triangle.mk f w_1 w_2)
⊢ Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
have octahedron_axiom : ∀ (w : C) (w_3 : X₃ ⟶ w) (w_4 : w ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂)
  (h₂₃' :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_6 inst_8 _)
      (Triangle.mk g w_3 w_4)),
  Nonempty.{v_2 + 1} (Octahedron comm h₁₂ h₂₃ h₁₃)
Tactic: obtain ⟨_, _, _, h₂₃'⟩ := distinguished_cocone_triangle g