mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
W : MorphismProperty C
L : C ⥤ D
L' : C ⥤ D'
inst✝¹ : L.IsLocalization W
inst✝ : L'.IsLocalization W
X Y : C
f : L'.obj X ⟶ L'.obj Y
⊢ (fun f ↦ StructuredArrow.mk ((homEquiv W L L') f.hom))
      ((fun f ↦ StructuredArrow.mk ((homEquiv W L' L) f.hom)) (StructuredArrow.mk f)) =
    StructuredArrow.mk f

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
W : MorphismProperty C
L : C ⥤ D
L' : C ⥤ D'
inst✝¹ : L.IsLocalization W
inst✝ : L'.IsLocalization W
X Y : C
f : L'.obj X ⟶ L'.obj Y
⊢ StructuredArrow.mk ((homEquiv W L L') ((homEquiv W L' L) f)) = StructuredArrow.mk f
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 ℤ
inst✝² : EnoughInjectives C
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
this : K.IsStrictlyGE n
L' : CochainComplex C ℤ
w✝² : L'.IsStrictlyGE n
i : K ⟶ L'
p : L' ⟶ L
w✝¹ : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w✝ : QuasiIso p
⊢ ∃ K', ∃ (_ : K'.IsStrictlyGE n), ∃ ι π, Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = i ≫ p

Tactic:
obtain ⟨K', _, ι, π, _, _, hπ, rfl⟩ := cm5a_cof i n

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K L : CochainComplex C ℤ
inst✝² : EnoughInjectives C
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
this : K.IsStrictlyGE n
L' : CochainComplex C ℤ
w✝³ : L'.IsStrictlyGE n
p : L' ⟶ L
hp : degreewiseEpiWithInjectiveKernel p
w✝² : QuasiIso p
K' : CochainComplex C ℤ
w✝¹ : K'.IsStrictlyGE n
ι : K ⟶ K'
π : K' ⟶ L'
left✝¹ : Mono ι
left✝ : QuasiIso ι
hπ : degreewiseEpiWithInjectiveKernel π
w✝ : Mono (ι ≫ π)
⊢ ∃ K'_1,
    ∃ (_ : K'_1.IsStrictlyGE n),
      ∃ ι_1 π_1, Mono ι_1 ∧ QuasiIso ι_1 ∧ degreewiseEpiWithInjectiveKernel π_1 ∧ ι_1 ≫ π_1 = (ι ≫ π) ≫ p
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
F : C₂ ⥤ D
X₃ : C₃
inst✝ : (w.costructuredArrowRightwards X₃).Final
⊢ L.HasPointwiseLeftKanExtensionAt (T ⋙ F) X₃ ↔ R.HasPointwiseLeftKanExtensionAt F (B.obj X₃)

Tactic:
dsimp [Functor.HasPointwiseLeftKanExtensionAt]

Goal state after:
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
F : C₂ ⥤ D
X₃ : C₃
inst✝ : (w.costructuredArrowRightwards X₃).Final
⊢ HasColimit (CostructuredArrow.proj L X₃ ⋙ T ⋙ F) ↔ HasColimit (CostructuredArrow.proj R (B.obj X₃) ⋙ F)
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₁ F₂ : C₂ ⥤ D
τ : F₁ ⟶ F₂
⊢ ((whiskeringLeft C₁ C₂ D).obj T ⋙ L.lan).map τ ≫
      ((L.lanAdjunction D).homEquiv (((whiskeringLeft C₁ C₂ D).obj T).obj F₂)
            ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₂)).symm
        (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F₂) (R.lanUnit.app F₂)).compTwoSquare w)) =
    ((L.lanAdjunction D).homEquiv (((whiskeringLeft C₁ C₂ D).obj T).obj F₁)
            ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₁)).symm
        (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F₁) (R.lanUnit.app F₁)).compTwoSquare w)) ≫
      (R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).map τ

Tactic:
dsimp

Goal state after:
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₂
⊢ L.lan.map (T.whiskerLeft τ) ≫
      ((L.lanAdjunction D).homEquiv (T ⋙ F₂) (B ⋙ R.lan.obj F₂)).symm
        (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) =
    ((L.lanAdjunction D).homEquiv (T ⋙ F₁) (B ⋙ R.lan.obj F₁)).symm
        (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) ≫
      B.whiskerLeft (R.lan.map τ)
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)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (L.map w)
⊢ IsIso (e.hom.app X₁ ≫ (L ⋙ G).map w ≫ e.inv.app X₂)

Tactic:
dsimp

Goal state after:
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φ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (L.map w)
⊢ IsIso (e.hom.app X₁ ≫ G.map (L.map w) ≫ e.inv.app X₂)
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 ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage Y₂)))

Tactic:
dsimp

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 (L₂.obj (Φ.functor.obj ((Φ.functor ⋙ L₂).objPreimage Y₂))))
Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
K : CochainComplex C₁ ℤ
⊢ F.mapDerivedCategoryFactors.hom.app K =
    (whiskerRight (DerivedCategory.quotientCompQhIso C₁).inv F.mapDerivedCategory ≫
          ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).associator DerivedCategory.Qh F.mapDerivedCategory).hom ≫
            (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).whiskerLeft F.mapDerivedCategoryFactorsh.hom ≫
              ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).associator (F.mapHomotopyCategory (ComplexShape.up ℤ))
                    DerivedCategory.Qh).inv ≫
                whiskerRight (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom DerivedCategory.Qh ≫
                  ((F.mapHomologicalComplex (ComplexShape.up ℤ)).associator
                        (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh).hom ≫
                    (F.mapHomologicalComplex (ComplexShape.up ℤ)).whiskerLeft
                      (DerivedCategory.quotientCompQhIso C₂).hom).app
      K

Tactic:
dsimp

Goal state after:
C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
K : CochainComplex C₁ ℤ
⊢ F.mapDerivedCategoryFactors.hom.app K =
    F.mapDerivedCategory.map ((DerivedCategory.quotientCompQhIso C₁).inv.app K) ≫
      𝟙 (F.mapDerivedCategory.obj (DerivedCategory.Qh.obj ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K))) ≫
        F.mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K) ≫
          𝟙
              (DerivedCategory.Qh.obj
                ((HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)).obj
                  ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K).as))) ≫
            DerivedCategory.Qh.map ((F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom.app K) ≫
              𝟙
                  (DerivedCategory.Qh.obj
                    ((HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)).obj
                      ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K))) ≫
                (DerivedCategory.quotientCompQhIso C₂).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : Plus (InjectiveObject C)
n : ℤ
⊢ Injective (((InjectiveObject.ι C).mapCochainComplexPlus.obj K).obj.X n)

Tactic:
dsimp

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 (K.obj.X n).obj
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : FibrantObject (Plus C)
n : ℤ
⊢ isInjective C (((FibrantObject.ι ⋙ ι C).obj K).X n)

Tactic:
dsimp

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 : FibrantObject (Plus C)
n : ℤ
⊢ isInjective C (K.obj.obj.X n)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex.Plus (InjectiveObject C)
f : K ⟶ L
⊢ IsIso
      (((InjectiveObject.ι C).mapHomotopyCategory (ComplexShape.up ℤ)).map
        ((ι (InjectiveObject C)).map ((quotient (InjectiveObject C)).map f))) ↔
    CochainComplex.Plus.quasiIso C ((InjectiveObject.ι C).mapCochainComplexPlus.map f)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex.Plus (InjectiveObject C)
f : K ⟶ L
⊢ IsIso
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
        (((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).map f.hom)) ↔
    CochainComplex.Plus.quasiIso C ((InjectiveObject.ι C).mapCochainComplexPlus.map f)
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
i : ℤ
hi : autoParam (i < -d) isStrictlyGE_iff._auto_1
⊢ d < ComplexShape.embeddingUpIntDownInt.f i

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
d : ℤ
inst✝¹ : K.IsStrictlyLE d
inst✝ : ∀ (n : ℤ), Projective (K.X n)
L : CochainComplex Cᵒᵖ ℤ := (opEquivalence C).functor.obj (op K)
this : ∀ (n : ℤ), Injective (L.X n)
i : ℤ
hi : autoParam (i < -d) isStrictlyGE_iff._auto_1
⊢ d < -i
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✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
        Q.map (CochainComplex.mappingCone.triangle (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))).f).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))).X₁ ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
dsimp

Goal state after:
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✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map (CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
        Q.map (CochainComplex.mappingCone.triangle ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map S.f)).mor₃ ≫
          (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
Module: Mathlib.Algebra.Homology.HasNoLoop

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k

Tactic:
by
  grind +splitIndPred

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ (∃ i, c.Rel i j ∧ i ≠ j) ∨ ∀ (i : ι), ¬c.Rel i j

Tactic:
by
  grind +splitIndPred

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 ≅ Y
⊢ (𝟙 X).f = 𝟙 X.obj

Tactic:
id_f

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 ≅ Y
⊢ 𝟙 X.obj = 𝟙 X.obj
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 ≅ Y
⊢ (𝟙 Y).f = 𝟙 Y.obj

Tactic:
id_f

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 ≅ Y
⊢ 𝟙 Y.obj = 𝟙 Y.obj
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 := f.hom, comm := hf } ≫ { f := f.inv, comm := ⋯ }).f = (𝟙 X).f) ext._auto_1

Tactic:
dsimp

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
⊢ autoParam (f.hom ≫ f.inv = 𝟙 X.obj) ext._auto_1
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 := f.inv, comm := ⋯ } ≫ { f := f.hom, comm := hf }).f = (𝟙 Y).f) ext._auto_1

Tactic:
dsimp

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
⊢ autoParam (f.inv ≫ f.hom = 𝟙 Y.obj) ext._auto_1
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₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ ((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:
dsimp

Goal state after:
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
⊢ ((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.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✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ { obj := F.obj X✝.obj, d := F.map X✝.d ≫ η.app X✝.obj, d_squared := ⋯ }.d ≫ (shiftFunctor D 1).map (F.map f.f) =
    F.map f.f ≫ { obj := F.obj Y✝.obj, d := F.map Y✝.d ≫ η.app Y✝.obj, d_squared := ⋯ }.d

Tactic:
dsimp

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
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✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ (F.map X✝.d ≫ η.app X✝.obj) ≫ (shiftFunctor D 1).map (F.map f.f) = F.map f.f ≫ F.map Y✝.d ≫ η.app Y✝.obj
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : HomSubtype S C X✝ Y✝
⊢ ⟨ConcreteCategory.hom { f := ConcreteCategory.ofHom ↑x✝, comm := ⋯ }.f, ⋯⟩ = x✝

Tactic:
dsimp

Goal state after:
S : Type u_1
inst✝⁵ : AddMonoidWithOne S
C : Type (u + 1)
inst✝⁴ : LargeCategory C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasShift C S
X✝ Y✝ : DifferentialObject S C
x✝ : HomSubtype S C X✝ Y✝
⊢ ⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = x✝
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✝
⊢ { obj := (CategoryTheory.shiftFunctor C n).obj X✝.obj,
          d := (CategoryTheory.shiftFunctor C n).map X✝.d ≫ (shiftComm X✝.obj 1 n).hom, d_squared := ⋯ }.d ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.f) =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      { obj := (CategoryTheory.shiftFunctor C n).obj Y✝.obj,
          d := (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftComm Y✝.obj 1 n).hom, d_squared := ⋯ }.d

Tactic:
dsimp

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 ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.f) =
    (CategoryTheory.shiftFunctor C n).map f.f ≫
      (CategoryTheory.shiftFunctor C n).map Y✝.d ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj
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
⊢ autoParam
    ({ f := (CategoryTheory.shiftFunctor C n).map (𝟙 X).f, comm := ⋯ }.f =
      (𝟙
          { obj := (CategoryTheory.shiftFunctor C n).obj X.obj,
            d := (CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom, d_squared := ⋯ }).f)
    ext._auto_1

Tactic:
dsimp

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
⊢ autoParam ((CategoryTheory.shiftFunctor C n).map (𝟙 X.obj) = 𝟙 ((CategoryTheory.shiftFunctor C n).obj X.obj))
    ext._auto_1