mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ {
        X₁ :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨0, ⋯⟩,
        X₂ :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨1, ⋯⟩,
        X₃ :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨2, ⋯⟩,
        f :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
            0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
        g :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
            1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
        zero := ⋯ }.f =
    0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
            ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
        0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
            ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
        1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ {
        X₁ :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨0, ⋯⟩,
        X₂ :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨1, ⋯⟩,
        X₃ :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
            ⟨2, ⋯⟩,
        f :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
            0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
        g :=
          (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
                ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
            1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
        zero := ⋯ }.f =
    0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ShortComplex C
φ : R₁ ⟶ R₂
hR₂ : R₂.Exact
hR₁' : Epi R₁.g
h₀ : Epi φ.τ₁
h₁ : Mono φ.τ₂
⊢ R₁.toComposableArrows.map' 0 2 Abelian.mono_of_epi_of_mono_of_mono'._proof_2
      Abelian.mono_of_epi_of_epi_mono'._proof_1 =
    0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ShortComplex C
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂' : Mono R₂.f
h₀ : Epi φ.τ₂
h₁ : Mono φ.τ₃
⊢ R₂.toComposableArrows.map' 0 2 Abelian.mono_of_epi_of_mono_of_mono'._proof_2
      Abelian.mono_of_epi_of_epi_mono'._proof_1 =
    0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : (Triangle C)ᵒᵖ
⊢ (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
          (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
            (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).mor₁ ≫
      (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₂).hom =
    (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₁).hom ≫
      (Opposite.unop T).mor₁

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
a : A
X✝ : C
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    (shiftFunctor C a).map (adj.unit.app X✝) ≫
      (shiftFunctorCompIsoId C (-a) a ⋯).inv.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        (shiftFunctorCompIsoId C (-a) a ⋯).hom.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
          (𝟭 C).map ((Functor.commShiftIso G a).inv.app (F.obj X✝)) ≫ (Functor.commShiftIso G a).hom.app (F.obj X✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : (Triangle C)ᵒᵖ
⊢ (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
          (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
            (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).mor₂ ≫
      (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₃).hom =
    (Iso.refl
          (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
              (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₂).hom ≫
      (Opposite.unop T).mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ (contractibleTriangle X).mor₁ ≫ (Iso.refl (contractibleTriangle X).obj₂).hom =
    (Iso.refl (contractibleTriangle X).obj₁).hom ≫
      ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ (contractibleTriangle X).mor₂ ≫ (⋯.iso ⋯).hom =
    (Iso.refl (contractibleTriangle X).obj₂).hom ≫
      ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : Cᵒᵖ
⊢ (contractibleTriangle X).mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map (Iso.refl (contractibleTriangle X).obj₁).hom =
    (⋯.iso ⋯).hom ≫
      ((triangleOpEquivalence C).functor.obj (Opposite.op (contractibleTriangle (Opposite.unop X)).invRotate)).mor₃

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.mor₁ ≫
      (Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₂).hom =
    (Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₁).hom ≫
      (Opposite.unop ((triangleOpEquivalence C).inverse.obj T)).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ ((Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.mor₂ ≫
        (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop).hom).op =
    ((Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₂).hom ≫
        (Opposite.unop ((triangleOpEquivalence C).inverse.obj T)).mor₂).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.mor₃ ≫
      (shiftFunctor C 1).map
        (Iso.refl (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate.obj₁).hom =
    (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop).hom ≫
      (Opposite.unop ((triangleOpEquivalence C).inverse.obj T)).mor₃

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).Exact

Tactic:
ShortComplex.ab_exact_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).f) x₁ = x₂
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).Exact

Tactic:
ShortComplex.ab_exact_iff

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
B : C
T : Triangle Cᵒᵖ
hT : T ∈ distinguishedTriangles
⊢ ∀ (x₂ : ↑((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).X₂),
    (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).g) x₂ = 0 →
      ∃ x₁, (ConcreteCategory.hom ((shortComplexOfDistTriangle T hT).map (preadditiveYoneda.obj B)).f) x₁ = x₂
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₁ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ (Opposite.unop
          ((triangleOpEquivalence C).inverse.obj
            (Triangle.mk f g.op
              ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₁ ≫
      (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₂).hom =
    (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₁).hom ≫
      (Triangle.mk g f.unop h).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₂ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ (Opposite.unop
          ((triangleOpEquivalence C).inverse.obj
            (Triangle.mk f g.op
              ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₂ ≫
      (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₃).hom =
    (Iso.refl
          (Opposite.unop
              ((triangleOpEquivalence C).inverse.obj
                (Triangle.mk f g.op
                  ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                    (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₂).hom ≫
      (Triangle.mk g f.unop h).mor₂

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
a : ℤ
⊢ NatIso.ofComponents
      (fun A ↦
        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' 0 a a ⋯).symm;
          { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
      ⋯ =
    Functor.isoWhiskerRight (shiftFunctorZero Cᵒᵖ ℤ) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
      (preadditiveYoneda.obj ((shiftFunctor C a).obj B)).leftUnitor

Tactic:
by ext; apply ShiftedHom.opEquiv'_zero_add_symm

Goal state after:
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 φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝⁶ : Category.{v_2, u_4} D
inst✝⁵ : HasShift D B
F : C ⥤ D
inst✝⁴ : F.CommShift B
G✝ : C ⥤ D
inst✝³ : G✝.CommShift B
E : Type u_5
inst✝² : Category.{v_3, u_5} E
inst✝¹ : HasShift E B
G : D ⥤ E
inst✝ : G.CommShift B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ G.map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      G.map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app (F.obj x✝) ≫ (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj (F.obj x✝)) =
    G.map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      G.map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        (G.map (𝟙 ((shiftFunctor D (φ x✝¹)).obj (F.obj x✝))) ≫ (commShiftIso G (φ x✝¹)).hom.app (F.obj x✝)) ≫
          (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj (F.obj x✝))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (shiftFunctor C 1).map T₂.mor₃.unop ≫ (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ (shiftFunctor C 1).map ((shiftFunctor Cᵒᵖ 1).map a).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop =
    (((shiftFunctor C 1).map
              ((shiftFunctor Cᵒᵖ 1).map (a ≫ (opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁)).unop).op ≫
          (opShiftFunctorEquivalence C 1).unitIso.inv.app
            (Opposite.op ((shiftFunctor C 1).obj (Opposite.unop ((shiftFunctor Cᵒᵖ 1).obj T₂.obj₁))))).unop ≫
      (shiftFunctor C 1).map T₁.mor₃.unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.hom ≫ (↑z * ↑z⁻¹).app Y ≫ e.inv = 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Center.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
z : (CatCenter C)ˣ
e : X ≅ Y
⊢ e.inv ≫ (↑z⁻¹ * ↑z).app X ≫ e.hom = 𝟙 Y

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ (localization 1 L W).app (L.obj X) = app 1 (L.obj X)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
r s : CatCenter C
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ ((r * s).localization L W).app (L.obj X) = (r.localization L W * s.localization L W).app (L.obj X)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : L.Additive
X : C
⊢ (localization 0 L W).app (L.obj X) = app 0 (L.obj X)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
r s : CatCenter C
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : L.Additive
⊢ ∀ (X : C), ((r + s).localization L W).app (L.obj X) = (r.localization L W + s.localization L W).app (L.obj X)

Tactic:
simp

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
⊢ (ComplexShape.up ℤ).next i = i + 1

Tactic:
simp

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
⊢ i < i + 1

Tactic:
simp

Goal state after: