mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.colimitsClosure J ≤ (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop

Tactic:
apply colimitsClosure_le

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P ≤ (P.op.limitsClosure fun a ↦ (J a)ᵒᵖ).unop
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteCoproducts C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
this✝ : P.IsClosedUnderIsomorphisms
this : HasFiniteCoproducts P.FullSubcategory
⊢ P.IsClosedUnderFiniteCoproducts

Tactic:
have := PreservesFiniteCoproducts.of_preserves_binary_and_initial P.ι

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteCoproducts C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
this✝¹ : P.IsClosedUnderIsomorphisms
this✝ : HasFiniteCoproducts P.FullSubcategory
this : ∀ (J : Type ?u.31) [Finite J], PreservesColimitsOfShape (Discrete J) P.ι
⊢ P.IsClosedUnderFiniteCoproducts
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 : Localization W), Hom.map (𝟙 X) F hF = 𝟙 (F.obj X)

Tactic:
intro (X : C)
    change (Hom.mk (ofHom W (𝟙 X))).map F hF = _
    rw [Hom.map_mk, map_ofHom, F.map_id]

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

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✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj φ.left
H : Triangle.mk φ.hom g h ∈ distinguishedTriangles
⊢ Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
      (L.map h ≫ (Functor.commShiftIso L 1).hom.app φ.left ≫ (shiftFunctor D 1).map (Arrow.Hom.left e.hom)) ≅
    L.mapTriangle.obj (Triangle.mk φ.hom g h)

Tactic:
refine Triangle.isoMk _ _ (Arrow.leftFunc.mapIso e.symm) (Arrow.rightFunc.mapIso e.symm)
    (Iso.refl _) e.inv.w.symm (by simp) ?_

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✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj φ.left
H : Triangle.mk φ.hom g h ∈ distinguishedTriangles
⊢ (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
          (L.map h ≫ (Functor.commShiftIso L 1).hom.app φ.left ≫ (shiftFunctor D 1).map (Arrow.Hom.left e.hom))).mor₃ ≫
      (shiftFunctor D 1).map (Arrow.leftFunc.mapIso e.symm).hom =
    (Iso.refl
          (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
              (L.map h ≫
                (Functor.commShiftIso L 1).hom.app φ.left ≫ (shiftFunctor D 1).map (Arrow.Hom.left e.hom))).obj₃).hom ≫
      (L.mapTriangle.obj (Triangle.mk φ.hom g h)).mor₃
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.RightFraction X Y
h : RightFractionRel z₁ z₂
⊢ LeftFractionRel z₁.op z₂.op

Tactic:
by
  obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
  exact ⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs,
    Quiver.Hom.unop_inj hf, ht⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ RightFractionRel z₁.op z₂.op

Tactic:
by
  obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
  exact ⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs,
    Quiver.Hom.unop_inj hf, ht⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
X Y Z : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (-β) h = -α.comp β h

Tactic:
rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
⊢ ∀ (h : RetractArrow f✝ g✝), P g✝ → P f✝

Tactic:
h₂

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h₂ : RetractArrow f✝ g✝
⊢ P g✝ → P f✝
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
F : C ⥤ D
inst✝ : F.CommShift M
⊢ (mk₀ m₀ hm₀ f).map F = mk₀ m₀ hm₀ (F.map f)

Tactic:
by
  subst hm₀
  simp [map, mk₀, shiftFunctorZero', F.commShiftIso_zero M, ← Functor.map_comp_assoc]

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

Goal state before:
pp: case succ
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 Q : ObjectProperty C
hPQ : P ≤ Q
n : ℕ
h : P.extensionProductIter n ≤ Q.extensionProductIter n
⊢ P.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)

Tactic:
monotone_extensionProduct_left _ hPQ,

Goal state after:
case succ
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 Q : ObjectProperty C
hPQ : P ≤ Q
n : ℕ
h : P.extensionProductIter n ≤ Q.extensionProductIter n
⊢ Q.extensionProduct (P.extensionProductIter n) ≤ Q.extensionProduct (Q.extensionProductIter n)
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 Q : ObjectProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
Z : C
a : Y ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f a b ∈ distinguishedTriangles
hZ : P Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), Q Z

Tactic:
exact ⟨Z, a, b, hT, h _ hZ⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
⊢ Q.map f = Q.map g

Tactic:
exact Q_map_eq_of_homotopy h

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Tactic:
by
        simp only [next] at hj hj'
        obtain rfl : i' = i + n := by lia
        obtain rfl : j' = j + n := by lia
        dsimp at hf ⊢
        simp only [Linear.comp_units_smul] at hf
        apply (one_smul (M := ℤˣ) _).symm.trans _
        rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Localization

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
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ 𝟙
        ((F.mapHomologicalComplexUpToQuasiIso c).obj
          (HomologicalComplexUpToQuasiIso.Qh.obj ((HomotopyCategory.quotient C c).obj K))) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        𝟙
          (HomologicalComplexUpToQuasiIso.Qh.obj
            ((HomotopyCategory.quotient D c).obj
              ((F.mapHomologicalComplex c).obj ((HomotopyCategory.quotient C c).obj K).as))) =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)

Tactic:
simp only [Category.comp_id, Category.id_comp]

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
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K =
    (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫
          HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)
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
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
eq₁ : (P.inverseImage F).trW (Triangle.mk s g h).mor₁ ↔ P.inverseImage F (Triangle.mk s g h).obj₃
eq₂ : P.trW (F.mapTriangle.obj (Triangle.mk s g h)).mor₁ ↔ P (F.mapTriangle.obj (Triangle.mk s g h)).obj₃
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)

Tactic:
dsimp at eq₁ eq₂

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
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ (inl f).v (p + 1) p ⋯ ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯ =
      (inl f).v (p + 1) p ⋯ ≫
        (Cochain.ofHom
              ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
          p p ⋯ ∧
    (inr f).f p ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯ =
      (inr f).f p ≫
        (Cochain.ofHom
              ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
          p p ⋯

Tactic:
ext_to_iff _ _ (p + 1) rfl

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ (((inl f).v (p + 1) p ⋯ ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯) ≫ (↑(fst g)).v p (p + 1) ⋯ =
        ((inl f).v (p + 1) p ⋯ ≫
            (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
              p p ⋯) ≫
          (↑(fst g)).v p (p + 1) ⋯ ∧
      ((inl f).v (p + 1) p ⋯ ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯) ≫ (snd g).v p p ⋯ =
        ((inl f).v (p + 1) p ⋯ ≫
            (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
              p p ⋯) ≫
          (snd g).v p p ⋯) ∧
    (inr f).f p ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯ =
      (inr f).f p ≫
        (Cochain.ofHom
              ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
          p p ⋯
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
inst✝ : P.IsTriangulated
T₁ T₂ : Triangle P.FullSubcategory
hT₁ : T₁ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
hT₂ : T₂ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : (P.ι.mapTriangle.obj T₁).obj₃ ⟶ (P.ι.mapTriangle.obj T₂).obj₃
hc₁ : (P.ι.mapTriangle.obj T₁).mor₂ ≫ c = P.ι.map b ≫ (P.ι.mapTriangle.obj T₂).mor₂
hc₂ : (P.ι.mapTriangle.obj T₁).mor₃ ≫ (shiftFunctor C 1).map (P.ι.map a) = c ≫ (P.ι.mapTriangle.obj T₂).mor₃
⊢ (T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a).hom = (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom

Tactic:
have := P.ι.commShiftIso_hom_naturality a (1 : ℤ)

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
inst✝ : P.IsTriangulated
T₁ T₂ : Triangle P.FullSubcategory
hT₁ : T₁ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
hT₂ : T₂ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : (P.ι.mapTriangle.obj T₁).obj₃ ⟶ (P.ι.mapTriangle.obj T₂).obj₃
hc₁ : (P.ι.mapTriangle.obj T₁).mor₂ ≫ c = P.ι.map b ≫ (P.ι.mapTriangle.obj T₂).mor₂
hc₂ : (P.ι.mapTriangle.obj T₁).mor₃ ≫ (shiftFunctor C 1).map (P.ι.map a) = c ≫ (P.ι.mapTriangle.obj T₂).mor₃
this :
  P.ι.map ((shiftFunctor P.FullSubcategory 1).map a) ≫ (Functor.commShiftIso P.ι 1).hom.app T₂.obj₁ =
    (Functor.commShiftIso P.ι 1).hom.app T₁.obj₁ ≫ (shiftFunctor C 1).map (P.ι.map a)
⊢ (T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a).hom = (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
⊢ (liftCochain φ α β h).comp (snd φ) ⋯ = β

Tactic:
by
  ext p q hpq
  simp [Cochain.comp_v (n₁ := n) (n₂ := -1) (n₁₂ := m) _ _ _ p _ _ (by lia)
    (Int.add_neg_cancel_right q 1)]

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

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i j : ι
hi : e.f i = i'
hj : e.f j = j'
⊢ (K.extend e).d i' j' = (K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv

Tactic:
apply extend.d_eq

Goal state after:
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:
intro i hi
    apply hi' i
    rw [← c'.prev_eq' hj, c'.prev_eq' hi]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryGE j
i' : ι'
hi' : c'.Rel i' (e.f j)
a : ι
ha : e.f a = i'
⊢ c'.Rel (e.f a) (e.f j)

Tactic:
simpa only [ha] using hi'

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

Tactic:
· obtain ⟨k', hk'⟩ := e.mem_next hj
    rw [← hk', e.rel_iff] at hj
    rw [← hk', ← c.next_eq' hj, hjk]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ i' = j'

Tactic:
← hj,

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✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ i' = e.f 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
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
by
  by_cases hij : c.Rel i j
  · have hi'' : e.f i = i' := by rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
    have : (K.extendXIso e hi'').hom ≫ f' = f'' := by
      apply Fork.IsLimit.hom_ext hcone
      rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
    rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, assoc]
  · have h₁ : f' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      simp only [zero_comp, hf', K.shape _ _ hij]
    have h₂ : f'' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
        K.extend_d_to_eq_zero e i' j' j hj']
      rw [hi]
      exact hij
    simp [h₁, h₂]

Goal state after:
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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).LeftHomologyData
⊢ (h.i ≫ (K.extendXIso e hj').inv) ≫ (K.extend e).d j' k' = 0

Tactic:
rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk']

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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).LeftHomologyData
⊢ h.i ≫ K.d j k = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

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.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
this : QuasiIsoAt (K.op.πTruncGE e.op) j'
⊢ QuasiIsoAt (K.ιTruncLE e) j'

Tactic:
exact inferInstanceAs (QuasiIsoAt ((unopFunctor _ _).map (K.op.πTruncGE e.op).op) j')

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

Goal state before:
pp: case left.inr.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₂ j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inr i₂) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inr i₂ = Sum.inr j₂

Tactic:
obtain rfl := e₂.injective_f h
      rfl

Goal state after: