mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
⊢ (w ≫ₕ w'.hom).GuitartExact ↔ w.GuitartExact

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
E : C₂ ≌ C₃
E' : D₂ ≌ D₃
w' : E.functor ⋙ V₃ ≅ V₂ ⋙ E'.functor
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ E.functor ≅ T₁₂
eB : B₁ ⋙ E'.functor ≅ B₁₂
⊢ (w.hComp' w'.hom eT eB).GuitartExact ↔ w.GuitartExact

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
  (B.functor ⋙ R.inv.functor).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor.asEquivalence.counitIso.symm (B.functor ⋙ R.inv.functor) ≪≫
      L.functor.asEquivalence.inverse.associator L.functor.asEquivalence.functor (B.functor ⋙ R.inv.functor) ≪≫
        L.functor.asEquivalence.inverse.isoWhiskerLeft
            (L.functor.asEquivalence.functor.associator B.functor R.inv.functor).symm ≪≫
          L.functor.asEquivalence.inverse.isoWhiskerLeft (isoWhiskerRight iso.symm R.inv.functor) ≪≫
            L.functor.asEquivalence.inverse.isoWhiskerLeft (T.functor.associator R.functor R.inv.functor) ≪≫
              L.functor.asEquivalence.inverse.isoWhiskerLeft
                  (T.functor.isoWhiskerLeft R.functor.asEquivalence.unitIso.symm) ≪≫
                (L.functor.asEquivalence.inverse.associator T.functor (𝟭 C₂)).symm ≪≫
                  (L.functor.asEquivalence.inverse ⋙ T.functor).rightUnitor
⊢ W₁.RespectsIso

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
  (B.functor ⋙ R.inv.functor).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor.asEquivalence.counitIso.symm (B.functor ⋙ R.inv.functor) ≪≫
      L.functor.asEquivalence.inverse.associator L.functor.asEquivalence.functor (B.functor ⋙ R.inv.functor) ≪≫
        L.functor.asEquivalence.inverse.isoWhiskerLeft
            (L.functor.asEquivalence.functor.associator B.functor R.inv.functor).symm ≪≫
          L.functor.asEquivalence.inverse.isoWhiskerLeft (isoWhiskerRight iso.symm R.inv.functor) ≪≫
            L.functor.asEquivalence.inverse.isoWhiskerLeft (T.functor.associator R.functor R.inv.functor) ≪≫
              L.functor.asEquivalence.inverse.isoWhiskerLeft
                  (T.functor.isoWhiskerLeft R.functor.asEquivalence.unitIso.symm) ≪≫
                (L.functor.asEquivalence.inverse.associator T.functor (𝟭 C₂)).symm ≪≫
                  (L.functor.asEquivalence.inverse ⋙ T.functor).rightUnitor
this : W₁.RespectsIso
⊢ W₂.RespectsIso

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
⊢ T.IsLeftDerivabilityStructure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
⊢ T.IsRightDerivabilityStructure ↔ B.IsRightDerivabilityStructure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁰ : Category.{v_1, u_1} C₁
inst✝⁹ : Category.{v_2, u_2} C₂
inst✝⁸ : Category.{v_3, u_3} D₁
inst✝⁷ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁶ : W₁'.RespectsIso
inst✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsInduced
inst✝³ : L.functor.IsEquivalence
inst✝² : R.IsInduced
inst✝¹ : R.functor.IsEquivalence
inst✝ : T.IsRightDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
⊢ B.IsRightDerivabilityStructure

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ F.mapDerivedCategoryFactors.hom =
    whiskerRight (DerivedCategory.quotientCompQhIso C₁).inv F.mapDerivedCategory ≫
      ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).associator DerivedCategory.Qh F.mapDerivedCategory).hom ≫
        (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).whiskerLeft F.mapDerivedCategoryFactorsh.hom ≫
          ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).associator (F.mapHomotopyCategory (ComplexShape.up ℤ))
                DerivedCategory.Qh).inv ≫
            whiskerRight (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom DerivedCategory.Qh ≫
              ((F.mapHomologicalComplex (ComplexShape.up ℤ)).associator
                    (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh).hom ≫
                (F.mapHomologicalComplex (ComplexShape.up ℤ)).whiskerLeft (DerivedCategory.quotientCompQhIso C₂).hom

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝¹² : Category.{v₁, u₁} C₁
inst✝¹¹ : Abelian C₁
inst✝¹⁰ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Abelian C₂
inst✝⁷ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝⁶ : F.Additive
inst✝⁵ : PreservesFiniteLimits F
inst✝⁴ : PreservesFiniteColimits F
R : Type u_1
inst✝³ : Ring R
inst✝² : CategoryTheory.Linear R C₁
inst✝¹ : CategoryTheory.Linear R C₂
inst✝ : Linear R F
⊢ Linear R F.mapDerivedCategory

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
X : C₁
⊢ F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X) ≫
      (F.mapDerivedCategorySingleFunctor 0).hom.app X =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
X : C₁
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app X ≫
      F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X) =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Q.obj K ≅ (singleFunctor C a).obj X
Y : C
eY : Q.obj L ≅ (singleFunctor C b).obj Y
p q : ℤ
φ : (shiftFunctor (DerivedCategory C) p).obj (Q.obj K) ⟶ (shiftFunctor (DerivedCategory C) q).obj (Q.obj L)
⊢ p + (a - p) = a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Q.obj K ≅ (singleFunctor C a).obj X
Y : C
eY : Q.obj L ≅ (singleFunctor C b).obj Y
p q : ℤ
φ : (shiftFunctor (DerivedCategory C) p).obj (Q.obj K) ⟶ (shiftFunctor (DerivedCategory C) q).obj (Q.obj L)
⊢ q + (b - q) = b

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Q.obj K ≅ (singleFunctor C a).obj X
Y : C
eY : Q.obj L ≅ (singleFunctor C b).obj Y
p q : ℤ
φ₁ φ₂ : (shiftFunctor (DerivedCategory C) p).obj (Q.obj K) ⟶ (shiftFunctor (DerivedCategory C) q).obj (Q.obj L)
h :
  (fun φ ↦
        ((singleFunctors C).shiftIso p (a - p) a ⋯).inv.app X ≫
          (shiftFunctor (DerivedCategory C) p).map eX.inv ≫
            φ ≫ (shiftFunctor (DerivedCategory C) q).map eY.hom ≫ ((singleFunctors C).shiftIso q (b - q) b ⋯).hom.app Y)
      φ₁ =
    (fun φ ↦
        ((singleFunctors C).shiftIso p (a - p) a ⋯).inv.app X ≫
          (shiftFunctor (DerivedCategory C) p).map eX.inv ≫
            φ ≫ (shiftFunctor (DerivedCategory C) q).map eY.hom ≫ ((singleFunctors C).shiftIso q (b - q) b ⋯).hom.app Y)
      φ₂
