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 ℤ
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.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0 ≫ 0))) 0
rw₂ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0) ≫ F.map 0)) 0
rw₃ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0) 0
rw₄ :
  Eq (α := F.obj X ⟶ F.obj Y)
    (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (CategoryStruct.comp (Y := F.obj 0) 0 (F.map 0))) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have rw₅ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) 0) 0
Tactic: rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
-- 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.IsTriangulated
X Y : C
h₁ : Eq.{v_1 + 1} (α := X ⟶ Y) 0 (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))
h₂ : Eq.{v_2 + 1} (α := F.obj 0 ⟶ F.obj 0) (𝟙 (F.obj 0)) 0
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := 0) 0 (𝟙 0 ≫ 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0 ≫ 0))) 0
rw₂ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map (𝟙 0) ≫ F.map 0)) 0
rw₃ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0) 0
rw₄ :
  Eq (α := F.obj X ⟶ F.obj Y)
    (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (CategoryStruct.comp (Y := F.obj 0) 0 (F.map 0))) 0
rw₅ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) 0) 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) 0
have rw₆ : Eq.{v_2 + 1} (α := F.obj X ⟶ F.obj Y) 0 0
Tactic: rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]
-- 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
inst_20 : F.IsTriangulated
this :
  ∀ (X₁ X₃ : C),
    IsIso (X := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (prodComparison F X₁ X₃)
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F
have this₁ : ∀ (X₁ X₃ : C), PreservesLimit (pair X₁ X₃) F
Tactic: have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.of_iso_prod_comparison F X₁ X₃
-- 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.IsTriangulated
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F
have suffices : ∀ (X₁ X₃ : C),
  IsIso (X := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (prodComparison F X₁ X₃)
Tactic: suffices ∀ (X₁ X₃ : C), IsIso (prodComparison F X₁ X₃) by
    have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.of_iso_prod_comparison F X₁ X₃
    exact ⟨fun {K} ↦ preservesLimit_of_iso_diagram F (diagramIsoPair K).symm⟩
-- 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.IsTriangulated
X₁ X₃ : C
⊢ Triangle.mor₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃)) ≫
      prodComparison F X₁ X₃ =
    𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))) ≫
      Triangle.mor₁ (binaryProductTriangle (F.obj X₁) (F.obj X₃))
have dsimp : Eq (α := F.obj X₁ ⟶ Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
  (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
    (prodComparison F X₁ X₃))
  (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
Tactic: dsimp
-- 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.IsTriangulated
X₁ X₃ : C
⊢ Eq (α := F.obj X₁ ⟶ Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
      (prodComparison F X₁ X₃))
    (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
have h₁ : CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
      (prodComparison F X₁ X₃))
    prod.fst =
  CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃)) (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
    prod.fst
Tactic: ext
-- 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.IsTriangulated
X₁ X₃ : C
h₁ :
  CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
      (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
        (prodComparison F X₁ X₃))
      prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃)) (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
      prod.fst
⊢ Eq (α := F.obj X₁ ⟶ Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
      (prodComparison F X₁ X₃))
    (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
have h₂ : CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃))
    (CategoryStruct.comp (Y := F.obj (Limits.prod.{v_1, u_1} X₁ X₃)) (F.map (prod.lift (𝟙 X₁) 0))
      (prodComparison F X₁ X₃))
    prod.snd =
  CategoryStruct.comp (Y := Limits.prod.{v_2, u_2} (F.obj X₁) (F.obj X₃)) (𝟙 (F.obj X₁) ≫ prod.lift (𝟙 (F.obj X₁)) 0)
    prod.snd
Tactic: ext
-- 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.IsTriangulated
X₁ X₃ : C
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D)
  (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))
  (binaryProductTriangle (F.obj X₁) (F.obj X₃)) :=
  { hom₁ := 𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso φ.hom₁
have dsimp : IsIso.{v_2, u_2} (𝟙 (F.obj X₁))
Tactic: dsimp [φ]
-- 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.IsTriangulated
X₁ X₃ : C
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D)
  (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))
  (binaryProductTriangle (F.obj X₁) (F.obj X₃)) :=
  { hom₁ := 𝟙 (Triangle.obj₁ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    hom₂ := prodComparison F X₁ X₃,
    hom₃ := 𝟙 (Triangle.obj₃ (obj (C := Triangle.{v_1, u_1} C) F.mapTriangle (binaryProductTriangle X₁ X₃))),
    comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
⊢ IsIso φ.hom₃
have dsimp : IsIso.{v_2, u_2} (𝟙 (F.obj X₃))
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 ℤ
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.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
      (obj F.mapTriangle T) ↔
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
have refine : ∀
  (hT :
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
      (obj F.mapTriangle T)),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
Tactic: refine ⟨fun hT ↦ ?_, F.map_distinguished T⟩
-- 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.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
    (obj F.mapTriangle T)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
have obtain : ∀ (Z : C) (g : T.obj₂ ⟶ Z) (h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁)
  (mem :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
      (Triangle.mk T.mor₁ g h)),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
Tactic: obtain ⟨Z, g, h, mem⟩ := distinguished_cocone_triangle T.mor₁
-- 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.Full
inst_15 : F.Faithful
T : Triangle.{v_1, u_1} C
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_6 _ inst_8 inst_10 _)
    (obj F.mapTriangle T)
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _)
    (Triangle.mk T.mor₁ g h)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_5 _ inst_7 inst_9 _) T
have refine : Iso (C := Triangle.{v_2, u_2} D) (obj F.mapTriangle T) (obj F.mapTriangle (Triangle.mk T.mor₁ g h))
Tactic: refine isomorphic_distinguished _ mem _ (F.mapTriangle.preimageIso ?_)
-- 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 : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), 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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
⊢ F₁.IsTriangulated ↔ F₂.IsTriangulated
have mp : F₁.IsTriangulated → F₂.IsTriangulated
Tactic: constructor
-- 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 : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), 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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
mp : F₁.IsTriangulated → F₂.IsTriangulated
⊢ F₁.IsTriangulated ↔ F₂.IsTriangulated
have mpr : F₂.IsTriangulated → F₁.IsTriangulated
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Functor (hypothesis)
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 : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), 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₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
e : F₁ ≅ F₂
inst_12 : F₁.CommShift ℤ
inst_13 : F₂.CommShift ℤ
inst_14 : NatTrans.CommShift e.hom ℤ
h : F₂.IsTriangulated
⊢ F₁.IsTriangulated
have this : NatTrans.CommShift e.symm.hom ℤ
Tactic: have : NatTrans.CommShift e.symm.hom ℤ := inferInstanceAs (NatTrans.CommShift e.inv ℤ)
-- 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 ↔ H.IsTriangulated
have rw : F.IsTriangulated ↔ (F ⋙ G).IsTriangulated
Tactic: rw [← isTriangulated_iff_of_iso e]