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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
⊢ T₁.mor₂ ≫ (Triangle.π₃.mapIso h.choose).hom = e₂.hom ≫ T₂.mor₂

Tactic:
dsimp at eq ⊢

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₂ = e₂.hom
⊢ T₁.mor₂ ≫ h.choose.hom.hom₃ = e₂.hom ≫ T₂.mor₂
Module: Mathlib.CategoryTheory.Triangulated.Functor

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ : D
⊢ ∀ {Z₁₃ : D} {u₁₂ : Y₁ ⟶ Y₂} {u₂₃ : Y₂ ⟶ Y₃} {u₁₃ : Y₁ ⟶ Y₃} (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : Y₂ ⟶ Z₁₂}
    {w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃}
    {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
Z₁₃

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated 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₁₂ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃}
    {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = (Triangle.π₃.mapIso h.choose).hom ≫ T₂.mor₃

Tactic:
dsimp at eq ⊢

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₁ = e₁.hom
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = h.choose.hom.hom₃ ≫ T₂.mor₃
Module: Mathlib.CategoryTheory.Triangulated.Functor

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated 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₁₂ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃}
    {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
w₁₂

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated 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₁₂ ⟶ (shiftFunctor D 1).obj Y₁
⊢ ∀ (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂}
    (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁}
    (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles), Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
Module: Mathlib.CategoryTheory.Localization.Predicate

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
L : C ⥤ D
inst✝ : L.IsLocalization ⊤
⊢ IsGroupoid D

Tactic:
isGroupoid_iff_isomorphisms_eq_top

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
L : C ⥤ D
inst✝ : L.IsLocalization ⊤
⊢ MorphismProperty.isomorphisms D = ⊤
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ L.map f = L.map g → W.Q.map f = W.Q.map g

Tactic:
intro h
    let e := Localization.compUniqFunctor L W.Q W
    rw [← NatIso.naturality_1 e f, ← NatIso.naturality_1 e g]
    dsimp
    rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case mp.refine_1
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ φ.s ≫ t₁' ≫ α.s ≫ u ≫ u' = ψ.s ≫ t₂' ≫ α.s ≫ u ≫ u'

Tactic:
rw [reassoc_of% hst']

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
φ : W.RightFraction₂ X Y
inst✝ : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f ≫ ψ₁.s = φ.s ≫ ψ₁.f
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' ≫ ψ₂.s = φ.s ≫ ψ₂.f
α : W.LeftFraction ψ₁.Y' ψ₂.Y'
hα : ψ₂.s ≫ α.s = ψ₁.s ≫ α.f
⊢ φ.f' ≫ { Y' := α.Y', f := ψ₁.f ≫ α.f, f' := ψ₂.f ≫ α.s, s := ψ₂.s ≫ α.s, hs := ⋯ }.s =
    φ.s ≫ { Y' := α.Y', f := ψ₁.f ≫ α.f, f' := ψ₂.f ≫ α.s, s := ψ₂.s ≫ α.s, hs := ⋯ }.f'

Tactic:
rw [reassoc_of% hψ₂]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
⊢ W ((shiftFunctor C a).map f) ↔ W f

Tactic:
by
  conv_rhs => rw [← @IsCompatibleWithShift.condition _ _ W A _ _ _ a]
  rfl

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT (Subtype (P i)) κ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨i, ⟨x, hx⟩⟩ => ⟨x, ⋯⟩

Tactic:
by
    rintro ⟨_, h⟩
    simp only [iSup_apply, iSup_Prop_eq] at h
    obtain ⟨i, hi⟩ := h
    exact ⟨⟨i, _, hi⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
g : Y ⟶ Z
f : W.LeftFraction X Y
⊢ Hom.map (Hom.mk f ≫ g) F hF = (Hom.mk f).map F hF ≫ Hom.map g F hF

Tactic:
obtain ⟨g, rfl⟩ := Hom.mk_surjective g

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
⊢ Hom.map (Hom.mk f ≫ Hom.mk g) F hF = (Hom.mk f).map F hF ≫ (Hom.mk g).map F hF
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderRetracts
⊢ P ≤ Q → P.retracts ≤ Q

Tactic:
intro h
    exact le_trans (retracts_monotone h) Q.retracts_le

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

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : HasZeroObject C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
P₁ P₂ Q : ObjectProperty C
inst✝¹ : Q.IsTriangulatedClosed₂
inst✝ : Q.IsClosedUnderIsomorphisms
h₁ : P₁ ≤ Q
h₂ : P₂ ≤ Q
⊢ P₁.extensionProduct P₂ ≤ Q

Tactic:
intro _ ⟨_, _, _, _, _, hT, hY, hZ⟩
  exact ext_of_isTriangulatedClosed₂ Q _ hT (h₁ _ hY) (h₂ _ hZ)

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

Goal state before:
pp: C : Type u_1
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : Preadditive C
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁸ : Pretriangulated C
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : HasShift E ℤ
P : ObjectProperty C
X Y Y' : C
e : Y ⟶ Y'
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ P.trW (f ≫ e)

Tactic:
refine ⟨Z, inv e ≫ g, h, isomorphic_distinguished _ mem _ ?_, mem'⟩

Goal state after:
C : Type u_1
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasShift C ℤ
inst✝¹⁰ : Preadditive C
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁸ : Pretriangulated C
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : HasShift E ℤ
P : ObjectProperty C
X Y Y' : C
e : Y ⟶ Y'
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ Triangle.mk (f ≫ e) (inv e ≫ g) h ≅ Triangle.mk f g h
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ (if h : ∃ i, e.f i = i' then some h.choose else none) = some i

Tactic:
dif_pos ⟨i, hi⟩,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i : ι
i' : ι'
hi : e.f i = i'
h : ∃ i, e.f i = i'
this : h.choose = i
⊢ some ⋯.choose = some i
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
⊢ IsZero (X K none)

Tactic:
exact Limits.isZero_zero _

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
rw [extend.d_none_eq_zero' K _ _ hj']

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ (extend.XIso K hi).hom ≫
      K.d i j ≫ (extend.XIso K hj).inv ≫ (extend.XIso K hj).hom ≫ K.d j k ≫ (extend.XIso K hk).inv =
    0

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ (extend.XIso K hi).hom ≫ K.d i j ≫ K.d j k ≫ (extend.XIso K hk).inv = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
⊢ ¬c'.Rel (e.f i) (e.f j)

Tactic:
hi

Goal state after:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
i : ι
hi : c'.Rel (e.f i) (e.f j)
⊢ False
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.right
p : ℤ
i : ℕ
⊢ ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Tactic:
hi

Goal state after:
case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
⊢ False
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.right
p : ℤ
i : ℕ
⊢ ¬(up ℤ).Rel ((embeddingUpIntLE p).f 0) ((embeddingUpIntLE p).f i)

Tactic:
hi

Goal state after:
case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntLE p).f 0) ((embeddingUpIntLE p).f i)
⊢ False
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'✝ : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'✝ : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ k, e.f k = i'
⊢ i' = e.f i

Tactic:
hi

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ k, e.f k = i'
⊢ i' = i'
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ k, e.f k = i'
⊢ f φ i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv

Tactic:
have : hi'.choose = i := e.injective_f (by rw [hi'.choose_spec, hi])

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ k, e.f k = i'
this : hi'.choose = i
⊢ f φ i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'✝ : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
⊢ K.d i j ≫ φ = 0 ↔ (K.extendXIso e hi').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv ≫ (K.extendXIso e hj').hom ≫ φ = 0

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'✝ : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
⊢ K.d i j ≫ φ = 0 ↔ (K.extendXIso e hi').hom ≫ K.d i j ≫ φ = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) j

Tactic:
hi

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬c.Rel i j
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ ¬c.Rel (c.prev j) j

Tactic:
hi

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ ¬c.Rel i j
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.iCycles j' ≫
      (K.restrictionXIso e hj').inv ≫ (K.restrictionXIso e hj').hom ≫ K.d j' k' ≫ (K.restrictionXIso e hk').inv =
    0

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.iCycles j' ≫ K.d j' k' ≫ (K.restrictionXIso e hk').inv = 0