mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
h₃ : c₃.Rel i₃ (c₃.next i₃)
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, c₃.next i₃) = j'

Tactic:
dsimp [ComplexShape.r]
            rw [← h₂, ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₂ c₂ c₂₃ i₂ h₃]

Goal state after:
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
n : ℤ
⊢ (t.truncGT n).Additive

Tactic:
dsimp only [truncGT]
  infer_instance

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

Goal state before:
pp: C : Type u_1
J : Type u_2
ι : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} J
c : ComplexShape ι
inst✝³ : IsCofiltered J
inst✝² : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝¹ : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
inst✝ : CategoryWithHomology C
q₀ q₁ q₂ : ι
h₀ : c.prev q₁ = q₀
h₂ : c.next q₁ = q₂
j : J
hq₀ : (F ⋙ eval C c q₀).IsEventuallyConstantTo j
hq₁ : (F ⋙ eval C c q₁).IsEventuallyConstantTo j
hq₂ : (F ⋙ eval C c q₂).IsEventuallyConstantTo j
φ : (shortComplexFunctor' C c q₀ q₁ q₂).obj (((Functor.const J).obj cF.pt).obj j) ⟶
  (shortComplexFunctor' C c q₀ q₁ q₂).obj (F.obj j) :=
  (shortComplexFunctor' C c q₀ q₁ q₂).map (cF.π.app j)
this✝ : IsIso φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C c q₀ q₁ q₂).map (cF.π.app j))

Tactic:
have : IsIso φ.τ₃ := isIso_π_f_of_isLimit_of_isEventuallyConstantTo F hcF _ _ hq₂

Goal state after:
C : Type u_1
J : Type u_2
ι : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} J
c : ComplexShape ι
inst✝³ : IsCofiltered J
inst✝² : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
inst✝¹ : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
inst✝ : CategoryWithHomology C
q₀ q₁ q₂ : ι
h₀ : c.prev q₁ = q₀
h₂ : c.next q₁ = q₂
j : J
hq₀ : (F ⋙ eval C c q₀).IsEventuallyConstantTo j
hq₁ : (F ⋙ eval C c q₁).IsEventuallyConstantTo j
hq₂ : (F ⋙ eval C c q₂).IsEventuallyConstantTo j
φ : (shortComplexFunctor' C c q₀ q₁ q₂).obj (((Functor.const J).obj cF.pt).obj j) ⟶
  (shortComplexFunctor' C c q₀ q₁ q₂).obj (F.obj j) :=
  (shortComplexFunctor' C c q₀ q₁ q₂).map (cF.π.app j)
this✝¹ : IsIso φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C c q₀ q₁ q₂).map (cF.π.app j))
Module: Mathlib.CategoryTheory.Category.Factorisation

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
d : Factorisation f✝
f : d ⟶ Factorisation.terminal
⊢ f = d.terminalHom

Tactic:
apply Factorisation.Hom.ext; simp [← f.h_π]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ f i = eqToHom ⋯ ≫ f j ≫ eqToHom ⋯

Tactic:
subst h
  simp

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 ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
⊢ QuasiIsoAt (π K L n₁) i

Tactic:
obtain (hi | rfl) := hi.lt_or_eq
  · rw [quasiIsoAt_iff' _ (i - 1) i (i + 1) (by simp) (by simp)]
    let φ := (shortComplexFunctor' C _ (i - 1) i (i + 1)).map (π K L n₁)
    have : IsIso φ.τ₁ := isIso_π_f ..
    have : IsIso φ.τ₂ := isIso_π_f ..
    have : IsIso φ.τ₃ := isIso_π_f ..
    exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ
  · rw [quasiIsoAt_iff_isIso_homologyMap]
    have : homologyMap (biprod.inl : _ ⟶ mid K L n₁) i = 0 :=
      (ShortComplex.isZero_homology_of_isZero_X₂ _
        (isZero_single_obj_X (.up ℤ) _ _ _ (by lia))).eq_of_src _ _
    refine ⟨homologyMap (σ K L n₁) i, ?_, ?_⟩
    · simp [← homologyMap_id, ← biprod.total, homologyMap_comp, this]
    · simp [← homologyMap_comp, homologyMap_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

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

Tactic:
simp only [precomp_mk, Category.comp_id]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ModelCategory C
X Y : C
inst✝⁴ : IsCofibrant X
inst✝³ : IsCofibrant Y
inst✝² : IsFibrant X
inst✝¹ : IsFibrant Y
f : X ⟶ Y
inst✝ : WeakEquivalence f
g : Y ⟶ X
hg : mk (f ≫ g) = mk (𝟙 X)
⊢ mk (f ≫ g ≫ f) = mk f
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 Y : C
n : ℕ
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y n)

Tactic:
induction n generalizing Y with

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₀ : ι
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
⊢ (𝟙 ((double f hi₀₁).X k₀) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁) ≫ 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₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
id_comp,

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₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
⊢ ((doubleXIso₁ f hi₀₁ h).hom ≫ φ₁) ≫ 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₁ = k₀ 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
⊢ 𝟙 ((double f hi₀₁).X i₀) ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀) = (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
id_comp,

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₁
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
⊢ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀) = (doubleXIso₀ f hi₀₁).hom ≫ φ₀
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
⊢ 𝟙 ((double f hi₀₁).X i₁) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X i₁) = (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Tactic:
id_comp,

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₁
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
⊢ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X i₁) = (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
D₁ D₂ : ComposableArrows (CochainComplex C ℤ) 2
φ : D₁ ⟶ D₂
⊢ (ComposableArrows.functorArrows (CochainComplex C ℤ) 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        φ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            (D₂.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            (D₂.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))).mor₃ =
    ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            (D₁.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            (D₁.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))).mor₃ ≫
      (ComposableArrows.functorArrows (CochainComplex C ℤ) 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        φ

Tactic:
by
    obtain ⟨_, _, _, f, g, rfl⟩ := ComposableArrows.mk₂_surjective D₁
    obtain ⟨_, _, _, f', g', rfl⟩ := ComposableArrows.mk₂_surjective D₂
    have eq := CochainComplex.mappingConeCompTriangle_mor₃_naturality f g f' g' φ
    dsimp [ComposableArrows.Precomp.map] at eq ⊢
    simp only [Category.assoc, ← Functor.map_comp_assoc]
    simp [eq]

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
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p = (F.map P.p).f ≫ (φ.app P.X).f

Tactic:
simp only [obj_obj_p, assoc, ← h]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ (φ.app P.X).f = (F.map P.p).f ≫ (φ.app P.X).f
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 ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : ((n + 1).negOnePow * (n + 1).negOnePow) • Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α

Tactic:
Int.units_mul_self,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
q n : ℤ
α : Cocycle K ((singleFunctor C q).obj X) n
p : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
f : K.X p ⟶ X
hf : Cochain.toSingleMk f h = ↑α
hα : 1 • Cochain.toSingleMk (K.d p' p ≫ f) ⋯ = 0
⊢ ∃ f, ∃ (hf : K.d p' p ≫ f = 0), toSingleMk f h p' hp' hf = α
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 : ℕ
⊢ (F.leftDerived n).map f ≫ (Q.isoLeftDerivedObj F n).hom =
    (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        φ

Tactic:
by
  dsimp [isoLeftDerivedObj, Functor.leftDerived]
  rw [assoc, ← Functor.map_comp_assoc,
    ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality f P Q φ comm F,
    Functor.map_comp, assoc]
  erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.naturality]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Single

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (singleObjApplyIsoOfEq i X i ⋯).inv ≫ (single i).map f i = f ≫ (singleObjApplyIsoOfEq i Y i ⋯).inv

Tactic:
simp [singleObjApplyIsoOfEq, single]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Single

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (single i).map f i ≫ (singleObjApplyIsoOfEq i Y i ⋯).hom = (singleObjApplyIsoOfEq i X i ⋯).hom ≫ f

Tactic:
simp [singleObjApplyIsoOfEq, single]

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

Tactic:
id_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
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) =
    (F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
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 : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₂ :
  (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (lift (𝟙 X) P (projectiveResolution X))
h₁ :
  HomologicalComplex.opcyclesMap
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫
      (projectiveResolution X).fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫
          (projectiveResolution X).fromLeftDerivedZero' F =
    𝟙
        ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).obj
          ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            P.complex)) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F

Tactic:
id_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 : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₂ :
  (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
      (lift (𝟙 X) P (projectiveResolution X))
h₁ :
  HomologicalComplex.opcyclesMap
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift (𝟙 X) P (projectiveResolution X))) 0 ≫
      (projectiveResolution X).fromLeftDerivedZero' F =
    P.fromLeftDerivedZero' F
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫
          (projectiveResolution X).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).homologyι 0 ≫ P.fromLeftDerivedZero' F
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ φ j ≫
      e.inv.app (Y' j) ≫
        (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ =
    e.inv.app (Y j) ≫
      (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫
        𝟙 ((F.obj ((single₀ I).obj X 0)).obj (Y j)) ≫
          (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯

Tactic:
id_comp,

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ φ j ≫
      e.inv.app (Y' j) ≫
        (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ =
    e.inv.app (Y j) ≫
      (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫
        (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m = e.inv.app (X j) ≫ 𝟙 ((F.obj (X j)).obj Y) ≫ e.hom.app (X j) ≫ m

Tactic:
id_comp,

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m = e.inv.app (X j) ≫ e.hom.app (X j) ≫ m