mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f✝ ≫
      (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y✝).X x)) ⋯).hom =
    (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X✝).X x)) ⋯).hom ≫
      ChainComplex.alternatingConst.map f✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f✝ ≫
      (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y✝).X x)) ⋯).hom =
    (HomologicalComplex.Hom.isoOfComponents
          (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X✝).X x)) ⋯).hom ≫
      ChainComplex.alternatingConst.map f✝
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
i✝ : ℕ
⊢ ((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f✝ ≫
          (HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y✝).X x))
              ⋯).hom).f
      i✝ =
    ((HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X✝).X x)) ⋯).hom ≫
          ChainComplex.alternatingConst.map f✝).f
      i✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
i✝ : ℕ
⊢ ((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f✝ ≫
          (HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y✝).X x))
              ⋯).hom).f
      i✝ =
    ((HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X✝).X x)) ⋯).hom ≫
          ChainComplex.alternatingConst.map f✝).f
      i✝
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.hom e'.hom ≫ mapBifunctorMapMap F p e.inv e'.inv) x✝ =
    ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₁ Y₁) x✝

Tactic:
;

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.hom e'.hom ≫ mapBifunctorMapMap F p e.inv e'.inv) x✝ =
    ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₁ Y₁) x✝
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.inv e'.inv ≫ mapBifunctorMapMap F p e.hom e'.hom) x✝ =
    ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₂ Y₂) x✝

Tactic:
;

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.inv e'.inv ≫ mapBifunctorMapMap F p e.hom e'.hom) x✝ =
    ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₂ Y₂) x✝
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ C.d i j = 0

Tactic:
;

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ C.d i j = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n i : ℕ
x✝² x✝¹ : Δ[n] _⦋i⦌
h : (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝² = (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝¹
x✝ : Fin ((unop (op ⦋i⦌)).len + 1)
⊢ (Hom.toOrderHom (objEquiv x✝²)) x✝ = (Hom.toOrderHom (objEquiv x✝¹)) x✝

Tactic:
;

Goal state after:
n i : ℕ
x✝² x✝¹ : Δ[n] _⦋i⦌
h : (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝² = (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝¹
x✝ : Fin ((unop (op ⦋i⦌)).len + 1)
⊢ (Hom.toOrderHom (objEquiv x✝²)) x✝ = (Hom.toOrderHom (objEquiv x✝¹)) x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
x : Δ[n] _⦋0⦌
i : Fin (0 + 1)
⊢ ((fun i ↦ const n i (op ⦋0⦌)) ((fun x ↦ x 0) x)) i = x i

Tactic:
;

Goal state after:
n : ℕ
x : Δ[n] _⦋0⦌
i : Fin (0 + 1)
⊢ ((fun i ↦ const n i (op ⦋0⦌)) ((fun x ↦ x 0) x)) i = x i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case «0»
n : ℕ
x : Δ[n] _⦋0⦌
⊢ ((fun i ↦ const n i (op ⦋0⦌)) ((fun x ↦ x 0) x)) ((fun i ↦ i) ⟨0, ⋯⟩) = x ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
;

Goal state after:
case «0»
n : ℕ
x : Δ[n] _⦋0⦌
⊢ ((fun i ↦ const n i (op ⦋0⦌)) ((fun x ↦ x 0) x)) ((fun i ↦ i) ⟨0, ⋯⟩) = x ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X✝ Y✝ : SimplexCategoryᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Δ[m].obj X✝
⊢ (ConcreteCategory.hom (Δ[m].map x✝¹ ≫ (objEquiv.trans h.homEquiv).toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom ((objEquiv.trans h.homEquiv).toIso.hom ≫ X.map x✝¹)).toFun x✝

Tactic:
;

Goal state after:
X : SSet
m : ℕ
h : Functor.RepresentableBy X ⦋m⦌
X✝ Y✝ : SimplexCategoryᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Δ[m].obj X✝
⊢ (ConcreteCategory.hom (Δ[m].map x✝¹ ≫ (objEquiv.trans h.homEquiv).toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom ((objEquiv.trans h.homEquiv).toIso.hom ≫ X.map x✝¹)).toFun x✝
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i + 1 = 1 + ↑i

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i + 1 = 1 + ↑i
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℕ
hpq : q + 1 = p
⊢ q + r + 1 = p + r

Tactic:
;

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℕ
hpq : q + 1 = p
⊢ q + r + 1 = p + r
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℕ
hpq : q + 1 = p
⊢ r + q + 1 = r + p

Tactic:
;

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℕ
hpq : q + 1 = p
⊢ r + q + 1 = r + p
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℤ
hpq : p + 1 = q
⊢ p + r + 1 = q + r

Tactic:
;

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℤ
hpq : p + 1 = q
⊢ p + r + 1 = q + r
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℤ
hpq : p + 1 = q
⊢ r + p + 1 = r + q

Tactic:
;

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q r : ℤ
hpq : p + 1 = q
⊢ r + p + 1 = r + q
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ 1 = 1 * 1

Tactic:
;

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ 1 = 1 * 1
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ c.ε x✝² * 1 = 1 * c.ε x✝²

Tactic:
;

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ c.ε x✝² * 1 = 1 * c.ε x✝²
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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ c.ε (x✝² + x✝¹) = c.ε x✝² * c.ε x✝¹

Tactic:
;

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
x✝² x✝¹ x✝ : I
⊢ c.ε (x✝² + x✝¹) = c.ε x✝² * c.ε x✝¹
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 : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ : I₁
i✝ j✝ k✝ : I₂
a✝¹ : c₂.Rel i✝ j✝
a✝ : c₂.Rel j✝ k✝
⊢ d₂ i₁ i✝ j✝ ≫ d₂ i₁ j✝ k✝ = 0

Tactic:
;

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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ : I₁
i✝ j✝ k✝ : I₂
a✝¹ : c₂.Rel i✝ j✝
a✝ : c₂.Rel j✝ k✝
⊢ d₂ i₁ i✝ j✝ ≫ d₂ i₁ j✝ k✝ = 0
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 : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
i✝ j✝ : I₂
a✝ : c₂.Rel i✝ j✝
⊢ d₁ i₁ i₁' i✝ ≫ { X := fun i₂ ↦ X (i₁', i₂), d := fun i₂ i₂' ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i✝ j✝ =
    { X := fun i₂ ↦ X (i₁, i₂), d := fun i₂ i₂' ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i✝ j✝ ≫ d₁ i₁ i₁' j✝

Tactic:
;

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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
i✝ j✝ : I₂
a✝ : c₂.Rel i✝ j✝
⊢ d₁ i₁ i₁' i✝ ≫ { X := fun i₂ ↦ X (i₁', i₂), d := fun i₂ i₂' ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i✝ j✝ =
    { X := fun i₂ ↦ X (i₁, i₂), d := fun i₂ i₂' ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ }.d i✝ j✝ ≫ d₁ i₁ i₁' j✝
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 : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' i₁'' : I₁
x✝¹ : c₁.Rel i₁ i₁'
x✝ : c₁.Rel i₁' i₁''
i₂ : I₂
⊢ ({ f := fun i₂ ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } ≫ { f := fun i₂ ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ }).f i₂ = Hom.f 0 i₂

Tactic:
;

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₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' i₁'' : I₁
x✝¹ : c₁.Rel i₁ i₁'
x✝ : c₁.Rel i₁' i₁''
i₂ : I₂
⊢ ({ f := fun i₂ ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } ≫ { f := fun i₂ ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ }).f i₂ = Hom.f 0 i₂
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✝ j✝ : I₁
a✝ : c₁.Rel i✝ j✝
⊢ (f.f i✝).f i ≫ (L.flip.X i).d i✝ j✝ = (K.flip.X i).d i✝ j✝ ≫ (f.f j✝).f i

Tactic:
;

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 L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i : I₂
i✝ j✝ : I₁
a✝ : c₁.Rel i✝ j✝
⊢ (f.f i✝).f i ≫ (L.flip.X i).d i✝ j✝ = (K.flip.X i).d i✝ j✝ ≫ (f.f j✝).f i
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₂
a✝ : 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 ↦ (f.f j).f j✝, comm' := ⋯ }

Tactic:
;

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 L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i✝ j✝ : I₂
a✝ : 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 ↦ (f.f j).f j✝, comm' := ⋯ }
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₂
a✝ : c₂.Rel i✝¹ j✝
i✝ : I₁
⊢ ({ f := fun j ↦ (f.f j).f i✝¹, comm' := ⋯ } ≫ L.flip.d i✝¹ j✝).f i✝ =
    (K.flip.d i✝¹ j✝ ≫ { f := fun j ↦ (f.f j).f j✝, comm' := ⋯ }).f i✝

Tactic:
;

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 L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i✝¹ j✝ : I₂
a✝ : c₂.Rel i✝¹ j✝
i✝ : I₁
⊢ ({ f := fun j ↦ (f.f j).f i✝¹, comm' := ⋯ } ≫ L.flip.d i✝¹ j✝).f i✝ =
    (K.flip.d i✝¹ j✝ ≫ { f := fun j ↦ (f.f j).f j✝, comm' := ⋯ }).f i✝
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₁ : I₁
x₂ : I₂
⊢ (K.X x₁).X x₂ = (K.X x₁).X x₂

Tactic:
;

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₂
x₁ : I₁
x₂ : I₂
⊢ (K.X x₁).X x₂ = (K.X x₁).X x₂
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₂ K₂' : HomologicalComplex C₂ c₂
φ : K₂ ⟶ K₂'
⊢ ∀ (i₁ i₁' : I₁) (i₂ : I₂),
    c₁.Rel i₁ i₁' →
      (F.obj (K₁.X i₁)).map (φ.f i₂) ≫ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂) =
        (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂)

Tactic:
;

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✝³ : 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₂ K₂' : HomologicalComplex C₂ c₂
φ : K₂ ⟶ K₂'
⊢ ∀ (i₁ i₁' : I₁) (i₂ : I₂),
    c₁.Rel i₁ i₁' →
      (F.obj (K₁.X i₁)).map (φ.f i₂) ≫ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂) =
        (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂)