mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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:
cat_disch

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

Goal state before:
pp: case refine_2.refine_1
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 C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).map (pathObject.π₀ K₂) =
    f₀

Tactic:
cat_disch

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

Goal state before:
pp: case refine_2.refine_2
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 C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ (pathObject.lift f₀ f₁ (homotopyOfEq f₀ f₁ ⋯) ≫
        (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C) ⋯).inv) ≫
      ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).map (pathObject.π₁ K₂) =
    f₁

Tactic:
cat_disch

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

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j k : β
hij : i + b = j
hjk : j + b = k
⊢ ((if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) ≫ if h : j + b = k then X.d j ≫ X.objEqToHom ⋯ else 0) = 0

Tactic:
subst hij hjk

Goal state after:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i : β
⊢ ((if h : i + b = i + b then X.d i ≫ X.objEqToHom ⋯ else 0) ≫
      if h : i + b + b = i + b + b then X.d (i + b) ≫ X.objEqToHom ⋯ else 0) =
    0
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
⊢ ∀ {i j : ℕ}, (up ℕ).Rel i j → (-1) ^ j = -(-1) ^ i

Tactic:
rintro _ _ rfl; simp [pow_add]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
⊢ ∀ {i j : ℕ}, (down ℕ).Rel i j → (-1) ^ j = -(-1) ^ i

Tactic:
rintro _ _ rfl; simp [pow_add]

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₁
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
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : k₀ = i₀
⊢ (if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
subst h₀

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₁ : ι
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 ≫ φ₁
⊢ (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) ≫
      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
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
⊢ (if i₀ = i₀ then 𝟙 ((double f hi₀₁).X i₀) ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
rw [if_pos rfl, id_comp, comp_id]

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
ι : 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:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

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

Tactic:
erw [← NatTrans.naturality]
    dsimp
    simp only [shiftFunctorZero_hom_app_shift, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (shiftFunctor C 0).map f ≫ (mkIso ((shiftFunctorZero C S).app Y✝.obj) ⋯).hom =
    (mkIso ((shiftFunctorZero C S).app X✝.obj) ⋯).hom ≫ (𝟭 (DifferentialObject S C)).map f

Tactic:
cat_disch

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
⊢ (shiftFunctorAdd C 0 n).hom.app X = eqToHom ⋯ ≫ (shiftFunctor C n).map ((shiftZero C).inv.app X)

Tactic:
ext1
        convert! shiftFunctorAdd_zero_add_hom_app n X.obj
        simp

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

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ δ n n' (toSingleMk f h) = n'.negOnePow • toSingleMk (K.d p' p ≫ f) h'

Tactic:
dsimp only [toSingleMk]

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 : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ δ n n' (single (f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv) n) =
    n'.negOnePow • single ((K.d p' p ≫ f) ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv) n'
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 : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ δ n (n + 1) (Cochain.fromSingleMk f h) = 0

Tactic:
Cochain.δ_fromSingleMk _ _ _ q' (by lia),

Goal state after:
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
⊢ Cochain.fromSingleMk (f ≫ K.d q q') (CochainComplex.HomComplex.Cocycle.fromSingleMk._proof_1 p q n h q' hq') = 0
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 : ℤ
f g : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
hg : g ≫ K.d q q' = 0
⊢ fromSingleMk (f + g) h q' hq' ⋯ = fromSingleMk f h q' hq' hf + fromSingleMk g h q' hq' hg

Tactic:
cat_disch

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 : ℤ
f g : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
hg : g ≫ K.d q q' = 0
⊢ fromSingleMk (f - g) h q' hq' ⋯ = fromSingleMk f h q' hq' hf - fromSingleMk g h q' hq' hg

Tactic:
cat_disch

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 : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ fromSingleMk (-f) h q' hq' ⋯ = -fromSingleMk f h q' hq' hf

Tactic:
cat_disch

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
q' : ℤ
hq' : q + 1 = q'
⊢ fromSingleMk 0 h q' hq' ⋯ = 0

Tactic:
cat_disch

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 : ℤ
f g : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
hg : K.d p' p ≫ g = 0
⊢ toSingleMk (f + g) h p' hp' ⋯ = toSingleMk f h p' hp' hf + toSingleMk g h p' hp' hg

Tactic:
cat_disch

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 : ℤ
f g : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
hg : K.d p' p ≫ g = 0
⊢ toSingleMk (f - g) h p' hp' ⋯ = toSingleMk f h p' hp' hf - toSingleMk g h p' hp' hg

Tactic:
cat_disch

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 : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ toSingleMk (-f) h p' hp' ⋯ = -toSingleMk f h p' hp' hf

Tactic:
cat_disch

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
p' : ℤ
hp' : p' + 1 = p
⊢ toSingleMk 0 h p' hp' ⋯ = 0

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

Tactic:
cat_disch

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

Goal state before:
pp: case g_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
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
⊢ (((projectiveResolution X).homotopyEquiv P).inv ≫ lift f (projectiveResolution X) (projectiveResolution Y)) ≫
      (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
cat_disch

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

Goal state before:
pp: case h_comm
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
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
⊢ (φ ≫ ((projectiveResolution Y).homotopyEquiv Q).inv) ≫ (projectiveResolution Y).π =
    P.π ≫ (ChainComplex.single₀ C).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_2
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (F.mapComposableArrows 1).map (homMk₁ (f.app 1) (f.app 2) ⋯) ≫
      (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom =
    (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_3
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
      (F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
        (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom =
    homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯

Tactic:
cat_disch

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
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
⊢ (P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫ F.leftDerivedToHomotopyCategory.map f =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ ≫
      (Q.isoLeftDerivedToHomotopyCategoryObj F).inv

Tactic:
dsimp [Functor.leftDerivedToHomotopyCategory, isoLeftDerivedToHomotopyCategoryObj]
  rw [assoc, ← Functor.map_comp, iso_inv_naturality f P Q φ comm, Functor.map_comp]
  erw [(F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.naturality_assoc]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case refine_1
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
⊢ (F.mapComposableArrows 1).map (homMk₁ (𝟙 w✝²) g ⋯) ≫ (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝)) ⋯).hom =
    (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝¹)) ⋯).hom ≫ twoδ₂Toδ₁ (F.map f) (F.map g) (F.map f ≫ F.map g) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case refine_2
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
⊢ (F.mapComposableArrows 1).map (homMk₁ f (𝟙 w✝) ⋯) ≫ (isoMk₁ (Iso.refl (F.obj w✝¹)) (Iso.refl (F.obj w✝)) ⋯).hom =
    (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝)) ⋯).hom ≫ twoδ₁Toδ₀ (F.map f) (F.map g) (F.map f ≫ F.map g) ⋯

Tactic:
cat_disch

Goal state after: