mathlib-initiative/mathlib-tactics huggingface dataset:
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₂'.inverseImage R.functor).RespectsIso

Tactic:
infer_instance

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.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)

Tactic:
infer_instance

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 (K.X n).obj

Tactic:
infer_instance

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
n : ℤ
K : Plus C
hK✝ : fibrantObjects (Plus C) K
hK : ∀ (n : ℤ), Injective (K.obj.X n)
⊢ Injective ({ obj := K, property := hK✝ }.obj.obj.X n)

Tactic:
infer_instance

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:
obtain ⟨K, hK⟩ := K
  rw [fibrantObjects, modelCategoryQuillen.isFibrant_iff] at hK
  infer_instance

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)
n : ℤ
⊢ Injective (K.obj.X n).obj

Tactic:
infer_instance

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 (K.obj.obj.X n)

Tactic:
infer_instance

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
⊢ (FibrantObject.localizerMorphism (Plus C)).IsRightDerivabilityStructure

Tactic:
infer_instance

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
⊢ (FibrantObject.localizerMorphism (Plus C)).arrow.HasRightResolutions

Tactic:
infer_instance

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
n : ℤ
⊢ IsIso
    ((homologyFunctor C (ComplexShape.up ℤ) n).map ((ι C).map ((InjectiveObject.ι C).mapHomotopyCategoryPlus.map f)))

Tactic:
infer_instance

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
⊢ (quotient (InjectiveObject C)).IsLocalization
    ((HomologicalComplex.homotopyEquivalences (InjectiveObject C) (ComplexShape.up ℤ)).inverseImage
      (CochainComplex.Plus.ι (InjectiveObject C)))

Tactic:
infer_instance

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 : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
n : ℤ
⊢ Injective (op (K.X (-n)))

Tactic:
infer_instance

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

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
inst✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : EnoughInjectives C
⊢ ((F.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh).totalRightDerived DerivedCategory.Plus.Qh
        (HomotopyCategory.Plus.quasiIso C)).IsRightDerivedFunctor
    ((F.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh).totalRightDerivedUnit DerivedCategory.Plus.Qh
      (HomotopyCategory.Plus.quasiIso C))
    (HomotopyCategory.Plus.quasiIso C)

Tactic:
infer_instance

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

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
inst✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : EnoughInjectives C
X : HomotopyCategory.Plus (InjectiveObject C)
⊢ IsIso (F.rightDerivedFunctorPlusUnit.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj X))

Tactic:
infer_instance

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

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
inst✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : EnoughInjectives C
K : CochainComplex.Plus (InjectiveObject C)
⊢ IsIso
    (F.rightDerivedFunctorPlusUnit.app
      ((HomotopyCategory.Plus.quotient C).obj ((InjectiveObject.ι C).mapCochainComplexPlus.obj K)))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : K.IsKProjective
⊢ Function.Bijective toSmallShiftedHom

Tactic:
by
  let := HasDerivedCategory.standard C
  rw [← Function.Bijective.of_comp_iff'
      (SmallShiftedHom.equiv _ DerivedCategory.Q).bijective,
    ← Function.Bijective.of_comp_iff' (Iso.homCongr ((quotientCompQhIso C).symm.app K)
      ((Q.commShiftIso n).symm.app L ≪≫ (quotientCompQhIso C).symm.app (L⟦n⟧))).bijective]
  convert! (CochainComplex.IsKProjective.Qh_map_bijective _ _).comp (toHom_bijective K L n)
  ext x
  obtain ⟨x, rfl⟩ := x.mk_surjective
  simp [toHom_mk, ShiftedHom.map]

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
F : Plus C ⥤ H
inst✝² : HasDerivedCategory C
F' : DerivedCategory.Plus C ⥤ H
α : F ⟶ DerivedCategory.Plus.Qh ⋙ F'
inst✝¹ : F'.IsRightDerivedFunctor α (quasiIso C)
K : Plus C
inst✝ : ∀ (n : ℤ), Injective (K.obj.as.X n)
this : ∀ (Y : Plus (InjectiveObject C)), IsIso (α.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y))
Y : Plus (InjectiveObject C)
e : (InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y ≅ K
⊢ IsIso (α.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y))

Tactic:
infer_instance

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
F : Plus C ⥤ H
inst✝¹ : HasDerivedCategory C
F' : DerivedCategory.Plus C ⥤ H
α : F ⟶ DerivedCategory.Plus.Qh ⋙ F'
inst✝ : F'.IsRightDerivedFunctor α (quasiIso C)
X : Plus (InjectiveObject C)
⊢ IsIso
    ((F.totalRightDerivedUnit DerivedCategory.Plus.Qh (quasiIso C)).app
      ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj X))

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ ((K.restriction e).extend e).IsStrictlySupported e

Tactic:
infer_instance

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

Goal state before:
pp: case mpr.left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupported e

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀ = (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
by
  dsimp [mkHomFromDouble]
  rw [if_pos rfl, id_comp, comp_id]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFilteredColimitsOfSize.{w, w', v, u} C
J : Type w'
x✝¹ : Category.{w, w'} J
x✝ : IsFiltered J
⊢ HasColimitsOfShape J (HomologicalComplex C c)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝³ : HasZeroMorphisms C
inst✝² : HasFilteredColimitsOfSize.{w', w, v, u} C
inst✝¹ : HasFiniteLimits C
inst✝ : AB5OfSize.{w', w, v, u} C
J : Type w
x✝¹ : Category.{w', w} J
x✝ : IsFiltered J
⊢ HasExactColimitsOfShape J (HomologicalComplex C c)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
inst✝¹ : c.HasNoLoop
inst✝ : Small.{w, t} ι
this : HasCoproductsOfShape ι C
⊢ HasSeparator (HomologicalComplex C c)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso (𝟙 i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso g

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso f

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso (𝟙 k)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Transport

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A'
eA : A' ≌ A
eC : C' ≌ C
e : ι' ⋙ eA.functor ≅ eC.functor ⋙ ι
x✝ : A'
⊢ Epi
    (𝟙 (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
      eA.unitIso.hom.app (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
        𝟙 (eA.inverse.obj (eA.functor.obj (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
          𝟙 (eA.inverse.obj (eA.functor.obj (ι'.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
            eA.inverse.map (e.hom.app (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
              𝟙 (eA.inverse.obj (ι.obj (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
                eA.inverse.map (𝟙 (ι.obj (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
                  eA.inverse.map (ι.map (𝟙 (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))))) ≫
                    eA.inverse.map
                        (ι.map
                          (𝟙 (eC.functor.obj (eC.inverse.obj (Λ.F.obj (eA.functor.obj x✝)))) ≫
                            eC.counitIso.hom.app (Λ.F.obj (eA.functor.obj x✝)) ≫ 𝟙 (Λ.F.obj (eA.functor.obj x✝)))) ≫
                      eA.inverse.map
                          (𝟙 (ι.obj (Λ.F.obj (eA.functor.obj x✝))) ≫
                            Λ.π.app (eA.functor.obj x✝) ≫ 𝟙 (eA.functor.obj x✝)) ≫
                        eA.unitIso.inv.app x✝)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Transport

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A
G : C ⥤ C'
e : G ⋙ ι' ≅ ι
x✝ : A
⊢ Epi (𝟙 (ι'.obj (G.obj (Λ.F.obj x✝))) ≫ e.hom.app (Λ.F.obj x✝) ≫ Λ.π.app x✝)

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
⊢ (∃ g, g ≫ K.d q'' q = f) → ∃ β, δ (n - 1) n β = ↑(fromSingleMk f h q' hq' hf)

Tactic:
rintro ⟨g, rfl⟩
    exact ⟨Cochain.fromSingleMk g (by lia), Cochain.δ_fromSingleMk _ _ _ _ h⟩

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ Epi ((karoubi.π' Λ).app X)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝⁴ : Preadditive C
inst✝³ : Preadditive A
inst✝² : ι.Additive
inst✝¹ : IsIdempotentComplete A
inst✝ : IsIdempotentComplete C
⊢ ((toKaroubiEquivalence A).functor ⋙ Λ.karoubi.F ⋙ (toKaroubiEquivalence C).inverse).PreservesZeroMorphisms

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt P.π (n + 1)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ Cofork.π (CokernelCofork.ofπ (pOpcycles P.complex 0) ⋯) ≫
      (P.complex.isoHomologyι₀.symm ≪≫
          isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).hom =
    Cofork.π P.cokernelCofork

Tactic:
rw [← cancel_mono (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 _).inv,
    ← cancel_mono (isoHomologyι₀ _).hom]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ ((Cofork.π (CokernelCofork.ofπ (pOpcycles P.complex 0) ⋯) ≫
          (P.complex.isoHomologyι₀.symm ≪≫
              isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).hom) ≫
        (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt).inv) ≫
      (isoHomologyι₀ ((single C (ComplexShape.down ℕ) 0).obj P.cokernelCofork.pt)).hom =
    (Cofork.π P.cokernelCofork ≫ (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt).inv) ≫
      (isoHomologyι₀ ((single C (ComplexShape.down ℕ) 0).obj P.cokernelCofork.pt)).hom
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n✝ : ℕ
⊢ Epi 0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (({ app := fun P ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } ≫
            { app := fun P ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ }).app
        P).f =
    ((𝟙 ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G)).app P).f

Tactic:
simpa only [hom_ext_iff, G.map_comp, G.map_id] using! G.congr_map P.decompId.symm

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} E
inst✝ : IsIdempotentComplete D
⊢ (karoubiUniversal₂ C D).functor.IsEquivalence

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} E
inst✝ : IsIdempotentComplete D
⊢ (karoubiUniversal C D).functor.IsEquivalence

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} E
inst✝ : IsIdempotentComplete D
⊢ (karoubiUniversal C D).inverse.IsEquivalence

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Epi (Projective.π Z)

Tactic:
infer_instance

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

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✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Projective X
⊢ IsIso
    (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).descOpcycles (F.map (𝟙 X)) 1
      fromLeftDerivedZero'._proof_1 ⋯)

Tactic:
rw [ChainComplex.isIso_descOpcycles_iff]

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✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Projective X
⊢ { X₁ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).X 1,
        X₂ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).X 0, X₃ := F.obj X,
        f := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).d 1 0,
        g := F.map (𝟙 X), zero := ⋯ }.Exact ∧
    Epi (F.map (𝟙 X))
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

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✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Projective X
⊢ IsIso
    (((ProjectiveResolution.self X).isoLeftDerivedObj F 0).hom ≫
      (ChainComplex.isoHomologyι₀
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex)).hom ≫
        (ProjectiveResolution.self X).fromLeftDerivedZero' F)

Tactic:
infer_instance

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

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✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteColimits F
X : C
⊢ IsIso
    ((HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      (ChainComplex.isoHomologyι₀
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as)).hom ≫
        (projectiveResolution X).fromLeftDerivedZero' F)

Tactic:
infer_instance

Goal state after: