mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ L₁ : HomologicalComplex C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex C c
⊢ (forget C c).map (f ▷ K₂) =
    (Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj K₂)).inv ≫
      (forget C c).map f ▷ (forget C c).obj K₂ ≫ (Iso.refl ((forget C c).obj L₁ ⊗ (forget C c).obj K₂)).hom

Tactic:
by

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
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₁ L₁ K₂ L₂ : HomologicalComplex C c
f : K₁ ⟶ L₁
g : K₂ ⟶ L₂
⊢ (forget C c).map (f ⊗ₘ g) =
    (Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj K₂)).inv ≫
      ((forget C c).map f ⊗ₘ (forget C c).map g) ≫ (Iso.refl ((forget C c).obj L₁ ⊗ (forget C c).obj L₂)).hom

Tactic:
by

Goal state after:
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'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
⊢ φ ≫ (mapBifunctorRightUnitor F Y e p hp X').inv =
    (mapBifunctorRightUnitor F Y e p hp X).inv ≫ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y))

Tactic:
by

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
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₁ K₂ K₃ : HomologicalComplex C c
⊢ (forget C c).map (α_ K₁ K₂ K₃).hom =
    (((Iso.refl ((forget C c).obj (K₁ ⊗ K₂) ⊗ (forget C c).obj K₃)).symm ≪≫
          ((Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj K₂)).symm ⊗ᵢ Iso.refl ((forget C c).obj K₃))) ≪≫
        α_ ((forget C c).obj K₁) ((forget C c).obj K₂) ((forget C c).obj K₃) ≪≫
          (Iso.refl ((forget C c).obj K₁) ⊗ᵢ Iso.refl ((forget C c).obj K₂ ⊗ (forget C c).obj K₃)) ≪≫
            Iso.refl ((forget C c).obj K₁ ⊗ (forget C c).obj (K₂ ⊗ K₃))).hom

Tactic:
by

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
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 =
    (((Iso.refl ((forget C c).obj (𝟙_ (HomologicalComplex C c)) ⊗ (forget C c).obj K)).symm ≪≫
          ((tensorUnitIso C c).symm ⊗ᵢ Iso.refl ((forget C c).obj K))) ≪≫
        λ_ ((forget C c).obj K)).hom

Tactic:
by

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₂ Y₁ Y₂ : GradedObject I C
e₁ : X₁ ≅ Y₁
e₂ : X₂ ≅ Y₂
inst✝ : X₁.HasTensor X₂
⊢ Y₁.HasTensor Y₂

Tactic:
by

Goal state after:
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'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
⊢ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) ≫ (mapBifunctorRightUnitor F Y e p hp X').hom =
    (mapBifunctorRightUnitor F Y e p hp X).hom ≫ φ

Tactic:
by

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
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 =
    (((Iso.refl ((forget C c).obj K ⊗ (forget C c).obj (𝟙_ (HomologicalComplex C c)))).symm ≪≫
          (Iso.refl ((forget C c).obj K) ⊗ᵢ (tensorUnitIso C c).symm)) ≪≫
        ρ_ ((forget C c).obj K)).hom

Tactic:
by

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst✝ : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
⊢ r (i₁, 0, i₃) = π (i₁, i₃)

Tactic:
by

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₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
j : I
f g : tensorObj X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
⊢ f = g

Tactic:
by

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₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
k : I
f : (i₁ i₂ : I) → i₁ + i₂ = k → (X₁ i₁ ⊗ X₂ i₂ ⟶ A)
i₁ i₂ : I
hi : i₁ + i₂ = k
⊢ ιTensorObj X₁ X₂ i₁ i₂ k hi ≫ tensorObjDesc f = f i₁ i₂ hi

Tactic:
by

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₂ 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₁ ⊗ₘ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h

Tactic:
by

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 Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ tensorHom (𝟙 X) (𝟙 Y) = 𝟙 (tensorObj X Y)

Tactic:
by

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₃
⊢ tensorHom f₁ g₁ ≫ tensorHom f₂ g₂ = tensorHom (f₁ ≫ f₂) (g₁ ≫ g₂)

Tactic:
by

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₂ Y₁ Y₂ : GradedObject I C
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
⊢ tensorHom e.hom e'.hom ≫ tensorHom e.inv e'.inv = 𝟙 (tensorObj X₁ Y₁)

Tactic:
by

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₂ Y₁ Y₂ : GradedObject I C
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
⊢ tensorHom e.inv e'.inv ≫ tensorHom e.hom e'.hom = 𝟙 (tensorObj X₂ Y₂)

Tactic:
by

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
⊢ r (i₁, 0, i₃) = j

Tactic:
by

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₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝² : X₁.HasTensor Y₁
inst✝¹ : X₂.HasTensor Y₂
inst✝ : X₂.HasTensor Y₁
⊢ tensorHom f g = whiskerRight f Y₁ ≫ whiskerLeft X₂ g

Tactic:
by

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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ i₁ + (i₂ + i₃) = j

Tactic:
by

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:
by

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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ i₁ + i₂₃ = j

Tactic:
by

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₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₂₃ : I
h' : i₂ + i₃ = i₂₃
⊢ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h' ≫ ιTensorObj X₁ (tensorObj X₂ X₃) i₁ i₂₃ j ⋯

Tactic:
by

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 ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
⊢ (mk₂ f g).map' 1 2 _proof_246✝ _proof_247✝ ≫ β.app 1 = α.app 1 ≫ (mk₂ f' g').map' 1 2 _proof_246✝ _proof_247✝

Tactic:
by

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 ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α

Tactic:
by

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.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g fg h) = 0

Tactic:
by

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
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom f₁ (tensorHom f₂ f₃) j =
    (f₁ i₁ ⊗ₘ f₂ i₂ ⊗ₘ f₃ i₃) ≫ ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Tactic:
by

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

Tactic:
by

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

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.sc₁ f g fg h n₀ n₁ hn₁).Exact

Tactic:
by

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:
by

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₀ : ℤ
⊢ (X.sc₂ f g fg h n₀).Exact

Tactic:
by

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.sc₃ f g fg h n₀ n₁ hn₁).Exact

Tactic:
by

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₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g
⊢ f = g

Tactic:
by

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

Tactic:
by

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
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ i₁₂ + i₃ = j

Tactic:
by

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:
by

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₃ : GradedObject I C
inst✝¹ : X₁.HasTensor X₂
inst✝ : (tensorObj X₁ X₂).HasTensor X₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h =
    ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h' ▷ X₃ i₃ ≫ ιTensorObj (tensorObj X₁ X₂) X₃ i₁₂ i₃ j ⋯

Tactic:
by

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₀) ⋯
⊢ IsIso φ

Tactic:
by

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
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom (tensorHom f₁ f₂) f₃ j =
    ((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫ ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Tactic:
by

Goal state after: