mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ lift.shiftIso hΦ (m + n) a a'' ⋯ =
    (Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
      ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫ lift.shiftIso hΦ n a a' ha'

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (lift.shiftIso hΦ (m + n) a a'' ⋯).hom.app X =
    ((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
            ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
              isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                lift.shiftIso hΦ n a a' ha').hom.app
      X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj (Opposite.unop Y)
h₁ : Triangle.mk f.unop a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.unop Z
⊢ ∃ X_1 f_1 h, ∃ (_ : Triangle.mk f_1 f h ∈ Pretriangulated.distinguishedTriangles), P X_1

Tactic:
exact ⟨_, _, _, Pretriangulated.op_distinguished _ h₁, h₂⟩

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
ha' : n + a = a'
⊢ (((F.lift G Φ hΦ).postcomp G).shiftIso n a a' ha').hom ≫ (hΦ a).hom =
    whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
ha' : n + a = a'
X : C
⊢ ((((F.lift G Φ hΦ).postcomp G).shiftIso n a a' ha').hom ≫ (hΦ a).hom).app X =
    (whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom).app X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ IsIso ((t.truncLEι n).app X)

Tactic:
← isLE_iff_isIso_truncLEι_app

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsLE X n
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ ((singleFunctor C n).obj X).IsLE n

Tactic:
rw [← isLE_ι_obj_iff]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ (ι.obj ((singleFunctor C n).obj X)).IsLE 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
a b : ℤ
h : a ≤ b
⊢ t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C 1) =
    t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b

Tactic:
ext X

Goal state after:
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
a b : ℤ
h : a ≤ b
X : C
⊢ (t.truncGEδLT a ≫ Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (shiftFunctor C 1)).app X =
    (t.natTransTruncGEOfLE a b h ≫ t.truncGEδLT b).app X
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ModelCategory C
X Y : C
inst✝⁴ : IsCofibrant X
inst✝³ : IsCofibrant Y
inst✝² : IsFibrant X
inst✝¹ : IsFibrant Y
f : X ⟶ Y
inst✝ : WeakEquivalence f
g : Y ⟶ X
hg : LeftHomotopyRel (f ≫ g) (𝟙 X)
⊢ LeftHomotopyRel (f ≫ g ≫ f) f

Tactic:
simpa using hg.postcomp f

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

Goal state before:
pp: case mp
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'.hom ↔ TwoSquare.GuitartExact e.inv
hasLeftResolutions✝ : Φ.HasLeftResolutions
guitartExact'✝ : TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).inv
⊢ TwoSquare.GuitartExact e'.hom

Tactic:
eq

Goal state after:
case mp
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'.hom ↔ TwoSquare.GuitartExact e.inv
hasLeftResolutions✝ : Φ.HasLeftResolutions
guitartExact'✝ : TwoSquare.GuitartExact (CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).inv
⊢ TwoSquare.GuitartExact e.inv
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
X Y : C
w : X ⟶ Y
hw : W w
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ F.HasPointwiseRightDerivedFunctorAt W Y

Tactic:
simp only [F.hasPointwiseRightDerivedFunctorAt_iff W.Q W]

Goal state after:
C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
X Y : C
w : X ⟶ Y
hw : W w
⊢ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj Y)
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: case e_6
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝ : ∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F
F₁ F₂ : C₂ ⥤ D
τ : F₁ ⟶ F₂
⊢ T.whiskerLeft τ ≫
      T.whiskerLeft (R.lanUnit.app F₂) ≫
        (T.associator R (R.lan.obj F₂)).inv ≫
          whiskerRight w.natTrans (R.lan.obj F₂) ≫ (L.associator B (R.lan.obj F₂)).hom =
    (T.whiskerLeft (R.lanUnit.app F₁) ≫
        (T.associator R (R.lan.obj F₁)).inv ≫
          whiskerRight w.natTrans (R.lan.obj F₁) ≫ (L.associator B (R.lan.obj F₁)).hom) ≫
      ((whiskeringLeft C₁ C₃ D).obj L).map (B.whiskerLeft (R.lan.map τ))

Tactic:
ext X

Goal state after:
case e_6
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝ : ∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F
F₁ F₂ : C₂ ⥤ D
τ : F₁ ⟶ F₂
X : C₁
⊢ (T.whiskerLeft τ ≫
          T.whiskerLeft (R.lanUnit.app F₂) ≫
            (T.associator R (R.lan.obj F₂)).inv ≫
              whiskerRight w.natTrans (R.lan.obj F₂) ≫ (L.associator B (R.lan.obj F₂)).hom).app
      X =
    ((T.whiskerLeft (R.lanUnit.app F₁) ≫
            (T.associator R (R.lan.obj F₁)).inv ≫
              whiskerRight w.natTrans (R.lan.obj F₁) ≫ (L.associator B (R.lan.obj F₁)).hom) ≫
          ((whiskeringLeft C₁ C₃ D).obj L).map (B.whiskerLeft (R.lan.map τ))).app
      X
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.41) → [inst : Category.{?u.42, ?u.41} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L

Tactic:
obtain ⟨X, ⟨eX⟩⟩ := DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE (Q.obj K) a

Goal state after:
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
⊢ HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
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 : IsFibrant K
⊢ Injective ({ obj := K, property := hK✝ }.obj.obj.X n)

Tactic:
modelCategoryQuillen.isFibrant_iff

Goal state after:
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)
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)
⊢ IsFibrant ((InjectiveObject.ι C).mapCochainComplexPlus.obj K)

Tactic:
modelCategoryQuillen.isFibrant_iff

Goal state after:
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 (((InjectiveObject.ι C).mapCochainComplexPlus.obj K).obj.X n)
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
    ((CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus)

Tactic:
by
  rw [inverseImage_quasiIso_mapCochainComplexPlus_injectiveObjectι]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map X.d ≫
      (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map X.d) ≫
        (shiftComm ((CategoryTheory.shiftFunctor C 1).obj X.obj) 1 n).hom ≫
          (CategoryTheory.shiftFunctor C 1).map (shiftComm X.obj 1 n).hom =
    0

Tactic:
← Functor.map_comp_assoc,

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map (X.d ≫ (CategoryTheory.shiftFunctor C 1).map X.d) ≫
      (shiftComm ((CategoryTheory.shiftFunctor C 1).obj X.obj) 1 n).hom ≫
        (CategoryTheory.shiftFunctor C 1).map (shiftComm X.obj 1 n).hom =
    0
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.shiftFunctor C n).map X✝.d ≫
      (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.f) ≫ (shiftComm Y✝.obj 1 n).hom =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj

Tactic:
← Functor.map_comp_assoc,

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.shiftFunctor C n).map (X✝.d ≫ (CategoryTheory.shiftFunctor C 1).map f.f) ≫
      (shiftComm Y✝.obj 1 n).hom =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj
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₁ : ι
K : HomologicalComplex C c
φ₁ : X₁ ⟶ K.X i₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
hi₀₁ : c.Rel k₀ i₁
h : k₀ ≠ i₁
φ₀ : X₀ ⟶ K.X k₀
comm : φ₀ ≫ K.d k₀ i₁ = f ≫ φ₁
⊢ (eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
obtain rfl := c.next_eq hk 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 ι
K : HomologicalComplex C c
k₀ k₁ : ι
hk : c.Rel k₀ k₁
φ₀ : X₀ ⟶ K.X k₀
φ₁ : X₁ ⟶ K.X k₁
hφ : ∀ (k : ι), c.Rel k₁ k → φ₁ ≫ K.d k₁ k = 0
hi₀₁ : c.Rel k₀ k₁
h : k₀ ≠ k₁
comm : φ₀ ≫ K.d k₀ k₁ = f ≫ φ₁
⊢ (eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain ((singleFunctor C p).obj X) K n
p' q' : ℤ
hpq' : p' + n = q'
hp : ¬p' = p
⊢ ((fun f ↦ fromSingleMk f h)
          ((fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

Tactic:
exact (HomologicalComplex.isZero_single_obj_X _ _ _ _ hp).eq_of_src _ _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K ((singleFunctor C q).obj X) n
p' q' : ℤ
hpq' : p' + n = q'
⊢ ((fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

Tactic:
by_cases hq : q' = q

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K ((singleFunctor C q).obj X) n
p' q' : ℤ
hpq' : p' + n = q'
hq : q' = q
⊢ ((fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α)).v
      p' q' hpq' =
    α.v p' q' hpq'

case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
α : Cochain K ((singleFunctor C q).obj X) n
p' q' : ℤ
hpq' : p' + n = q'
hq : ¬q' = q
⊢ ((fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α)).v
      p' q' hpq' =
    α.v p' q' hpq'
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
F G H : C ⥤ Karoubi D
φ : F ⟶ G
φ' : G ⟶ H
⊢ FunctorExtension₁.map (φ ≫ φ') = FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ'

Tactic:
by
    ext P
    simp only [comp_f, FunctorExtension₁.map_app_f, NatTrans.comp_app, assoc]
    have h := φ.naturality P.p
    have h' := F.congr_map P.idem
    simp only [hom_ext_iff, comp_f, F.map_comp] at h h'
    slice_rhs 2 3 => rw [← h]
    slice_rhs 1 2 => rw [h']
    simp only [assoc]

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
⊢ ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
      (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
        (whiskeringRight C (Karoubi D) D).obj (toKaroubi D).inv).IsEquivalence

Tactic:
change (karoubiUniversal C D).inverse.IsEquivalence

Goal state after:
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
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
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
⊢ ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
      { app := fun P ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p, naturality := ⋯ } =
    τ

Tactic:
ext X

Goal state after:
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
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
          { app := fun P ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p, naturality := ⋯ }).app
      X =
    τ.app X
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
F G : Karoubi C ⥤ D
τ : F ⟶ G
⊢ {
      app := fun P ↦
        F.map P.decompId_i ≫ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map τ).app P.X ≫ G.map P.decompId_p,
      naturality := ⋯ } =
    τ

Tactic:
ext X

Goal state after:
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
F G : Karoubi C ⥤ D
τ : F ⟶ G
X : Karoubi C
⊢ {
          app := fun P ↦
            F.map P.decompId_i ≫
              (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map τ).app P.X ≫ G.map P.decompId_p,
          naturality := ⋯ }.app
      X =
    τ.app X
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
n : ℕ
⊢ Projective ((ofComplex Z).X n)

Tactic:
by
  obtain (_ | _ | _ | n) := n <;> apply Projective.projective_over

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
⊢ Projective.π (kernel (Projective.π Z)) ≫ kernel.ι (Projective.π Z) ≫ Projective.π Z = 0

Tactic:
kernel.condition,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective.π (kernel (Projective.π Z)) ≫ 0 = 0
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
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (Q.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n

Tactic:
← Functor.map_comp_assoc,

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
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        (F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n