mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
⊢ ∃ F, quasiIsoLE n₁ F ∧ isIsoLE n₀ F

Tactic:
obtain ⟨F₁, h₁, h₂, _⟩ := step₁ f n₀ n₁ hf
  obtain ⟨F₂, h₃, h₄⟩ := step₂ F₁.obj.ι n₀ n₁ h₁
  refine ⟨.mk { mid := F₂.obj.mid, ι := F₂.obj.ι, π := F₂.obj.π ≫ F₁.obj.π }
    ⟨by dsimp; infer_instance, MorphismProperty.comp_mem _ _ _ F₂.property.2 F₁.property.2⟩,
    ⟨h₃, fun i hi ↦ ?_⟩⟩
  have := h₂ i hi
  have := h₄ i (by lia)
  dsimp
  infer_instance

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α

Tactic:
exact fun _ => IsRightDerivedFunctor.isLeftKanExtension RF α W

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

Goal state before:
pp: case refine_1
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
f : X₁ ⟶ X₂
φ : 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 φ)
eq : F.map f ≫ s.ι.app (CostructuredArrow.mk φ) = s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
⊢ (e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))

Tactic:
assoc

Goal state after:
case refine_1
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
f : X₁ ⟶ X₂
φ : 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 φ)
eq : F.map f ≫ s.ι.app (CostructuredArrow.mk φ) = s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
⊢ (e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
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 ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))

Tactic:
assoc

Goal state after:
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 ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))
Module: Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
Y : C
p : (isInjective C).LimitOfShape (Discrete J) Y
this : ∀ (j : J), Injective (p.diag.obj { as := j })
X✝ Y✝ : C
q : X✝ ⟶ Y
i : X✝ ⟶ Y✝
x✝¹ : Mono i
x✝ : Discrete J
j : J
⊢ (i ≫
        p.isLimit.lift
          { pt := Y✝,
            π :=
              Discrete.natTrans fun x ↦
                match x with
                | { as := j } => Injective.factorThru (q ≫ p.π.app { as := j }) i }) ≫
      { pt := Y, π := p.π }.π.app { as := j } =
    q ≫ { pt := Y, π := p.π }.π.app { as := j }

Tactic:
by simp [p.isLimit.fac]

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✝⁴ : L.IsLocalizedEquivalence
inst✝³ : R.IsLocalizedEquivalence
inst✝² : R.functor.EssSurj
inst✝¹ : T.IsRightDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.hom
⊢ B.IsRightDerivabilityStructure

Tactic:
rw [isRightDerivabilityStructure_iff_op]
  let iso' : T.op.functor ⋙ R.op.functor ≅ L.op.functor ⋙ B.op.functor := NatIso.op iso.symm
  have : TwoSquare.GuitartExact iso'.inv :=
    inferInstanceAs (TwoSquare.op iso.hom).GuitartExact
  exact isLeftDerivabilityStructure_of_isLocalizedEquivalence iso'

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
⊢ (quotient (InjectiveObject C)).IsLocalization
    ((CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus)

Tactic:
rw [inverseImage_quasiIso_mapCochainComplexPlus_injectiveObjectι]

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
⊢ (quotient (InjectiveObject C)).IsLocalization
    ((HomologicalComplex.homotopyEquivalences (InjectiveObject C) (ComplexShape.up ℤ)).inverseImage
      (CochainComplex.Plus.ι (InjectiveObject C)))
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 : DifferentialObject S C
⊢ (eqToHom ⋯).f = eqToHom ⋯

Tactic:
eqToHom_refl,

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 : DifferentialObject S C
⊢ (𝟙 X).f = eqToHom ⋯
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:
by
        dsimp
        slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f]
        slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp]
        rw [Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i ↦ separatingFamily c (fun x ↦ X) (PUnit.unit, i)
⊢ IsSeparator (∐ fun i ↦ separatingFamily c (fun x ↦ X) (PUnit.unit, i))

Tactic:
refine isSeparator_of_isColimit_cofan
    (isSeparating_separatingFamily c (X := fun (_ : Unit) ↦ X) (by simpa using! hX))
      (c := Cofan.mk (∐ φ) (fun ⟨_, i⟩ ↦ Sigma.ι φ i)) ?_

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝³ : c.HasNoLoop
inst✝² : HasCoproductsOfShape ι C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
hX : IsSeparator X
φ : ι → HomologicalComplex C c := fun i ↦ separatingFamily c (fun x ↦ X) (PUnit.unit, i)
⊢ IsColimit
    (Cofan.mk (∐ φ) fun x ↦
      match x with
      | (fst, i) => Sigma.ι φ i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
⊢ toSingleMk f h p' hp' hf ∈ coboundaries K ((singleFunctor C q).obj X) n ↔ ∃ g, K.d p p'' ≫ g = f

Tactic:
rw [mem_coboundaries_iff _ (n - 1) (by simp)]
  constructor
  · rintro ⟨α, hα⟩
    obtain ⟨g, hg⟩ := Cochain.toSingleMk_surjective α p'' (by lia)
    refine ⟨n.negOnePow • g, ?_⟩
    rw [← hg, toSingleMk_coe, Cochain.δ_toSingleMk _ _ _ _ h] at hα
    exact (Cochain.toSingleEquiv h).symm.injective (by simpa)
  · rintro ⟨g, rfl⟩
    exact ⟨n.negOnePow • Cochain.toSingleMk g (by lia),
      by simp [Cochain.δ_toSingleMk _ _ _ _ h, smul_smul]⟩

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 ≫
        (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

Tactic:
assoc

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
⊢ (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:
assoc

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 ℕ)).obj
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
        (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
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)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (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:
assoc

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)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (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
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K : HomologicalComplex C c
⊢ (forget C c).map (ρ_ K).hom =
    (𝟙 ((forget C c).obj K ⊗ (forget C c).obj (𝟙_ (HomologicalComplex C c))) ≫
        (𝟙 ((forget C c).obj K) ⊗ₘ (tensorUnitIso C c).inv)) ≫
      (ρ_ ((forget C c).obj K)).hom

Tactic:
assoc

Goal state after:
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K : HomologicalComplex C c
⊢ (forget C c).map (ρ_ K).hom =
    𝟙 ((forget C c).obj K ⊗ (forget C c).obj (𝟙_ (HomologicalComplex C c))) ≫
      (𝟙 ((forget C c).obj K) ⊗ₘ (tensorUnitIso C c).inv) ≫ (ρ_ ((forget C c).obj K)).hom
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = (f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h

Tactic:
assoc

Goal state after:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).Exact

Tactic:
obtain rfl : n₀ = n₁ - 1 := by lia
  apply ShortComplex.exact_cokernel

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯

Tactic:
have hx₂' := hx₂ =≫ X.ιE ..

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯ = 0
hx₂' :
  (x₂ ≫ X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯ =
    0 ≫ X.ιE f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