mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
m : (shiftFunctor C 1).obj (Triangle.mk α β γ).obj₁ ⟶ ι.obj B
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ m
⊢ (shiftFunctorAdd' C 1 1 2 epi_πQ._proof_1_2).hom.app (ι.obj K) ≫ m = 0

Tactic:
]

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
m : (shiftFunctor C 1).obj (Triangle.mk α β γ).obj₁ ⟶ ι.obj B
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ m
⊢ (shiftFunctorAdd' C 1 1 2 epi_πQ._proof_1_2).hom.app (ι.obj K) ≫ m = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ 0
⊢ ι.map k = ι.map 0

Tactic:
hm,

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ 0
⊢ (Triangle.mk α β γ).mor₃ ≫ 0 = ι.map 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLTι b).app ((t.eTruncLT.obj c).obj X)) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))

Tactic:
]

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X) ≫
      (t.eTruncGE.obj a).map ((t.eTruncLTι b).app ((t.eTruncLT.obj c).obj X)) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
x₁ : B ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
k' : (shiftFunctor C 1).obj (ι.obj B) ⟶ (shiftFunctor C 1).obj (ι.obj K)
hk' : (shiftFunctor C 1).map (ι.map x₁) = k' ≫ α ≫ f₃
⊢ k' ≫ α ≫ f₃ = k' ≫ α ≫ f₃

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
W'✝ : A
x₁ : W'✝ ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
m : W'✝ ⟶ K
hm : m ≫ ιK f₃ α = x₁
this : Mono (ιK f₃ α)
⊢ x₁ = x₁

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝¹ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this✝ : Mono ((adj.homEquiv Z T.obj₃) h)
this : IsIso ((adj.homEquiv Z T.obj₃) h)
⊢ g = g

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : Category.{v_2, u_2} D
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : HasShift D ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
E : C ≌ D
inst✝² : E.functor.CommShift ℤ
inst✝¹ : E.inverse.CommShift ℤ
inst✝ : E.CommShift ℤ
⊢ Adjunction.id.IsTriangulated

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : Category.{v_2, u_2} D
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : HasShift D ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Pretriangulated D
E : C ≌ D
inst✝² : E.functor.CommShift ℤ
inst✝¹ : E.inverse.CommShift ℤ
inst✝ : E.CommShift ℤ
⊢ Adjunction.id.IsTriangulated
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝²⁵ : Category.{v_1, u_1} C
inst✝²⁴ : Category.{v_2, u_2} D
inst✝²³ : HasZeroObject C
inst✝²² : HasZeroObject D
inst✝²¹ : Preadditive C
inst✝²⁰ : Preadditive D
inst✝¹⁹ : HasShift C ℤ
inst✝¹⁸ : HasShift D ℤ
inst✝¹⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁵ : Pretriangulated C
inst✝¹⁴ : Pretriangulated D
E : C ≌ D
inst✝¹³ : E.functor.CommShift ℤ
inst✝¹² : E.inverse.CommShift ℤ
inst✝¹¹ : E.CommShift ℤ
D' : Type u_3
inst✝¹⁰ : Category.{v_3, u_3} D'
inst✝⁹ : HasZeroObject D'
inst✝⁸ : Preadditive D'
inst✝⁷ : HasShift D' ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D' n).Additive
inst✝⁵ : Pretriangulated D'
E' : D ≌ D'
inst✝⁴ : E'.functor.CommShift ℤ
inst✝³ : E'.inverse.CommShift ℤ
inst✝² : E'.CommShift ℤ
inst✝¹ : E.IsTriangulated
inst✝ : E'.IsTriangulated
⊢ (E.toAdjunction.comp E'.toAdjunction).IsTriangulated

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝²⁵ : Category.{v_1, u_1} C
inst✝²⁴ : Category.{v_2, u_2} D
inst✝²³ : HasZeroObject C
inst✝²² : HasZeroObject D
inst✝²¹ : Preadditive C
inst✝²⁰ : Preadditive D
inst✝¹⁹ : HasShift C ℤ
inst✝¹⁸ : HasShift D ℤ
inst✝¹⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁵ : Pretriangulated C
inst✝¹⁴ : Pretriangulated D
E : C ≌ D
inst✝¹³ : E.functor.CommShift ℤ
inst✝¹² : E.inverse.CommShift ℤ
inst✝¹¹ : E.CommShift ℤ
D' : Type u_3
inst✝¹⁰ : Category.{v_3, u_3} D'
inst✝⁹ : HasZeroObject D'
inst✝⁸ : Preadditive D'
inst✝⁷ : HasShift D' ℤ
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D' n).Additive
inst✝⁵ : Pretriangulated D'
E' : D ≌ D'
inst✝⁴ : E'.functor.CommShift ℤ
inst✝³ : E'.inverse.CommShift ℤ
inst✝² : E'.CommShift ℤ
inst✝¹ : E.IsTriangulated
inst✝ : E'.IsTriangulated
⊢ (E.toAdjunction.comp E'.toAdjunction).IsTriangulated
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
Z'✝ : A
x₂ : X₂ ⟶ Z'✝
hx₂ : f₁ ≫ x₂ = 0
m : Q ⟶ Z'✝
hm : πQ f₂ β ≫ m = x₂
⊢ m = ⋯.choose

Tactic:
have := epi_πQ hι hT hT'

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
Z'✝ : A
x₂ : X₂ ⟶ Z'✝
hx₂ : f₁ ≫ x₂ = 0
m : Q ⟶ Z'✝
hm : πQ f₂ β ≫ m = x₂
this : Epi (πQ f₂ β)
⊢ m = ⋯.choose
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
Z'✝ : A
x₂ : X₂ ⟶ Z'✝
hx₂ : f₁ ≫ x₂ = 0
m : Q ⟶ Z'✝
hm : πQ f₂ β ≫ m = x₂
this : Epi (πQ f₂ β)
⊢ x₂ = x₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: case refine_1
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: case refine_2
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
hQ : 𝟙 Q = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
hQ : 𝟙 Q = 0
this : IsIso α
⊢ (Triangle.mk (ι.map (-ιK f₃ α)) (ι.map π) (f₂ ≫ inv α)).rotate ∈ distinguishedTriangles

Tactic:
]

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι π
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₁
β : X₁ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
hQ : 𝟙 Q = 0
this : IsIso α
⊢ (Triangle.mk (ι.map (-ιK f₃ α)) (ι.map π) (f₂ ≫ inv α)).rotate ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
⊢ Nonempty (Abelian.AbelianStruct f₁)

Tactic:
have := epi_πQ hι hT hT'

Goal state after:
C : Type u_1
A : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁵ : Preadditive A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasFiniteProducts A
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
inst✝ : IsTriangulated C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι f₁
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
this : Epi (πQ f₂ β)
⊢ Nonempty (Abelian.AbelianStruct f₁)