mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
⊢ objEquiv
      ((ConcreteCategory.hom
            ((↾fun f ↦
                objEquiv.symm
                  (SimplexCategory.Hom.mk
                    { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
              SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1)).toFun
        x) =
    objEquiv
      ((ConcreteCategory.hom
            (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫ ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0))).toFun
        x)

Tactic:
ext j

Goal state after:
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
j : Fin ((unop (op ⦋0⦌)).len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom
          (objEquiv
            ((ConcreteCategory.hom
                  ((↾fun f ↦
                      objEquiv.symm
                        (SimplexCategory.Hom.mk
                          { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
                    SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1)).toFun
              x)))
        j) =
    ↑((SimplexCategory.Hom.toOrderHom
          (objEquiv
            ((ConcreteCategory.hom
                  (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫
                    ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0))).toFun
              x)))
        j)
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
⊢ ExtraDegeneracy.s f S 0 ≫
      WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
        ⋯ =
    (WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯

Tactic:
ext j

Goal state after:
case a
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
j : Fin 1
⊢ (ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j

case a
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
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.base fun x ↦ f.hom
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) ≫
      WidePullback.lift (WidePullback.base fun x ↦ f.hom)
        (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯ =
    WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1)) ⋯ ≫
      ExtraDegeneracy.s f S n

Tactic:
ext j

Goal state after:
case a
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)
j : Fin (n + 1 + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) j

case a
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) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.base fun x ↦ f.hom
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₁₂
p q : ℤ
⊢ (p * q).negOnePow = (p * q + q + q).negOnePow

Tactic:
Int.negOnePow_add,

Goal state after:
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₁₂
p q : ℤ
⊢ (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow
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₁₂
p q : ℤ
⊢ (p * q).negOnePow = (p * q + q).negOnePow * q.negOnePow

Tactic:
Int.negOnePow_add,

Goal state after:
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₁₂
p q : ℤ
⊢ (p * q).negOnePow = (p * q).negOnePow * q.negOnePow * q.negOnePow
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:
ext j

Goal state after:
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'
j : I₁
⊢ { f := fun j ↦ (K.X j).d i i', comm' := ⋯ }.f j = Hom.f 0 j
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 ≫
      WidePullback.lift (WidePullback.base fun x ↦ f.hom)
        (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯ =
    WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1)) ⋯ ≫
      ExtraDegeneracy.s f S (n + 1)

Tactic:
ext j

Goal state after:
case a
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)
j : Fin (n + 1 + 1 + 1)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x ↦ f.hom) j

case a
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 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.base fun x ↦ f.hom
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
inst✝ :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
⊢ mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j ≫ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j =
    mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j ≫ mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j

Tactic:
ext i₁ i₂ i₃ h

Goal state after:
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
inst✝ :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j ≫ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j =
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j ≫ mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : TotalComplexShape c₂ c₁ c
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c
⊢ K.flip.HasTotal c ↔ K.HasTotal c

Tactic:
by
  constructor
  · intro
    change K.flip.flip.HasTotal c
    have := TotalComplexShapeSymmetry.symmetry c₁ c₂ c
    infer_instance
  · intro
    infer_instance

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

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j : J
⊢ ((K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) ≫
      K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) =
    𝟙 ((K.flip.total c).X j)

Tactic:
by ext; simp

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

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j : J
⊢ ((K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) ≫
      K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) =
    𝟙 ((K.total c).X j)

Tactic:
by ext; simp

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₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun i₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)

Tactic:
let c₂₃' := fun (i : ρ₂₃.q ⁻¹' {j}) => (F.obj (X₁ i.1.1)).mapCocone (c₂₃ i.1.2)

Goal state after:
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₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun i₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) →
  Cocone (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i).2) ⋙ F.obj (X₁ (↑i).1)) :=
  fun i ↦ (F.obj (X₁ (↑i).1)).mapCocone (c₂₃ (↑i).2)
⊢ IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)
Module: Mathlib.CategoryTheory.Shift.CommShiftTwo

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
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} D
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₂
⊢ CommShift (flipApp (τ ≫ τ') x✝) M

Tactic:
simp only [flipApp, flipFunctor_obj, Functor.map_comp, comp_app]
    infer_instance

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

Goal state before:
pp: case pos.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p.negOnePow = x.negOnePow * (x + p).negOnePow

Tactic:
Int.negOnePow_add,

Goal state after:
case pos.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ p.negOnePow = x.negOnePow * (x.negOnePow * p.negOnePow)
Module: Mathlib.Algebra.Homology.BifunctorAssociator

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

Tactic:
ext i₁ i₂ i₃ h

Goal state after:
case e_a
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ mapBifunctor.D₁ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ j j' =
    ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ (D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' + D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j')
Module: Mathlib.Algebra.Homology.BifunctorShift

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✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
n₁ n₂ n : ℤ
h : n₁ + n₂ = n
m₂ m : ℤ
hm₂ : m₂ = n₂ + y
hm : m = n + y
⊢ K₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h ≫
      (K₁.mapBifunctorShift₂Iso K₂ F y).hom.f n =
    (n₁ * y).negOnePow •
      (F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom ≫
        K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯ ≫ ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso y n m hm).inv

Tactic:
dsimp [mapBifunctorShift₂Iso]

Goal state after:
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✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
n₁ n₂ n : ℤ
h : n₁ + n₂ = n
m₂ m : ℤ
hm₂ : m₂ = n₂ + y
hm : m = n + y
⊢ K₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h ≫
      (HomologicalComplex₂.total.map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom (ComplexShape.up ℤ)).f n ≫
        ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₂Iso
                y).hom.f
          n =
    (n₁ * y).negOnePow •
      (F.obj (K₁.X n₁)).map (XIsoOfEq K₂ ⋯).hom ≫
        K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯ ≫ (XIsoOfEq (K₁.mapBifunctor K₂ F) ⋯).inv