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

Goal state before:
pp: case mp
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) → ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
intro h n

Goal state after:
case mp
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h✝ : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h✝ ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
n : ℤ
⊢ IsIso ((F.shift n).map 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
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ c = 0

Tactic:
rw [← h, ha, hb, add_zero]

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
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : W.IsCompatibleWithTriangulation
n : ℤ
⊢ (shiftFunctor W.Localization n).Additive

Tactic:
by
  rw [Localization.functor_additive_iff W.Q W]
  exact Functor.additive_of_iso (W.Q.commShiftIso n)

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

Goal state before:
pp: case mpr
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 R : ObjectProperty C✝
inst✝ : IsTriangulated C✝
X A Z : C✝
f : A ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C✝ 1).obj A
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P A
B C : C✝
f' : B ⟶ Z
g' : Z ⟶ C
h' : C ⟶ (shiftFunctor C✝ 1).obj B
hT' : Triangle.mk f' g' h' ∈ distinguishedTriangles
hQ : Q B
hR : R C
⊢ (P.extensionProduct Q).extensionProduct R X

Tactic:
obtain ⟨Y, f'', h'', hT''⟩ := distinguished_cocone_triangle₁ (g ≫ g')

Goal state after:
case mpr
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 R : ObjectProperty C✝
inst✝ : IsTriangulated C✝
X A Z : C✝
f : A ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C✝ 1).obj A
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P A
B C : C✝
f' : B ⟶ Z
g' : Z ⟶ C
h' : C ⟶ (shiftFunctor C✝ 1).obj B
hT' : Triangle.mk f' g' h' ∈ distinguishedTriangles
hQ : Q B
hR : R C
Y : C✝
f'' : Y ⟶ X
h'' : C ⟶ (shiftFunctor C✝ 1).obj Y
hT'' : Triangle.mk f'' (g ≫ g') h'' ∈ distinguishedTriangles
⊢ (P.extensionProduct Q).extensionProduct R X
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
n : ℕ
⊢ ⊥.extensionProductIter (n + 1) = ⊥

Tactic:
rw [extensionProductIter_succ, extensionProduct_bot_left]

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✝¹ : HasZeroMorphisms C
inst✝ : CategoryWithHomology C
i : ι
x✝² x✝¹ : HomologicalComplex C c
x✝ : x✝² ⟶ x✝¹
hf : quasiIso C c x✝
⊢ IsIso ((homologyFunctor C c i).map x✝)

Tactic:
rw [mem_quasiIso_iff] at hf
  dsimp
  infer_instance

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f) → quasiIso C c ((quotient C c).map f)

Tactic:
rintro ⟨K', L', g, h, ⟨e⟩⟩
    rw [← quotient_map_mem_quasiIso_iff] at h
    exact ((quasiIso C c).arrow_mk_iso_iff e).1 h

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f → IsIso (Qh.map f)

Tactic:
exact Localization.inverts Qh (HomotopyCategory.quasiIso _ _) _

Goal state after:
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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            (δ (-1) 0
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯))
            ⋯ +
          -1 •
            (δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))

Tactic:
Units.neg_smul,

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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            (δ (-1) 0
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯))
            ⋯ +
          -(1 •
              (δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
                ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                  ⋯)
                ⋯)) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                ((inl f).comp (δ (-1) 0 (inl (mappingConeCompTriangle f g).mor₁)) ⋯ +
                  -1 • (δ (-1) 0 (inl f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                ⋯ +
              1 •
                (δ 1 2 ↑(fst (f ≫ g))).comp
                  ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))

Tactic:
Units.neg_smul,

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₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                ((inl f).comp (δ (-1) 0 (inl (mappingConeCompTriangle f g).mor₁)) ⋯ +
                  -(1 • (δ (-1) 0 (inl f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯))
                ⋯ +
              1 •
                (δ 1 2 ↑(fst (f ≫ g))).comp
                  ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
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
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
⊢ ∀ T ∈ distinguishedTriangles, F.essImage T.obj₁ → F.essImage T.obj₃ → F.essImage T.obj₂

Tactic:
rintro T hT ⟨X₁, ⟨e₁⟩⟩ ⟨X₃, ⟨e₃⟩⟩

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
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
T : Triangle D
hT : T ∈ distinguishedTriangles
X₁ : C
e₁ : F.obj X₁ ≅ T.obj₁
X₃ : C
e₃ : F.obj X₃ ≅ T.obj₃
⊢ F.essImage T.obj₂
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
⊢ False

Tactic:
obtain ⟨k, hk⟩ := hj hj'

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ False
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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' = K.iCycles j ≫ (K.extendXIso e hj').inv

Tactic:
simp only [← cancel_epi (K.extendCyclesIso e hj').hom, Iso.hom_inv_id_assoc,
    extendCyclesIso_hom_iCycles_assoc, Iso.hom_inv_id, comp_id]

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

Goal state before:
pp: case inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
φ : K ⟶ L
hK : K.IsStrictlySupportedOutside e₂
hL : L.IsStrictlySupportedOutside e₁
i₂ : ι₂
⊢ φ.f (e₂.f i₂) = HomologicalComplex.Hom.f 0 (e₂.f i₂)

Tactic:
apply (hK.isZero i₂).eq_of_src

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
h : (singleFunctor C n).map f₁ = (singleFunctor C n).map f₂
eq₁ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₁) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₁
eq₂ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₂
⊢ f₁ = f₂

Tactic:
rw [← eq₁, ← eq₂, h]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (equiv W L') ((equiv W L).symm f) = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
dsimp [equiv]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L')
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) ((homEquiv W L W.Q) f))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁵ : HasSmallLocalizedHom W₁ X Y
inst✝⁴ : HasSmallLocalizedHom W₁ Y Z
inst✝³ : HasSmallLocalizedHom W₁ X Z
inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)

Tactic:
by
  apply (SmallHom.equiv W₂ W₂.Q).injective
  simp [Φ.equiv_smallHomMap W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) (CatCommSq.iso _ _ _ _),
    SmallHom.equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (equiv W L) (f.shift n a' h) =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((equiv W L) f) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
dsimp [equiv]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (SmallHom.equiv W L) (f.shift n a' h) ≫ (Functor.commShiftIso L a').hom.app Y =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f ≫ (Functor.commShiftIso L a).hom.app Y) ≫
        (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ (equiv W L) (chgUniv e) = (equiv W L) e

Tactic:
dsimp [equiv]

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
L : C ⥤ D
inst✝³ : L.IsLocalization W
inst✝² : L.CommShift M
X Y : C
m : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ (SmallHom.equiv W L) (chgUniv e) ≫ (Functor.commShiftIso L m).hom.app Y =
    (SmallHom.equiv W L) e ≫ (Functor.commShiftIso L m).hom.app Y
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫
        ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso 1 n₀ n₁ ⋯).inv.app S.X₁ ≫
          ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso 1 n₀ n₁ ⋯).hom.app S.X₁ =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁

Tactic:
Iso.inv_hom_id_app

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles S.X₁ ((x' ≫ (triangle S.f).mor₃.f n₀) ≫ (S.X₁.shiftFunctorObjXIso 1 n₀ n₁ ⋯).hom)
        (n₁ + 1) ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₁ n₁ ≫ 𝟙 (((HomologicalComplex.homologyFunctor C (up ℤ) 0).shift n₁).obj S.X₁) =
    S.X₁.liftCycles (-a) (n₁ + 1) ⋯ ⋯ ≫ S.X₁.homologyπ n₁
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = (shiftFunctorZero C B).inv.app X ≫ (shiftFunctorZero C B).hom.app X

Tactic:
Iso.inv_hom_id_app

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = (shiftFunctorZero' C (φ 0) ⋯).inv.app X ≫ (shiftFunctorZero' C (φ 0) ⋯).hom.app X

Tactic:
Iso.inv_hom_id_app

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map
              ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X ≫ (shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫
            (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
              ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
Iso.inv_hom_id_app

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          (shiftFunctor Cᵒᵖ a₂).map (𝟙 ((shiftFunctor C b₁).op.obj X)) ≫
            (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
              ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X : Cᵒᵖ
⊢ (shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((shiftFunctor C (-n)).obj (Opposite.unop X)) ≫
      (shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X)) =
    𝟙 ((𝟭 C).obj ((shiftFunctor C (-n)).obj (Opposite.unop X)))

Tactic:
Iso.inv_hom_id_app

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X : Cᵒᵖ
⊢ 𝟙 ((𝟭 C).obj ((shiftFunctor C (-n)).obj (Opposite.unop X))) =
    𝟙 ((𝟭 C).obj ((shiftFunctor C (-n)).obj (Opposite.unop X)))