mathlib-initiative/mathlib-tactics huggingface dataset:
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
n a a' : ℤ
h : n + a = a'
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).map f ≫
        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' h).symm;
            { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso.hom =
      (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' h).symm;
            { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso.hom ≫
        (preadditiveYoneda.obj ((shiftFunctor C a').obj B)).map f

Tactic:
by

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

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ᵒᵖ
⊢ (inverse C ⋙ functor C).obj T ≅ (𝟭 (Triangle Cᵒᵖ)).obj T

Tactic:
by

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
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ NatIso.ofComponents
      (fun A ↦
        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm;
          { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
      ⋯ =
    Functor.isoWhiskerRight (shiftFunctorAdd Cᵒᵖ m n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
      (shiftFunctor Cᵒᵖ m).associator (shiftFunctor Cᵒᵖ n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
        (shiftFunctor Cᵒᵖ m).isoWhiskerLeft
            (NatIso.ofComponents
              (fun A ↦
                (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' ha').symm;
                  { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
              ⋯) ≪≫
          NatIso.ofComponents
            (fun A ↦
              (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' m a' a'' ha'').symm;
                { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
            ⋯

Tactic:
by

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₃ ≫
        (shiftFunctor C 1).map
          (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).op =
    ((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₃).op

Tactic:
by

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 ℤ
⊢ ∀ {X Y : Triangle Cᵒᵖ} (f : X ⟶ Y),
    (inverse C ⋙ functor C).map f ≫
        (((inverse C ⋙ functor C).obj Y).isoMk ((𝟭 (Triangle Cᵒᵖ)).obj Y)
            (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₁) (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₂)
            (Iso.refl ((inverse C ⋙ functor C).obj Y).obj₃) ⋯ ⋯ ⋯).hom =
      (((inverse C ⋙ functor C).obj X).isoMk ((𝟭 (Triangle Cᵒᵖ)).obj X) (Iso.refl ((inverse C ⋙ functor C).obj X).obj₁)
            (Iso.refl ((inverse C ⋙ functor C).obj X).obj₂) (Iso.refl ((inverse C ⋙ functor C).obj X).obj₃) ⋯ ⋯ ⋯).hom ≫
        (𝟭 (Triangle Cᵒᵖ)).map f

Tactic:
by

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 g h, Triangle.mk f g h ∈ distinguishedTriangles C

Tactic:
by

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
⊢ (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x✝).hom ≫
      whiskerRight (PullbackShift.natIsoComp φ F G).hom (shiftFunctor (PullbackShift E φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natIsoComp φ F G).hom ≫
      (commShiftIso (PullbackShift.functor φ F ⋙ PullbackShift.functor φ G) x✝).hom

Tactic:
by

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
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ (shiftFunctor C a).obj B
⊢ (ConcreteCategory.hom ((preadditiveYoneda.obj B).shiftMap f a a' h)) z = ((ShiftedHom.opEquiv n).symm f).comp z ⋯

Tactic:
by

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : PullbackShift C φ
⊢ (functor φ F).map
        (((NatTrans.PullbackShift.natIsoId C φ).hom ≫
              natTrans φ adj.unit ≫ (NatTrans.PullbackShift.natIsoComp φ F G).hom).app
          x✝) ≫
      ((NatTrans.PullbackShift.natIsoComp φ G F).inv ≫
            natTrans φ adj.counit ≫ (NatTrans.PullbackShift.natIsoId D φ).inv).app
        ((functor φ F).obj x✝) =
    𝟙 ((functor φ F).obj x✝)

Tactic:
by

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : PullbackShift D φ
⊢ ((NatTrans.PullbackShift.natIsoId C φ).hom ≫ natTrans φ adj.unit ≫ (NatTrans.PullbackShift.natIsoComp φ F G).hom).app
        ((functor φ G).obj x✝) ≫
      (functor φ G).map
        (((NatTrans.PullbackShift.natIsoComp φ G F).inv ≫
              natTrans φ adj.counit ≫ (NatTrans.PullbackShift.natIsoId D φ).inv).app
          x✝) =
    𝟙 ((functor φ G).obj x✝)

Tactic:
by

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 : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.CommShift B
inst✝ : adj.CommShift B
⊢ NatTrans.CommShift (PullbackShift.adjunction φ adj).unit A

Tactic:
by

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 : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.CommShift B
inst✝ : adj.CommShift B
⊢ NatTrans.CommShift (PullbackShift.adjunction φ adj).counit A

Tactic:
by

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
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ (ConcreteCategory.hom
        ((preadditiveYoneda.obj B).homologySequenceδ ((triangleOpEquivalence C).functor.obj (op T)) n₀ n₁ h))
      x =
    T.mor₃ ≫ (shiftFunctor C 1).map x ≫ (shiftFunctorAdd' C n₀ 1 n₁ h).inv.app B

Tactic:
by

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₁ : T₁ ∈ distinguishedTriangles C
hT₂ : T₂ ∈ distinguishedTriangles C
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃

Tactic:
by

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ᵒᵖ
⊢ T ∈ distinguishedTriangles ↔ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ distinguishedTriangles

Tactic:
by

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
hT : T ∈ distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (Opposite.op T) ∈ distinguishedTriangles

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
X : C
⊢ (x * y).app X = x.app X ≫ y.app X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : CatCenter C
⊢ x * y = y * x

Tactic:
by

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
⊢ (↑z • e.hom) ≫ (↑z⁻¹ • e.inv) = 𝟙 X

Tactic:
by

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
⊢ (↑z⁻¹ • e.inv) ≫ (↑z • e.hom) = 𝟙 Y

Tactic:
by

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 : CatCenter C
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ (r.localization L W).app (L.obj X) = L.map (r.app X)

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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:
by

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:
by

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 := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
⊢ π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv

Tactic:
by

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

Tactic:
by

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 := 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
⊢ ∀ (k : ℤ), (ComplexShape.up ℤ).Rel i k → Projective.factorThru (𝟙 P) α ≫ K.d i k = 0

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
⊢ { app := fun X ↦ 1 • 𝟙 X, naturality := ⋯ } = 1

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a * b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ a • 𝟙 X, naturality := ⋯ } * { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
⊢ { app := fun X ↦ 0 • 𝟙 X, naturality := ⋯ } = 0

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a + b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ a • 𝟙 X, naturality := ⋯ } + { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }

Tactic:
ext X; simp [add_smul]

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

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
⊢ { app := fun X ↦ (a + b) • 𝟙 X, naturality := ⋯ } =
    { app := fun X ↦ a • 𝟙 X, naturality := ⋯ } + { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
a : R
f : X ⟶ Y
⊢ a • f = f ≫ (φ a).app Y

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a b : R
f : X ⟶ Y
⊢ (a * b) • f = a • b • f

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : X ⟶ Y
⊢ 1 • a = a

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : R
⊢ a • 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : R
b : X ⟶ Y
⊢ ∀ (y : X ⟶ Y), a • (b + y) = a • b + a • y

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a b : R
f : X ⟶ Y
⊢ (a + b) • f = a • f + b • f

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
this : SMul R (X ⟶ Y) := smulOfRingMorphism φ X Y
a : X ⟶ Y
⊢ 0 • a = 0

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
⊢ Module R (X ⟶ Y)

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X✝ Y✝ : C
this : (X Y : C) → Module R (X ⟶ Y) := homModuleOfRingMorphism φ
X Y Z : C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : HasDerivedCategory C
X Y Z : C
n : ℕ
x : Ext X Y n
f : Y ⟶ Z
⊢ x.hom ≫ (shiftFunctor (DerivedCategory C) ↑n).map ((singleFunctor C 0).map f) = (x.comp (mk₀ f) ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X✝ : C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ ↑n₀ + 1 = ↑n₁

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
⊢ Functor.Linear R L

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X✝ Y✝ : C
this : (X Y : C) → Module R (X ⟶ Y) := homModuleOfRingMorphism φ
X Y Z : C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
φ : R →+* CatCenter C
X Y : C
⊢ Linear R C

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹³ : Ring R
C : Type u_4
inst✝¹² : Category.{v_1, u_4} C
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Linear R C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : Linear R D
M : Type u_3
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : ∀ (n : M), Functor.Linear R (shiftFunctor C n)
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
inst✝² : Functor.Linear R L
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
⊢ Functor.Linear R (shiftFunctor D n)

Tactic:
by

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 := 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) α) ⋯ ≫ π = 𝟙 ((singleFunctor C i).obj P)

Tactic:
by

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
⊢ IsSplitEpi π

Tactic:
by

Goal state after: