mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
this :
  Triangle.mk o.m₃.op o.m₁.op
      ((opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
        (shiftFunctor Cᵒᵖ 1).map
          ((((shiftFunctor C 1).map w₂₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂) ≫ v₁₂)) ∈
    Pretriangulated.distinguishedTriangles
⊢ w₂₃ ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂ =
    (opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
      (shiftFunctor Cᵒᵖ 1).map ((shiftFunctor C 1).map w₂₃.unop).op ≫
        (shiftFunctor Cᵒᵖ 1).map ((opShiftFunctorEquivalence C 1).unitIso.inv.app X₂ ≫ v₁₂)

Tactic:
Functor.map_comp,

Goal state after:
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
this :
  Triangle.mk o.m₃.op o.m₁.op
      ((opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
        (shiftFunctor Cᵒᵖ 1).map
          ((((shiftFunctor C 1).map w₂₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂) ≫ v₁₂)) ∈
    Pretriangulated.distinguishedTriangles
⊢ w₂₃ ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂ =
    (opShiftFunctorEquivalence C 1).counitIso.inv.app Z₂₃ ≫
      (shiftFunctor Cᵒᵖ 1).map ((shiftFunctor C 1).map w₂₃.unop).op ≫
        (shiftFunctor Cᵒᵖ 1).map ((opShiftFunctorEquivalence C 1).unitIso.inv.app X₂) ≫ (shiftFunctor Cᵒᵖ 1).map v₁₂
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 Y : C
f : X ⟶ Y
a b : ℤ
h : a + 1 = b
⊢ IsIso ((t.truncLE a).map f) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLEι a).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z b

Tactic:
by
  subst h
  apply isIso_truncLT_map_iff

Goal state after:
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
K : CochainComplex C ℤ
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ ∃ Z a b,
    HomotopyCategory.plus C Z ∧
      HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ

Tactic:
HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ ∃ Z a b,
    HomotopyCategory.plus C Z ∧
      HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (K.truncGE n))

Tactic:
HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ HomologicalComplex.Acyclic (K.truncGE 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
X : C
a b : ℤ
hn : b ≤ a
this : t.IsGE ((t.truncGE a).obj X) a
⊢ t.IsGE ((t.truncGE a).obj X) b

Tactic:
exact t.isGE_of_ge _ _ a (by lia)

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
A B : Plus C
i : A ⟶ B
inst✝ : Cofibration i
⊢ Mono i

Tactic:
rwa [← cofibration_iff]

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

Goal state before:
pp: case inr
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝¹ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝ : ∀ (n : ℤ), Injective ((kernel p).X n)
this : (kernel p).IsKInjective
h✝ : QuasiIso p
⊢ ∃ α, δ 0 1 α = ↑β

Tactic:
refine IsKInjective.eq_δ_of_cocycle' β ?_ 0 (by simp)
        have := hp.epi
        have : (ShortComplex.mk _ _ (kernel.condition p)).ShortExact :=
          { exact := ShortComplex.exact_kernel p }
        exact this.acyclic_X₁ (by dsimp; infer_instance)

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f : { obj := K, property := ⋯ }.obj ⟶ { obj := L, property := ⋯ }.obj
d : ℤ
left✝² : K.IsStrictlyGE (d + 1)
right✝ : L.IsStrictlyGE d
K' : CochainComplex C ℤ
w✝ : K'.IsStrictlyGE d
i : { obj := K, property := ⋯ }.obj ⟶ K'
p : K' ⟶ { obj := L, property := ⋯ }.obj
left✝¹ : Mono i
left✝ : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
⊢ Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) { hom := f })

Tactic:
exact ⟨{
      Z := ⟨K', d, inferInstance⟩
      i := ObjectProperty.homMk i
      p := ObjectProperty.homMk p
      hi :=
        ⟨by rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff],
          by assumption⟩
      hp := hp }⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
⊢ Mono (homologyMap (ι f n₁) n₁)

Tactic:
rw [mono_homologyMap_iff_up_to_refinements _ n₀ n₁ (n₁ + 1) (by simp; lia) (by simp)]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X n₁),
    x₂ ≫ K.d n₁ (n₁ + 1) = 0 →
      ∀ (y₁ : A ⟶ (mid K L n₁).X n₀),
        x₂ ≫ (ι f n₁).f n₁ = y₁ ≫ (mid K L n₁).d n₀ n₁ → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d n₀ n₁
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : Cylinder X.obj
left✝ : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject C ⥤ (weakEquivalences (FibrantObject C)).Localization := (weakEquivalences (FibrantObject C)).Q
this : L.map (homMk P.i₀) = L.map (homMk P.i₁)
⊢ L.map f = L.map g

Tactic:
by
    simp only [show f = homMk P.i₀ ≫ homMk h.h by cat_disch,
      show g = homMk P.i₁ ≫ homMk h.h by cat_disch, Functor.map_comp, this]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
e : (w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂ ≅
  w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
  NatIso.ofComponents (fun f ↦ StructuredArrow.isoMk (α.symm.app f.right) ⋯) ⋯
⊢ ((w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂).Initial

Tactic:
rw [Functor.initial_natIso_iff e]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
X₂ : D₁
e : (w.whiskerVertical α.hom β.inv).structuredArrowDownwards X₂ ≅
  w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
  NatIso.ofComponents (fun f ↦ StructuredArrow.isoMk (α.symm.app f.right) ⋯) ⋯
⊢ (w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor).Initial
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝² : L.IsEquivalence
inst✝¹ : R.IsEquivalence
inst✝ : IsIso w.natTrans
⊢ w.GuitartExact

Tactic:
by
  rw [guitartExact_iff_initial]
  intro X₂
  have := StructuredArrow.isEquivalence_post X₂ T R
  have : (Comma.mapRight _ w : StructuredArrow (R.obj X₂) _ ⥤ _).IsEquivalence :=
    (Comma.mapRightIso _ (asIso w)).isEquivalence_functor
  have := StructuredArrow.isEquivalence_pre (R.obj X₂) L B
  dsimp only [structuredArrowDownwards]
  infer_instance

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
⊢ (localizerMorphism C).arrow.HasRightResolutions

Tactic:
LocalizerMorphism.hasRightResolutions_arrow_iff_of_equivalences
    (T := localizerMorphism C) (B := FibrantObject.localizerMorphism (Plus C))
    (R := .id _) (L := fibrantObjectLocalizerMorphism C) (Iso.refl _)

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
⊢ (FibrantObject.localizerMorphism (Plus C)).arrow.HasRightResolutions
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0

Tactic:
HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
x✝ : K.IsKProjective
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : L.Acyclic
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0
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; lia

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 : DifferentialObject S C
⊢ (F.map X.d ≫ η.app X.obj) ≫ (shiftFunctor D 1).map (F.map X.d ≫ η.app X.obj) = 0

Tactic:
Functor.map_comp,

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 : DifferentialObject S C
⊢ (F.map X.d ≫ η.app X.obj) ≫ (shiftFunctor D 1).map (F.map X.d) ≫ (shiftFunctor D 1).map (η.app X.obj) = 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 : DifferentialObject S C
⊢ ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom) =
    0

Tactic:
Functor.map_comp,

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 ≫ (shiftComm X.obj 1 n).hom) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map X.d) ≫
        (CategoryTheory.shiftFunctor C 1).map (shiftComm X.obj 1 n).hom =
    0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ (ComplexShape.embeddingUpIntLE (-1)).f n = Int.negSucc n

Tactic:
dsimp; lia

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 K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n + 1) = Int.negSucc (n + 1)

Tactic:
dsimp; lia

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
n : ℕ
⊢ Projective ((ofComplex Z).X n)

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

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
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
          (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ) ≫
      (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,

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 (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ)) ≫
      (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
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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
      ((P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
          (P.isoLeftDerivedToHomotopyCategoryObj G).inv) =
    ((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 ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Tactic:
Functor.map_comp,

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
          (P.isoLeftDerivedToHomotopyCategoryObj G).inv) =
    ((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 ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv