mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
⊢ HomComplex.δ 0 1 (HomComplex.Cochain.ofHoms fun n ↦ Injective.ι (K.X n)) +
      (↑(HomComplex.Cocycle.mk (HomComplex.Cochain.mk fun p q x ↦ K.d p q ≫ Injective.ι (K.X q)) 2 i._proof_2 ⋯)).comp
        (HomComplex.Cochain.ofHom (𝟙 (I K))) ⋯ =
    0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
this : ∀ (f : Y ⟶ (t.truncLT n).obj X), f ≫ (t.truncLTι n).app X = 0 → f = 0
⊢ (f₁ - f₂) ≫ (t.truncLTι n).app X = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
⊢ (t.truncLT n).map f ≫ (t.truncLTι n).app Y = (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).mor₁ ≫ e.hom.hom₂

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂).hom
⊢ (t.truncGEπ n₁).app Y ≫ (t.truncGE n₁).map g = e.hom.hom₂ ≫ (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h).mor₂

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
l : Q.X n ⟶ X.X m
hl : π.f n ≫ l = (↑(cocycle₁' sq hsq)).v n m hnm
l' : Q.X n ⟶ ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m)).pt
hl' : l' ≫ Fork.ι ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m)) = l
⊢ π.f n ≫ l' ≫ ι.f m = (↑(cocycle₁' sq hsq)).v n m hnm

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : Plus C
⊢ Fibration (terminal.from X) ↔ ∀ (n : ℤ), Injective (X.obj.X n)

Tactic:
fibration_iff,

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : Plus C
⊢ degreewiseEpiWithInjectiveKernel (terminal.from X).hom ↔ ∀ (n : ℤ), Injective (X.obj.X n)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X
hφ :
  (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLTι b).app X ≫ (t.truncGEπ a).app X
⊢ (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ φ ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
⊢ (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK)).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)

Tactic:
ext n m hnm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
n m : ℤ
hnm : n + 1 = m
⊢ ((Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK)).comp (Cochain.ofHom ι) ⋯) ⋯).v n m hnm =
    (↑(cocycle₁' sq hsq)).v n m hnm
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : C
⊢ toHoCat.map (homMk (resolutionMap (𝟙 X))) = toHoCat.map (𝟙 (mk (resolutionObj X)))

Tactic:
exact resolutionObj_hom_ext (by simpa using .refl _)

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map (homMk (resolutionMap (f ≫ g))) = toHoCat.map (homMk (resolutionMap f) ≫ homMk (resolutionMap g))

Tactic:
exact resolutionObj_hom_ext (by simpa using .refl _)

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
⊢ (midπ f n₀ q₂).f i ≫ ((functor f n₀).map (homOfLE hq).op).hom.h.f i = (midπ f n₀ q₁).f i

Tactic:
rw [← midπ_w f n₀ q₁ q₂ hq]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
⊢ (midπ f n₀ q₂).f i ≫ ((functor f n₀).map (homOfLE hq).op).hom.h.f i =
    (midπ f n₀ q₂ ≫ ((functor f n₀).map (homOfLE hq).op).hom.h).f i
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: case refine_2
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.inv ↔ TwoSquare.GuitartExact e.hom
x✝ : Φ.op.IsLeftDerivabilityStructure
⊢ Φ.IsRightDerivabilityStructure

Tactic:
have : Φ.HasRightResolutions := by
      rw [hasRightResolutions_iff_op]
      infer_instance
    refine ⟨inferInstance, ?_⟩
    rw [← eq]
    exact Φ.op.guitartExact_of_isLeftDerivabilityStructure' _ _ _ e'

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
hα : ∀ (X₁ : C₁), IsIso (α.app (Φ.functor.obj X₁))
this✝¹ : F.HasPointwiseRightDerivedFunctor W₂
this✝ :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso ((F.totalRightDerivedUnit L₂ W₂).app (Φ.functor.obj X₁))
this : (Φ.functor ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
⊢ IsIso (φ.app Y₂)

Tactic:
NatTrans.isIso_app_iff_of_iso φ ((Φ.functor ⋙ L₂).objObjPreimageIso Y₂).symm

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
hα : ∀ (X₁ : C₁), IsIso (α.app (Φ.functor.obj X₁))
this✝¹ : F.HasPointwiseRightDerivedFunctor W₂
this✝ :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso ((F.totalRightDerivedUnit L₂ W₂).app (Φ.functor.obj X₁))
this : (Φ.functor ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
⊢ IsIso (φ.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage Y₂)))
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} H
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
hα : ∀ (X₁ : C₁), IsIso (α.app (Φ.functor.obj X₁))
this✝² : F.HasPointwiseRightDerivedFunctor W₂
this✝¹ :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso ((F.totalRightDerivedUnit L₂ W₂).app (Φ.functor.obj X₁))
this✝ : (Φ.functor ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
this : IsIso φ
⊢ F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft (asIso φ).hom = α

Tactic:
by cat_disch

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 cat_disch

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 cat_disch

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
⊢ (isomorphisms (Plus (InjectiveObject C))).inverseImage (L C).functor =
    (CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus

Tactic:
ext; apply isIso_quotient_map_iff

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✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
hS : S.ShortExact
⊢ (ConcreteCategory.hom
          { X₁ := AddCommGrpCat.of (Ext (F.obj X) (S.map F).X₂ n),
              X₂ := AddCommGrpCat.of (Ext (F.obj X) (S.map F).X₃ n),
              X₃ := AddCommGrpCat.of (Ext (F.obj X) (S.map F).X₁ (n + 1)),
              f := AddCommGrpCat.ofHom ((Ext.mk₀ (S.map F).g).postcomp (F.obj X) ⋯),
              g := AddCommGrpCat.ofHom (⋯.extClass.postcomp (F.obj X) ⋯), zero := ⋯ }.f).comp
      (F.mapExtAddHom X S.X₂ n) =
    (F.mapExtAddHom X S.X₃ n).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext X S.X₂ n), X₂ := AddCommGrpCat.of (Ext X S.X₃ n),
            X₃ := AddCommGrpCat.of (Ext X S.X₁ (n + 1)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.g).postcomp X ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.postcomp X ⋯), zero := ⋯ }.f)

Tactic:
by cat_disch

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✝¹ : EnoughInjectives C
inst✝ : F.PreservesInjectiveObjects
X : C
n : ℕ
hn : ∀ (Y : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
Y : C
I : InjectivePresentation Y := Classical.arbitrary (InjectivePresentation Y)
S : ShortComplex C := { X₁ := Y, X₂ := I.J, X₃ := cokernel I.f, f := I.f, g := cokernel.π I.f, zero := ⋯ }
this : Injective (S.map F).X₂
hS : S.ShortExact
⊢ (ConcreteCategory.hom
          { X₁ := AddCommGrpCat.of (Ext (F.obj X) (S.map F).X₂ n),
              X₂ := AddCommGrpCat.of (Ext (F.obj X) (S.map F).X₃ n),
              X₃ := AddCommGrpCat.of (Ext (F.obj X) (S.map F).X₁ (n + 1)),
              f := AddCommGrpCat.ofHom ((Ext.mk₀ (S.map F).g).postcomp (F.obj X) ⋯),
              g := AddCommGrpCat.ofHom (⋯.extClass.postcomp (F.obj X) ⋯), zero := ⋯ }.g).comp
      (F.mapExtAddHom X S.X₃ n) =
    (F.mapExtAddHom X S.X₁ (n + 1)).comp
      (ConcreteCategory.hom
        { X₁ := AddCommGrpCat.of (Ext X S.X₂ n), X₂ := AddCommGrpCat.of (Ext X S.X₃ n),
            X₃ := AddCommGrpCat.of (Ext X S.X₁ (n + 1)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.g).postcomp X ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.postcomp X ⋯), zero := ⋯ }.g)

Tactic:
by cat_disch

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 : ChainComplex C ℕ
inst✝¹ : ∀ (n : ℕ), Projective (K.X n)
inst✝ : ∀ (n : ℕ), Projective (L.X n)
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f

Tactic:
rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingDownNat,
    CochainComplex.IsKProjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]

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

Goal state before:
pp: case pos
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₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : i = i₀
⊢ ((if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫
      if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) =
    0

Tactic:
subst hi

Goal state after:
case pos
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 j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
⊢ ((if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫
      if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) =
    0
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 : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
i' : ι'
hi : e.f i = i'
⊢ (stupidTruncMap φ e).f i' ≫ (L.stupidTruncXIso e hi).hom = (K.stupidTruncXIso e hi).hom ≫ φ.f i'

Tactic:
subst hi

Goal state after:
ι : 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 : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (stupidTruncMap φ e).f (e.f i) ≫ (L.stupidTruncXIso e ⋯).hom = (K.stupidTruncXIso e ⋯).hom ≫ φ.f (e.f i)
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
ι : Type u_2
c : ComplexShape ι
i : ι
inst✝ : DecidableEq ι
hi : ∀ (j : ι), ¬c.Rel i j
X : C
K : HomologicalComplex C c
g : (single C c i).obj X ⟶ K
⊢ (fun f ↦ mkHomFromSingle f ⋯) ((fun g ↦ (singleObjXSelf c i X).inv ≫ g.f i) g) = g

Tactic:
by cat_disch

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
Z' : C
P' : ProjectiveResolution Z'
f : Z ⟶ Z'
φ : P.Hom P' f
⊢ φ.hom ≫ P'.π = P.π ≫ (single₀ C).map f

Tactic:
by cat_disch

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
⊢ ∀ {X Y : C ⥤ Karoubi D} (f : X ⟶ Y),
    (functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map f ≫
        (NatIso.ofComponents
            (fun X ↦
              { hom := { f := (Y.obj X).p, comm := ⋯ }, inv := { f := (Y.obj X).p, comm := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ })
            ⋯).hom =
      (NatIso.ofComponents
            (fun X_1 ↦
              { hom := { f := (X.obj X_1).p, comm := ⋯ }, inv := { f := (X.obj X_1).p, comm := ⋯ }, hom_inv_id := ⋯,
                inv_hom_id := ⋯ })
            ⋯).hom ≫
        (𝟭 (C ⥤ Karoubi D)).map f

Tactic:
by cat_disch

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
⊢ (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p ≫
      (G.map P.decompId_i).f ≫
        ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p =
    (G.map P.decompId_i).f

Tactic:
simpa only [hom_ext_iff, G.map_comp, G.map_id] using!
                    G.congr_map
                      (show 𝟙 _ ≫ P.decompId_i ≫ (toKaroubi C).map P.p = P.decompId_i by simp)

Goal state after: