mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Ext

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
x : Opposite.unop (Opposite.op ((ProjectiveResolution.self X).complex.X (n + 1))) ⟶ Y
⊢ n + 1 ≠ 0

Tactic:
simp

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
⊢ (Iso.refl
          { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
              g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.X₂).hom ≫
      { X₁ := syzygies (Projective.π Z), X₂ := over Z, X₃ := Z, f := d (Projective.π Z), g := Projective.π Z,
          zero := ⋯ }.g =
    { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
          g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.g ≫
      (Iso.refl
          { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
              g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.X₃).hom

Tactic:
simp

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
j : J
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (single j ⋙ eval j).map f ≫ (singleObjApplyIso j Y).hom = (singleObjApplyIso j X).hom ≫ (𝟭 C).map f

Tactic:
simp

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 : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp

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 : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)).f 0 ≫ (projectiveResolution Y).π.f 0 =
    (projectiveResolution X).π.f 0 ≫ f

Tactic:
simp

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 : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ (lift (𝟙 X) P (projectiveResolution X)).f 0 ≫ (projectiveResolution X).π.f 0 = P.π.f 0 ≫ 𝟙 X

Tactic:
simp

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

Goal state before:
pp: case pos
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'
j' : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j')
h : (0, j') ∈ p ⁻¹' {j'}
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j') ⟨(0, j'), h⟩ ≫
      e.inv.app (Y j') ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j') ≫ s.inj ⟨(0, j'), ⋯⟩ =
    s.inj ⟨(0, j'), h⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.map f ≫ (Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.obj Y)).hom =
      (Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.obj X)).hom ≫ ((functor J C ⋙ inverse J C).obj x✝).X₁.map f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.map f ≫ (Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj Y)).hom =
      (Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj X)).hom ≫ ((functor J C ⋙ inverse J C).obj x✝).X₂.map f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.map f ≫ (Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.obj Y)).hom =
      (Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.obj X)).hom ≫ ((functor J C ⋙ inverse J C).obj x✝).X₃.map f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝¹ : J ⥤ ShortComplex C
x✝ : J
⊢ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₁).hom ≫ (((𝟭 (J ⥤ ShortComplex C)).obj x✝¹).obj x✝).f =
    (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).f ≫ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₂).hom

Tactic:
simp

Goal state after:
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
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i j : I
hij : c.Rel i j
⊢ c.π c c (0, j) = j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝¹ : J ⥤ ShortComplex C
x✝ : J
⊢ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₂).hom ≫ (((𝟭 (J ⥤ ShortComplex C)).obj x✝¹).obj x✝).g =
    (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).g ≫ (Iso.refl (((inverse J C ⋙ functor J C).obj x✝¹).obj x✝).X₃).hom

Tactic:
simp

Goal state after:
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
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i j : I
hij : c.Rel i j
⊢ c.π c c (j, 0) = j

Tactic:
simp

Goal state after:
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₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
inst✝² : X₁.HasTensor Y₁
inst✝¹ : X₂.HasTensor Y₂
inst✝ : X₃.HasTensor Y₃
x✝ i₁✝ i₂✝ : I
hi✝ : i₁✝ + i₂✝ = x✝
⊢ ιTensorObj X₁ Y₁ i₁✝ i₂✝ x✝ hi✝ ≫ (tensorHom f₁ g₁ ≫ tensorHom f₂ g₂) x✝ =
    ιTensorObj X₁ Y₁ i₁✝ i₂✝ x✝ hi✝ ≫ tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂) x✝

Tactic:
simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst✝¹⁵ : Category.{v_1, u_1} C₁
inst✝¹⁴ : Category.{v_2, u_2} C₂
inst✝¹³ : Category.{v_3, u_3} C₃
inst✝¹² : Category.{v_4, u_4} D
inst✝¹¹ : Zero I₂
inst✝¹⁰ : DecidableEq I₂
inst✝⁹ : HasInitial C₂
F₁ : C₁ ⥤ C₂ ⥤ C₁
F₂ : C₂ ⥤ C₃ ⥤ C₃
G : C₁ ⥤ C₃ ⥤ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst✝⁸ : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst✝⁷ : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂
inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π
inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃
inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π
inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃
inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃
inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ τ.ρ₁₂.p (i₁, 0) = i₁

Tactic:
simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst✝¹⁵ : Category.{v_1, u_1} C₁
inst✝¹⁴ : Category.{v_2, u_2} C₂
inst✝¹³ : Category.{v_3, u_3} C₃
inst✝¹² : Category.{v_4, u_4} D
inst✝¹¹ : Zero I₂
inst✝¹⁰ : DecidableEq I₂
inst✝⁹ : HasInitial C₂
F₁ : C₁ ⥤ C₂ ⥤ C₁
F₂ : C₂ ⥤ C₃ ⥤ C₃
G : C₁ ⥤ C₃ ⥤ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst✝⁸ : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst✝⁷ : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂
inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π
inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃
inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π
inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃
inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃
inst✝ : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ τ.ρ₂₃.p (0, i₃) = i₃

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
by
  subst h
  exact (X.exact₃' n₀ n₁ hn₁ (mk₂ f g)).zero 0

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
⊢ f ≫ inv f = 𝟙 i₀

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} ι
inst✝¹ : Abelian C
X : SpectralObject C ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
this : IsIso φ
⊢ f ≫ inv f = 𝟙 i₀

Tactic:
simp

Goal state after:
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
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
n : ℤ
⊢ (X.H n).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ f g n (n + 1) ⋯ = 0

Tactic:
simp

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

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₀ 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₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ autoParam ((twoδ₁Toδ₀ f₁ f₂ (f₁ ≫ f₂) ⋯ ≫ twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃).app 1 = (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄).app 0)
    δ_naturality._auto_1

Tactic:
simp

Goal state after:
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
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
n : ℤ
⊢ X.δ f g (n - 1) n ⋯ ≫ (X.H n).map (twoδ₂Toδ₁ f g fg h) = 0

Tactic:
simp

Goal state after:
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
inst✝⁸ : DecidableEq I
inst✝⁷ : HasInitial C
inst✝⁶ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁵ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
X₁ X₃ : GradedObject I C
inst✝⁴ : X₁.HasTensor X₃
inst✝³ : (tensorObj X₁ tensorUnit).HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj tensorUnit X₃)
inst✝¹ : X₁.HasGoodTensor₁₂Tensor tensorUnit X₃
inst✝ : X₁.HasGoodTensorTensor₂₃ tensorUnit X₃
⊢ ∀ (X₁ X₃ : C),
    (((curriedAssociatorNatIso C).hom.app X₁).app (𝟙_ C)).app X₃ ≫
        ((curriedTensor C).obj X₁).map ((leftUnitorNatIso C).hom.app X₃) =
      ((curriedTensor C).map ((rightUnitorNatIso C).hom.app X₁)).app X₃

Tactic:
simp

Goal state after:
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₂ f₃ n₀ n₁ ⋯ ≫ X.δ f₁ f₂ n₁ (n₁ + 1) ⋯ = 0

Tactic:
simp

Goal state after:
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₂ f₃ (n₀ - 1) n₀ ⋯ ≫ X.δ f₁ f₂ n₀ n₁ hn₁ = 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ z ≫ X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁ = 0

Tactic:
← X.Ψ_fromOpcycles f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ hn₁,

Goal state after:
case refine_1
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ z ≫ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = 0
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

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₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ 𝟙 i₁ ≫ f₂ = f₂

Tactic:
simp

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

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₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ 𝟙 i₀ ≫ f₁ = f₁

Tactic:
simp

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

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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
⊢ (mk₁ (𝟙 i)).map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ (asIso f).hom =
    (Iso.refl ((mk₁ (𝟙 i)).obj' 0 homMk₁._proof_4)).hom ≫ (mk₁ f).map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
simp

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

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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl ((mk₁ (𝟙 i)).obj' 0 homMk₁._proof_4)) (asIso f) ⋯
⊢ 𝟙 i ≫ 𝟙 i = 𝟙 i

Tactic:
simp

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ X.iCycles f₁ f₂ n₁ ≫ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g = 0

Tactic:
simp

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯ ≫ cokernel.π (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) = 0

Tactic:
simp

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hi : IsLimit (KernelFork.ofι (X.kernelSequenceCycles f₁ f₂ n₁ n₂ hn₂).f ⋯) := ⋯.fIsKernel
this : hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).f ⋯) = X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯
⊢ (parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).map
        WalkingParallelPairHom.right ≫
      (Iso.refl
          ((parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.one)).hom =
    (Iso.refl
          ((parallelPair (hi.lift (KernelFork.ofι (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ⋯)) 0).obj
            WalkingParallelPair.zero)).hom ≫
      (parallelPair (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯) 0).map WalkingParallelPairHom.right

Tactic:
simp

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ = 0

Tactic:
simp [πE]

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (Iso.refl (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁).hom ≫
      { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁, X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles,
          X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology,
          f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles,
          g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyπ, zero := ⋯ }.f =
    (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).f ≫ (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).symm.hom

Tactic:
simp

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯).symm.hom ≫
      { X₁ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₁, X₂ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).cycles,
          X₃ := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homology,
          f := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).toCycles,
          g := (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).homologyπ, zero := ⋯ }.g =
    (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ≫
      (Iso.refl (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₃).hom

Tactic:
simp [πE]

Goal state after: