awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{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 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
⊢ Nonempty (Abelian.AbelianStruct f₁)
have have : ∀ (H : Octahedron sorry sorry sorry sorry), Nonempty (Abelian.AbelianStruct f₁)
Tactic: have H := someOctahedron (show f₂ ≫ β = ι.map (πQ f₂ β) by simp)
      (rot_of_distTriang _ hT) (rot_of_distTriang _ hT')
      (rot_of_distTriang _ hI)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{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 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
⊢ Nonempty (Abelian.AbelianStruct f₁)
have obtain : ∀ (m₁ : X₁ ⟶ I) (hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁), Nonempty (Abelian.AbelianStruct f₁)
Tactic: obtain ⟨m₁, hm₁⟩ : ∃ (m₁ : X₁ ⟶ I), (shiftFunctor C (1 : ℤ)).map (ι.map m₁) = H.m₁ :=
      ⟨(ι ⋙ shiftFunctor C (1 : ℤ)).preimage H.m₁, Functor.map_preimage (ι ⋙ _) _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{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 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
⊢ Nonempty (Abelian.AbelianStruct f₁)
have obtain : ∀ (m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
  (hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃), Nonempty (Abelian.AbelianStruct f₁)
Tactic: obtain ⟨m₃ : ι.obj I ⟶ (ι.obj K)⟦(1 : ℤ)⟧, hm₃⟩ :
        ∃ m₃, (shiftFunctor C (1 : ℤ)).map m₃ = H.m₃ :=
      ⟨(shiftFunctor C (1 : ℤ)).preimage H.m₃, Functor.map_preimage _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{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 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃))
have rw : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
  (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) 1)
    (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate)
Tactic: rw [rotate_distinguished_triangle, ← Triangle.shift_distinguished_iff _ 1]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{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 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) 1)
      (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate)
have refine : Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) 1) (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ≅
  Triangle.mk H.m₁ H.m₃
    ((-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk α β γ).mor₁) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk (ι.map f₁) f₂ f₃).mor₃)
Tactic: refine isomorphic_distinguished _ H.mem _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (hypothesis)
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{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 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
⊢ Nonempty (Abelian.AbelianStruct f₁)
have Hmem : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
  (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃))
Tactic: have Hmem : Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃) ∈ distTriang C := by
      rw [rotate_distinguished_triangle, ← Triangle.shift_distinguished_iff _ 1]
      refine isomorphic_distinguished _ H.mem _ ?_
      exact Triangle.isoMk _ _ (-(Iso.refl _)) (Iso.refl _) (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (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
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ ∃ (X : C) (Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y) (h :
    Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f g h)
have obtain : ∀ (X Y : C) (hX : t.le 0 X) (hY : t.ge 1 Y) (f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A)
  (g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y)
  (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
  (mem :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f g h)),
  ∃ (X : C) (Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y) (h :
    Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f g h)
Tactic: obtain ⟨X, Y, hX, hY, f, g, h, mem⟩ := t.exists_triangle_zero_one (A⟦n₀⟧)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (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
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃)
have refine : Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ≅
  Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)
Tactic: refine isomorphic_distinguished _ (Triangle.shift_distinguished _ mem (-n₀)) _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (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
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
⊢ Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ≅
    Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)
have refine_1 : (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₁ ≫ e.symm.hom =
  Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁) ≫
    (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₁
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (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
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
refine_1 :
  (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₁ ≫ e.symm.hom =
    Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁) ≫
      (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₁
⊢ Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ≅
    Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)
have refine_2 : (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₂ ≫
    Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃) =
  e.symm.hom ≫ (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₂
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (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
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
refine_1 :
  (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₁ ≫ e.symm.hom =
    Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁) ≫
      (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₁
refine_2 :
  (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₂ ≫
      Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃) =
    e.symm.hom ≫ (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₂
⊢ Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ≅
    Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)
have refine_3 : (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₃ ≫
    Functor.map (shiftFunctor C (A := ℤ) 1)
      (Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁)) =
  Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃) ≫
    (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₃
Tactic: refine Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _) ?_ ?_ ?_