mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Composition

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
⊢ (L₁ ⋙ L₂).IsLocalization W₃

Tactic:
let E₂ := Localization.uniq L₁ W₁.Q W₁
  let W₂' := W₂.map E₂.functor
  let Φ : LocalizerMorphism W₂ W₂' :=
    { functor := E₂.functor
      map := by
        have eq := W₂.isoClosure.inverseImage_map_eq_of_isEquivalence E₂.functor
        rw [MorphismProperty.map_isoClosure] at eq
        rw [eq]
        apply W₂.le_isoClosure }
  have := LocalizerMorphism.IsLocalizedEquivalence.of_equivalence Φ (by rfl)
  -- The fact that `Φ` is a localized equivalence allows to consider
  -- the induced equivalence of categories `E₃ : C₃ ≅ W₂'.Localization`, and
  -- the isomorphism `iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂`
  let E₃ := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
  let iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ := by
    calc
      _ ≅ L₁ ⋙ E₂.functor ⋙ W₂'.Q ⋙ E₃.inverse :=
          Functor.associator _ _ _ ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm _ ≪≫
            Functor.associator _ _ _
      _ ≅ L₁ ⋙ L₂ ⋙ E₃.functor ⋙ E₃.inverse :=
          isoWhiskerLeft _ ((Functor.associator _ _ _).symm ≪≫
            isoWhiskerRight (Φ.catCommSq L₂ W₂'.Q).iso E₃.inverse ≪≫ Functor.associator _ _ _)
      _ ≅ L₁ ⋙ L₂ := isoWhiskerLeft _ (isoWhiskerLeft _ E₃.unitIso.symm ≪≫ L₂.rightUnitor)
  -- In order to show `(W₁.Q ⋙ W₂'.Q).IsLocalization W₃`, we need
  -- to check the assumptions of `StrictUniversalPropertyFixedTarget.comp`
  have hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q) := by
    simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse,
      MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃
  have hW₂₃' : W₂' ≤ W₃.map W₁.Q := (MorphismProperty.monotone_map E₂.functor hW₂₃).trans
    (by simpa only [W₃.map_map]
      using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁)))
  have : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃ := by
    refine IsLocalization.mk' _ _ ?_ ?_
    all_goals
      exact (StrictUniversalPropertyFixedTarget.comp
        (strictUniversalPropertyFixedTargetQ W₁ _)
        (strictUniversalPropertyFixedTargetQ W₂' _) W₃ hW₃' hW₁₃ hW₂₃')
  -- Finally, the previous result can be transported via the equivalence `E₃`
  exact IsLocalization.of_equivalence_target _ W₃ _ E₃.symm iso

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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj (mappingCone.triangle u₁₂)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((quotient C (ComplexShape.up ℤ)).mapTriangle.map α).hom₁ =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₃ ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₁₂).obj₁

Tactic:
dsimp [α]

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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₃ ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app X₁) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((quotient C (ComplexShape.up ℤ)).map (𝟙 X₁)) =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₃ ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app X₁
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.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
exact c'.prev_eq' (by simpa only [e.rel_iff] using hij')

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 : 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
⊢ e.f i = i'

Tactic:
rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]

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 : 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
⊢ e.f i = i'

Tactic:
rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]

Goal state after:
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.restriction e).d j k = 0

Tactic:
by
      rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_comp]

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

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Tactic:
K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj,

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫
      (K.truncGE'XIsoOpcycles e hj' hj).hom ≫ K.fromOpcycles j' (e.f k) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    0
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.sc j).pOpcycles = (K.sc j).homologyData.right.p ≫ (K.sc j).homologyData.right.opcyclesIso.inv

Tactic:
ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv

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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles = (K.sc' (c.prev j) j (c.next j)).pOpcycles
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫
      opcyclesMap ((opFunctor C c').map φ.op) i' ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv =
    (L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫
      (L.opcyclesOpIso i').hom ≫
        (L.opcyclesOpIso i').inv ≫ opcyclesMap ((opFunctor C c').map φ.op) i' ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv

Tactic:
Iso.hom_inv_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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫
      opcyclesMap ((opFunctor C c').map φ.op) i' ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv =
    (L.op.truncGE'XIsoOpcycles e.op h ⋯).hom ≫
      opcyclesMap ((opFunctor C c').map φ.op) i' ≫ (K.op.truncGE'XIsoOpcycles e.op h ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ⋯.δ (e.f i) j' hj', zero := ⋯ }.f =
    0

Tactic:
rw [← cancel_epi (homologyMap (K.ιTruncLE e) (e.f i)), comp_zero]

Goal state after:
case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap (K.ιTruncLE e) (e.f i) ≫
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ⋯.δ (e.f i) j' hj', zero := ⋯ }.f =
    0
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case inl
ι : 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✝² : Abelian C
K : HomologicalComplex C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst✝¹ : e₁.IsTruncLE
inst✝ : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₁ : ι₁
⊢ QuasiIsoAt (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)

Tactic:
have h₁ := ((ac.isSupportedOutside₁_iff (K.truncGE e₂)).2 inferInstance).exactAt i₁

Goal state after:
case inl
ι : 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✝² : Abelian C
K : HomologicalComplex C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst✝¹ : e₁.IsTruncLE
inst✝ : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₁ : ι₁
h₁ : (K.truncGE e₂).ExactAt (e₁.f i₁)
⊢ QuasiIsoAt (K.shortComplexTruncLEX₃ToTruncGE ac) (e₁.f i₁)
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjHomologySelfIso c j A).inv ≫ ((single C c j).obj A).homologyι j = (singleObjOpcyclesSelfIso c j A).hom

Tactic:
← cancel_epi (singleObjCyclesSelfIso c j A).hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjHomologySelfIso c j A).inv ≫ ((single C c j).obj A).homologyι j =
    (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j = f ≫ (singleObjCyclesSelfIso c j B).inv

Tactic:
← cancel_epi (singleObjCyclesSelfIso c j A).hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j = f ≫ (singleObjOpcyclesSelfIso c j B).hom

Tactic:
← cancel_epi (singleObjCyclesSelfIso c j A).hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjOpcyclesSelfIso c j B).hom
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'
⊢ ((Functor.commShiftIso L n).hom.app X ≫
        (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
          (shiftFunctor D n).map ((Functor.commShiftIso L a).hom.app Y) ≫
            (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (Functor.commShiftIso L a').inv.app Y) ≫
      (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)

Tactic:
simp only [Functor.comp_obj, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]

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'
⊢ (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((Functor.commShiftIso L a).hom.app Y) ≫
          (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((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
inst✝¹ : HasSmallLocalizedShiftedHom W M Y X
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
hf' : W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f)
⊢ (isoOfHom L W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) hf').hom ≫
      (isoOfHom L W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) hf').inv ≫ ((Functor.commShiftIso L m₀).app X).hom =
    (isoOfHom L W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) hf').hom ≫ ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv

Tactic:
Iso.hom_inv_id_assoc

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✝¹ : HasSmallLocalizedShiftedHom W M Y X
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
hf' : W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f)
⊢ ((Functor.commShiftIso L m₀).app X).hom =
    (isoOfHom L W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) hf').hom ≫ ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
this✝ : Mono S.f
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ (𝟙 (S.X₁.homology j) ≫ HomologicalComplex.homologyMap S.f j) ≫ HomologicalComplex.homologyMap S.g j =
    (0 ≫ HomologicalComplex.homologyMap S.f j) ≫ HomologicalComplex.homologyMap S.g j

Tactic:
simp [← HomologicalComplex.homologyMap_comp]

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

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this✝ : Epi S.g
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i ≫ 𝟙 (S.X₃.homology i) =
    HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i ≫ 0

Tactic:
simp [← HomologicalComplex.homologyMap_comp]

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

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
⊢ NatIso.removeOp (commShiftIso (OppositeShift.functor A F) 0).symm = CommShift.isoZero F A

Tactic:
by
    rw [commShiftIso_zero]
    ext
    simp only [NatIso.removeOp_hom, Iso.symm_hom, NatTrans.removeOp_app,
      CommShift.isoZero_inv_app, unop_comp, CommShift.isoZero_hom_app]
    erw [oppositeShiftFunctorZero_hom_app, oppositeShiftFunctorZero_inv_app]
    rfl

Goal state after:
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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C p).map ((shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op

Tactic:
erw [Functor.map_id, Functor.map_id, Functor.map_id, Functor.map_id,
    id_comp, id_comp, id_comp, comp_id, comp_id]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctor C p).map
              ((𝟙 ((shiftFunctor C (-m)).obj (Opposite.unop ((shiftFunctor C (-n)).op.obj X)))).op ≫
                  ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op).unop).op
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ᵒᵖ
n m : ℤ
hnm : autoParam (n + m = 0) shiftFunctorCompIsoId_op_inv_app._auto_1
⊢ m + n = 0

Tactic:
omega

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := ⋯
α : K.X i ⟶ P := ⋯
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ (mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯ ≫ π).f i = (𝟙 ((singleFunctor C i).obj P)).f i

Tactic:
comp_f,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ (mkHomFromSingle (Projective.factorThru (𝟙 P) α) ⋯).f i ≫ π.f i = (𝟙 ((singleFunctor C i).obj P)).f i