⊢ φ₁ = φ₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K : CochainComplex (InjectiveObject C) ℤ
n✝ : ℤ
hn : K.IsStrictlyGE n✝
L : HomologicalComplex C (ComplexShape.up ℤ) := ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K
n : ℤ
⊢ Injective (L.X n)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K : Plus (InjectiveObject C)
⊢ IsKInjective (((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K.obj)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
L : CochainComplex C ℤ
i : K.obj ⟶ L
w✝¹ : QuasiIso i
w✝ : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE n
L' : CochainComplex (InjectiveObject C) ℤ := HomologicalComplex.liftObjectProperty (isInjective C) L ⋯
⊢ L'.IsStrictlyGE n

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
L : CochainComplex C ℤ
i : K.obj ⟶ L
w✝¹ : QuasiIso i
w✝ : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE n
L' : CochainComplex (InjectiveObject C) ℤ := HomologicalComplex.liftObjectProperty (isInjective C) L ⋯
hL' : L'.IsStrictlyGE n
⊢ quasiIso C (ObjectProperty.homMk i)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), ∃ i, quasiIso C i

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
⊢ K.IsGE n

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
this : K.obj.IsGE n
L : CochainComplex C ℤ
w✝¹ : L.IsStrictlyGE n
e : K.obj ≅ DerivedCategory.Q.obj L
M : CochainComplex.Plus (InjectiveObject C)
w✝ : M.obj.IsStrictlyGE n
i : { obj := L, property := ⋯ } ⟶ (InjectiveObject.ι C).mapCochainComplexPlus.obj M
hi : CochainComplex.Plus.quasiIso C i
⊢ QuasiIso i.hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.IsGE n
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), Nonempty (Q.obj ((InjectiveObject.ι C).mapCochainComplexPlus.obj L) ≅ K)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
⊢ (quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus ≤
    (quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : FibrantObject (Plus C)
n : ℤ
⊢ Injective (K.obj.obj.X n)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : Plus (InjectiveObject C)
⊢ fibrantObjects (Plus C) ((InjectiveObject.ι C).mapCochainComplexPlus.obj K)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : FibrantObject (Plus C)
n : ℤ
⊢ isInjective C (((FibrantObject.ι ⋙ ι C).obj K).X n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K₁ K₂ : CochainComplex C ℤ
e : HomotopyEquiv K₁ K₂
inst✝ : K₁.IsKProjective
L : CochainComplex C ℤ
f : K₂ ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ f = 𝟙 K₂ ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
⊢ ∀ (X : FibrantObject (Plus C)),
    CochainComplex.plus (InjectiveObject C)
      ((HomologicalComplex.liftFunctorObjectProperty (isInjective C) (FibrantObject.ι ⋙ ι C) ⋯).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K₁ K₂ : CochainComplex C ℤ
e : HomotopyEquiv K₁ K₂
inst✝ : K₁.IsKProjective
L : CochainComplex C ℤ
f : K₂ ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ (e.inv ≫ e.hom) ≫ f = e.inv ≫ e.hom ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
⊢ (quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus ≤
    (weakEquivalences (FibrantObject (Plus C))).inverseImage (fibrantObjectEquivalence C).functor

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K₁ K₂ : CochainComplex C ℤ
e : HomotopyEquiv K₁ K₂
inst✝ : K₁.IsKProjective
L : CochainComplex C ℤ
f : K₂ ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ e.inv ≫ 0 = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
⊢ (localizerMorphism C).IsRightDerivabilityStructure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
hS : S.ShortExact
⊢ (ConcreteCategory.hom
          { X₁ := AddCommGrpCat.of (Ext (S.map F).X₂ (F.obj Y) n),
              X₂ := AddCommGrpCat.of (Ext (S.map F).X₁ (F.obj Y) n),
              X₃ := AddCommGrpCat.of (Ext (S.map F).X₃ (F.obj Y) (n + 1)),
              f := AddCommGrpCat.ofHom ((Ext.mk₀ (S.map F).f).precomp (F.obj Y) ⋯),
              g := AddCommGrpCat.ofHom (⋯.extClass.precomp (F.obj Y) ⋯), zero := ⋯ }.f).comp
      (F.mapExtAddHom S.X₂ Y n) =
    (F.mapExtAddHom S.X₁ Y n).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₃ Y (n + 1)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp Y ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.precomp Y ⋯), zero := ⋯ }.f)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
⊢ (localizerMorphism C).arrow.HasRightResolutions

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
hS : S.ShortExact
⊢ (ConcreteCategory.hom
          { X₁ := AddCommGrpCat.of (Ext (S.map F).X₂ (F.obj Y) n),
              X₂ := AddCommGrpCat.of (Ext (S.map F).X₁ (F.obj Y) n),
              X₃ := AddCommGrpCat.of (Ext (S.map F).X₃ (F.obj Y) (n + 1)),
              f := AddCommGrpCat.ofHom ((Ext.mk₀ (S.map F).f).precomp (F.obj Y) ⋯),
              g := AddCommGrpCat.ofHom (⋯.extClass.precomp (F.obj Y) ⋯), zero := ⋯ }.g).comp
      (F.mapExtAddHom S.X₁ Y n) =
    (F.mapExtAddHom S.X₃ Y (n + 1)).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n),
            X₃ := AddCommGrpCat.of (Ext S.X₃ Y (n + 1)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp Y ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.precomp Y ⋯), zero := ⋯ }.g)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K L : Plus (InjectiveObject C)
f : K ⟶ L
hf : IsIso f
⊢ (quasiIso C).inverseImage (InjectiveObject.ι C).mapHomotopyCategoryPlus f

Tactic:
by

Goal state after: