mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
this : RF.IsLeftKanExtension α
⊢ α ≫ L.whiskerLeft (RF.rightDerivedDesc α W G β) = β

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

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
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
⊢ (structuredArrowEquiv W W.Q L) (StructuredArrow.mk (𝟙 (W.Q.obj X))) = StructuredArrow.mk (𝟙 (L.obj X))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: case hP₂
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
Y₁ Y₂ : C
w : Y₁ ⟶ Y₂
⊢ ∀ (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))

Tactic:
hw

Goal state after:
case hP₂
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := fun g ↦ P ((structuredArrowEquiv W W.Q L) g)
Y₁ Y₂ : C
w : Y₁ ⟶ Y₂
hw : W w
⊢ ∀ (φ : W.Q.obj X ⟶ W.Q.obj Y₂), P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
⊢ ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
simp

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

Goal state before:
pp: 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 : C₂ ⥤ D
⊢ ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w)) ↔
    (StructuredArrow.right ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w)).IsLeftKanExtension
      (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) = s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) = s.ι.app (CostructuredArrow.mk φ)
⊢ e.hom.app X₁ ≫
      G.map (L.map w ≫ (Localization.isoOfHom L W w hw).inv) ≫
        G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
F : C ⥤ H
RF : D ⥤ H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst✝ : RF.IsRightDerivedFunctor α W
⊢ α =
    (Localization.fac F hF L).inv ≫
      L.whiskerLeft ((Localization.lift F hF L).rightDerivedUnique RF (Localization.fac F hF L).inv α W).hom

Tactic:
simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} D₁
inst✝³ : Category.{v_5, u_5} D₂
inst✝² : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
X✝ : C₁ᵒᵖ
⊢ (w ≫ₕ w').op.natTrans.app X✝ = (w.op ≫ᵥ w'.op).natTrans.app X✝

Tactic:
simp

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

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

Tactic:
← isRightDerivabilityStructure_iff_of_equivalences iso

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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 ℤ
hK : ((opEquivalence C).functor.obj (op K)).IsKInjective
L : CochainComplex C ℤ
f : K ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ 0 = (opEquivalence C).functor.map (Quiver.Hom.op 0)

Tactic:
simp

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

Goal state before:
pp: case 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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
X✝ Y✝ : CochainComplex.Plus C
f : X✝ ⟶ Y✝
⊢ CochainComplex.Plus.quasiIso C f → IsIso ((quotient C ⋙ L).map f)

Tactic:
hf

Goal state after:
case 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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
X✝ Y✝ : CochainComplex.Plus C
f : X✝ ⟶ Y✝
hf : CochainComplex.Plus.quasiIso C f
⊢ IsIso ((quotient C ⋙ L).map f)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case 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
L✝ : Plus C ⥤ H
inst✝ : L✝.IsLocalization (quasiIso C)
K L : CochainComplex.Plus C
f : K ⟶ L
⊢ (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) f →
    CochainComplex.Plus.quasiIso C f

Tactic:
hf

Goal state after:
case 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
L✝ : Plus C ⥤ H
inst✝ : L✝.IsLocalization (quasiIso C)
K L : CochainComplex.Plus C
f : K ⟶ L
hf : (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) f
⊢ CochainComplex.Plus.quasiIso C f
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 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₁)
n : ℤ
⊢ (ComplexShape.up ℤ).Rel n (n + 1)

Tactic:
simp

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

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
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
pf✝⁷ : HasZeroObject C
pf✝⁶ : IsRightCancelAdd ℤ
pf✝⁵ : IsRightCancelAdd ℤ
pf✝⁴ : F.PreservesZeroMorphisms
pf✝³ : (HomologicalComplex.single C (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
pf✝² : (F.mapHomologicalComplex (ComplexShape.up ℤ)).PreservesZeroMorphisms
h1 :
  ((S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)).map
      (F.mapHomologicalComplex (ComplexShape.up ℤ))).ShortExact
pf✝¹ : HasZeroObject D
pf✝ : (HomologicalComplex.single D (ComplexShape.up ℤ) 0).PreservesZeroMorphisms
h2 : ((S.map F).map (HomologicalComplex.single D (ComplexShape.up ℤ) 0)).ShortExact
⊢ Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app S.X₃ ≫ (F.mapCochainComplexSingleFunctor 0).hom.app S.X₃) ≫
      triangleOfSESδ h2 =
    𝟙 (((singleFunctors D).functor 0).obj (F.obj S.X₃)) ≫
      triangleOfSESδ h2 ≫ (shiftFunctor (DerivedCategory D) 1).map (𝟙 ((singleFunctor D 0).obj (F.obj S.X₁)))

Tactic:
simp

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

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
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃ ≫
      ShiftedHom.map hS.singleδ F.mapDerivedCategory ≫
        (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    ⋯.singleδ

Tactic:
by
  dsimp [ShiftedHom.map, ShortComplex.ShortExact.singleδ]
  simp only [Functor.map_comp, Category.assoc, Functor.commShiftIso_hom_naturality,
    DerivedCategory.map_triangleOfSESδ, singleFunctorsPostcompQIso_hom_hom,
    singleFunctorsPostcompQIso_inv_hom]
  generalize_proofs _ _ _ _ _ _ h1 _ _ h2
  dsimp [CochainComplex.singleFunctors]
  rw [Functor.map_id, Category.id_comp,
    Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc,
    Iso.inv_hom_id_app_assoc, Functor.map_id, Functor.map_id, Category.id_comp,
    ← Functor.map_comp,
    F.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app,
    dsimp% triangleOfSESδ_naturality h1 h2
      (S.mapNatTrans (F.mapCochainComplexSingleFunctor 0).hom),
    ← Functor.map_comp_assoc]
  simp

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

Goal state before:
pp: ι : Type u_1
⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case refl
β : 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)
x : β
⊢ X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ X.d x y ≫ eqToHom ⋯ = X.d x y

Tactic:
simp

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

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✝¹ : HasExt C
inst✝ : HasExt D
X✝ Y✝ : C
n✝ : ℕ
X Y : C
n : ℕ
⊢ Ext.mapExactFunctor F 0 = 0

Tactic:
simp

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

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✝¹ : HasExt C
inst✝ : HasExt D
X✝ Y✝ : C
n✝ : ℕ
X Y : C
n : ℕ
⊢ ∀ (x y : Ext X Y n), Ext.mapExactFunctor F (x + y) = Ext.mapExactFunctor F x + Ext.mapExactFunctor F y

Tactic:
simp

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

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✝⁵ : HasExt C
inst✝⁴ : HasExt D
X✝ Y✝ : C
n✝ : ℕ
R : Type u_1
inst✝³ : Ring R
inst✝² : CategoryTheory.Linear R C
inst✝¹ : CategoryTheory.Linear R D
inst✝ : Linear R F
X Y : C
n : ℕ
⊢ ∀ (m : R) (x : Ext X Y n),
    (↑(F.mapExtAddHom X Y n)).toFun (m • x) = (RingHom.id R) m • (↑(F.mapExtAddHom X Y n)).toFun x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ f.hom ≫ Y.d = X.d ≫ (shiftFunctor C 1).map f.hom

Tactic:
hf

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

Goal state before:
pp: S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
f : X.obj ≅ Y.obj
hf : X.d ≫ (shiftFunctor C 1).map f.hom = f.hom ≫ Y.d
⊢ autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1

Tactic:
exact f.inv_hom_id

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
indices : Finset ι
h_support : finrankSupport X ⊆ ↑indices
⊢ eulerChar c X = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(X i))

Tactic:
simp only [eulerChar]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
indices : Finset ι
h_support : finrankSupport X ⊆ ↑indices
⊢ ∑ᶠ (i : ι), ↑(c.χ i) * ↑(Module.finrank R ↑(X i)) = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(X i))
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ : DifferentialObject S C
⊢ autoParam
    ({ f := F.map (𝟙 X✝).f, comm := ⋯ }.f =
      (𝟙 { obj := F.obj X✝.obj, d := F.map X✝.d ≫ η.app X✝.obj, d_squared := ⋯ }).f)
    DifferentialObject.ext._auto_1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X✝ Y✝ Z✝ : DifferentialObject S C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ autoParam
    ({ f := F.map (f✝ ≫ g✝).f, comm := ⋯ }.f = ({ f := F.map f✝.f, comm := ⋯ } ≫ { f := F.map g✝.f, comm := ⋯ }).f)
    DifferentialObject.ext._auto_1

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.ofNat n + 1 ≠ Int.ofNat m
⊢ ¬(ComplexShape.up ℕ).Rel n m

Tactic:
simp at hnm ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : ¬↑n + 1 = ↑m
⊢ ¬n + 1 = m
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.negSucc m
⊢ ¬(ComplexShape.down ℕ).Rel n m

Tactic:
simp at hnm ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : ¬Int.negSucc n + 1 = Int.negSucc m
⊢ ¬m + 1 = n
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₁
X : C
K : HomologicalComplex C c
φ₀ : (eval C c i₀ ⋙ coyoneda.obj (op X)).obj K
⊢ φ₀ ≫ K.d i₀ i₁ = 𝟙 X ≫ φ₀ ≫ K.d i₀ i₁

Tactic:
simp

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₁
X : C
K : HomologicalComplex C c
φ₀ : (eval C c i₀ ⋙ coyoneda.obj (op X)).obj K
⊢ ∀ (k : ι), c.Rel i₁ k → (φ₀ ≫ K.d i₀ i₁) ≫ K.d i₁ k = 0

Tactic:
simp

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

Goal state before:
pp: case pos.negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
hnm : Int.negSucc 0 + 1 = 0
hmp : 0 + 1 = 1
⊢ h.d (Int.negSucc 0) 0 ≫ h.d 0 1 = 0

Tactic:
simp

Goal state after: