mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
⊢ G.kernel.isoModSerre = (isomorphisms C).inverseImage G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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
inst✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.kernel.isoModSerre = ObjectProperty.isLocal fun x ↦ x ∈ Set.range F.obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
α : Ext X Y n
m : ℕ
hm : n + 1 = m
⊢ ∃ f, ∃ (hf : R.complex.d m n ≫ f = 0), R.extMk f m hm hf = α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
⊢ R.complex.d m n ≫ f ≫ g = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

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
inst✝⁵ : Abelian C
inst✝⁴ : Abelian D
G : D ⥤ C
inst✝³ : PreservesFiniteLimits G
inst✝² : PreservesFiniteColimits G
F : C ⥤ D
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ G.IsLocalization G.kernel.isoModSerre

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
      (J.isoRightDerivedObj F n).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero ((InjectiveResolution.self X).cocomplex.X (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero ((F.rightDerived (n + 1)).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (F.rightDerived n).map f ≫ (Q.isoRightDerivedObj F n).hom =
    ((P.isoRightDerivedObj F n).hom ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
            g ≫
          (Q.isoRightDerivedObj F n).inv) ≫
      (Q.isoRightDerivedObj F n).hom

Tactic:
InjectiveResolution.isoRightDerivedObj_hom_naturality f P Q g _ F n,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (P.isoRightDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map g =
    ((P.isoRightDerivedObj F n).hom ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
            g ≫
          (Q.isoRightDerivedObj F n).inv) ≫
      (Q.isoRightDerivedObj F n).hom

C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ P.ι.f 0 ≫ g.f 0 = f ≫ Q.ι.f 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ R.cochainComplex.d (-↑m) (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ 0 + ↑n + 0 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ (F.rightDerived n).map f =
    (P.isoRightDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map g ≫
        (Q.isoRightDerivedObj F n).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ 0 + 0 + ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
h : PseudoEqual G x y
⊢ (ModuleCat.Hom.hom x.hom).range = (ModuleCat.Hom.hom y.hom).range

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
⊢ (R.extMk f m hm hf).comp (Ext.mk₀ g) ⋯ = R.extMk (f ≫ g) m hm ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
⊢ R'.complex.d m n ≫ φ.hom.f n ≫ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ -↑n = -↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ -↑m + 1 = -↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ R.cochainComplex.d (-↑m) (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
⊢ (NatTrans.rightDerivedToHomotopyCategory α).app X =
    (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (P.isoRightDerivedToHomotopyCategoryObj G).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯
            ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯
          ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              (Cocycle.toSingleMk (φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯

Tactic:
Cocycle.toSingleMk_precomp _ _ _ (by lia)
    (by simpa [R.cochainComplex_d _ _ _ _ rfl rfl]),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯
            ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯
          ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
      ((ShiftedHom.map
            (Cocycle.equivHomShift.symm
              ((Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯).precomp φ.hom'))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ rightDerived (𝟙 F) n = 𝟙 (F.rightDerived n)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Abelian C
inst✝⁴ : HasInjectiveResolutions C
inst✝³ : Abelian D
F G H : C ⥤ D
inst✝² : F.Additive
inst✝¹ : G.Additive
inst✝ : H.Additive
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ rightDerived (α ≫ β) n = rightDerived α n ≫ rightDerived β n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ ↑n + 0 + ↑0 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ 0 + ↑n + ↑0 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
n : ℕ
⊢ (NatTrans.rightDerived α n).app X =
    (P.isoRightDerivedObj F n).hom ≫
      (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫
        (P.isoRightDerivedObj G n).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ 0 + ↑n + 0 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ ↑n + 0 + 0 = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.ι.f 0) ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).d 0 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Abelian C
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ P.toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0 = F.map (P.ι.f 0)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
φ : P.cocomplex ⟶ Q.cocomplex
comm : P.ι.f 0 ≫ φ.f 0 = f ≫ Q.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map f ≫ Q.toRightDerivedZero' F =
    P.toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso ((self X).toRightDerivedZero' F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ kernel.ι f ≫ f = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q P' : ObjectProperty C
h : P ≤ P'
⊢ ofObjectProperty P Q ≤ ofObjectProperty P' Q

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
⊢ ofObjectProperty P Q ≤ ofObjectProperty P Q'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ X' s, ∃ (_ : P.epiModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : D ⥤ C
⊢ ofObjectProperty (P.inverseImage F) (Q.inverseImage F) = (ofObjectProperty P Q).inverseImage F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (injectiveResolution X).ι.f 0 ≫ (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X)).f 0 =
    f ≫ (injectiveResolution Y).ι.f 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
⊢ (ofObjectProperty P Q).map F ≤ ofObjectProperty (P.map F) (Q.map F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ X' s, ∃ (_ : P.isoModSerre s), s ≫ f = 0) ↔ P (Abelian.image f)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ ∀ {X Y Z : C} (i : X ⟶ Y), isomorphisms C i → ∀ (f : Y ⟶ Z), ofObjectProperty P Q f → ofObjectProperty P Q (i ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ F.map f ≫
      (injectiveResolution Y).toRightDerivedZero' F ≫
        (CochainComplex.isoHomologyπ₀
              ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex)).hom ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution Y).cocomplex) =
    ((injectiveResolution X).toRightDerivedZero' F ≫
        (CochainComplex.isoHomologyπ₀
              ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)).hom ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)) ≫
      (F.rightDerived 0).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ (injectiveResolution X).ι.f 0 ≫ (desc (𝟙 X) I (injectiveResolution X)).f 0 = 𝟙 X ≫ I.ι.f 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ ∀ {X Y Z : C} (i : Y ⟶ Z), isomorphisms C i → ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q (f ≫ i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ f ≫ cokernel.π f = 0

Tactic:
by

Goal state after: