mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
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_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
⊢ ((mapTrifunctor F I₁ I₂ I₃).obj X₁).map φ ≫
      { app := fun x x_1 ↦ ((α.app (X₁ x_1.1)).app (Y₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ } =
    { app := fun x x_1 ↦ ((α.app (X₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ } ≫
      ((mapTrifunctor F' I₁ I₂ I₃).obj X₁).map φ

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
f : K.toGradedObject ⟶ L.toGradedObject
comm₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), c₁.Rel i₁ i₁' → f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ f (i₁', i₂)
comm₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), c₂.Rel i₂ i₂' → f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ f (i₁, i₂')
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ { f := fun i₂ ↦ f (i₁, i₂), comm' := ⋯ } ≫ L.d i₁ i₁' = K.d i₁ i₁' ≫ { f := fun i₂ ↦ f (i₁', i₂), comm' := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
i₂ i₂' : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.X i₁').d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ (K.d i₁ i₁').f i₂'

Tactic:
by

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
⊢ ∀ {i₁ i₁' : ℤ},
    (up ℤ).Rel i₁ i₁' →
      ∀ (i₂ : ℤ),
        (i₁ * i₂).negOnePow * (up ℤ).ε₁ (up ℤ) (up ℤ) (i₁, i₂) = (up ℤ).ε₂ (up ℤ) (up ℤ) (i₂, i₁) * (i₁' * i₂).negOnePow

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i i' : I₂
w : ¬c₂.Rel i i'
⊢ { f := fun j ↦ (K.X j).d i i', comm' := ⋯ } = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i : I₂
⊢ ∀ (i_1 j : I₁), c₁.Rel i_1 j → (f.f i_1).f i ≫ (L.flip.X i).d i_1 j = (K.flip.X i).d i_1 j ≫ (f.f j).f i

Tactic:
by

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
⊢ ∀ (i₁ : ℤ) {i₂ i₂' : ℤ},
    (up ℤ).Rel i₂ i₂' →
      (i₁ * i₂).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (i₁, i₂) = (up ℤ).ε₁ (up ℤ) (up ℤ) (i₂, i₁) * (i₁ * i₂').negOnePow

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
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_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
⊢ (mapTrifunctor F I₁ I₂ I₃).map φ ≫
      { app := fun X₂ ↦ { app := fun x x_1 ↦ ((α.app (Y₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ },
        naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun x x_1 ↦ ((α.app (X₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ },
        naturality := ⋯ } ≫
      (mapTrifunctor F' I₁ I₂ I₃).map φ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ ExtraDegeneracy.s f S (n + 1) ≫ f.augmentedCechNerve.left.δ i.succ =
    f.augmentedCechNerve.left.δ i ≫ ExtraDegeneracy.s f S n

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      { f := fun j ↦ (f.f j).f i, comm' := ⋯ } ≫ L.flip.d i j =
        K.flip.d i j ≫ { f := fun j_1 ↦ (f.f j_1).f j, comm' := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ : I₁
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      (Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i₁).X i)).hom ≫
          (((flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁).obj K).X i₁).d i j =
        (((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i₁).d i j ≫
          (Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i₁).X j)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
⊢ ∀ (i j : I₁),
    c₁.Rel i j →
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i).X x)) ⋯).hom ≫
          ((flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁).obj K).d i j =
        ((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).d i j ≫
          (Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X j).X x)) ⋯).hom

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
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_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
⊢ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ = 𝟙 (mapTrifunctor F I₁ I₂ I₃)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
⊢ ∀ {X Y : HomologicalComplex₂ C c₁ c₂} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex₂ C c₁ c₂)).map f ≫
        (Hom.isoOfComponents
            (fun i₁ ↦ Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj Y).X i₁).X x)) ⋯)
            ⋯).hom =
      (Hom.isoOfComponents
            (fun i₁ ↦ Hom.isoOfComponents (fun x ↦ Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj X).X i₁).X x)) ⋯)
            ⋯).hom ≫
        (flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁).map f

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
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_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
⊢ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ = 𝟙 (mapTrifunctor F' I₁ I₂ I₃)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₂ c₁
i₂ : I₂
⊢ ∀ (i j : I₁),
    c₁.Rel i j →
      (Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i₂).X i)).hom ≫
          (((𝟭 (HomologicalComplex₂ C c₂ c₁)).obj K).X i₂).d i j =
        (((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i₂).d i j ≫
          (Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i₂).X j)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₂ c₁
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i).X x)) ⋯).hom ≫
          ((𝟭 (HomologicalComplex₂ C c₂ c₁)).obj K).d i j =
        ((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).d i j ≫
          (Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X j).X x)) ⋯).hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
⊢ ∀ {X Y : HomologicalComplex₂ C c₂ c₁} (f : X ⟶ Y),
    (flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).map f ≫
        (Hom.isoOfComponents
            (fun i₂ ↦
              Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj Y).X i₂).X x)) ⋯)
            ⋯).hom =
      (Hom.isoOfComponents
            (fun i₂ ↦
              Hom.isoOfComponents (fun x ↦ Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj X).X i₂).X x)) ⋯)
            ⋯).hom ≫
        (𝟭 (HomologicalComplex₂ C c₂ c₁)).map f

Tactic:
by

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₁ c₁ c₁₂ (i₂, i₁) = c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂'

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
⊢ (K.X x₁).X x₂ = (K.X y₁).X y₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ ExtraDegeneracy.s f S n ≫ f.augmentedCechNerve.left.σ i.succ =
    f.augmentedCechNerve.left.σ i ≫ ExtraDegeneracy.s f S (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ point.obj X ⟶ (AlternatingFaceMapComplex.obj (drop.obj X)).X 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂

Tactic:
by

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₂ c₁ c₁₂ (i₂, i₁) = c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂

Tactic:
by

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₂ c₁ c₁₂
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c₁₂
inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂
i₁ : I₁
i₂ : I₂
⊢ c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h'

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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} C₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p f₁ f₂ f₃ j =
    ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫ ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) = 0

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ : I₁
i₂ i₂' : I₂
h₂ : ¬c₂.Rel i₂ i₂'
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') = 0

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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} C₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
Y : C₄
j : J
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ'
⊢ φ = φ'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      i =
    (((dNext i) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD i) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f i

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
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_3} C₃
inst✝³ : Category.{v_4, u_4} C₄
inst✝² : Category.{v_5, u_5} C₁₂
inst✝¹ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
⊢ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) = 𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s' ≫
      AlternatingFaceMapComplex.ε.app X =
    𝟙 ((ChainComplex.single₀ C).obj (point.obj X))

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) ≠ i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ = 0

Tactic:
by

Goal state after: