awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₁.Rel i₁ (c₁.next i₁)
dsimp :
  HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X (c₁.next i₁))).obj (K₂.X i₂))).obj (K₃.X i₃))
          (NatTrans.app (G.map (NatTrans.app (F₁₂.map (K₁.d i₁ (c₁.next i₁))) (K₂.X i₂))) (K₃.X i₃))
          (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ (c₁.next i₁) i₂ i₃ j) :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j) =
    0
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
    (d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
    (0 :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
dsimp [d₁]

Premises used: HomologicalComplex.mapBifunctor₁₂.d₁
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ i₁' : ι₁
h₁ : c₁.Rel i₁ i₁'
i₂ : ι₂
i₃ : ι₃
j : ι₄
obtain :
  ∀ (h₁ : c₁.Rel i₁ (c₁.next i₁)),
    d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
      HSMul.hSMul (β :=
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
        (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂))
        (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X (c₁.next i₁))).obj (K₂.X i₂))).obj (K₃.X i₃))
            (NatTrans.app (G.map (NatTrans.app (F₁₂.map (K₁.d i₁ (c₁.next i₁))) (K₂.X i₂))) (K₃.X i₃))
            (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ (c₁.next i₁) i₂ i₃ j) :
          (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
            X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
⊢ d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (NatTrans.app (G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))) (K₃.X i₃) ≫
          ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
obtain rfl := c₁.next_eq' h₁

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h₁ : c₁.Rel i₁ (c₁.next i₁)
⊢ d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X (c₁.next i₁))).obj (K₂.X i₂))).obj (K₃.X i₃))
          (NatTrans.app (G.map (NatTrans.app (F₁₂.map (K₁.d i₁ (c₁.next i₁))) (K₂.X i₂))) (K₃.X i₃))
          (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ (c₁.next i₁) i₂ i₃ j) :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₂.Rel i₂ (c₂.next i₂)
dsimp :
  HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X (c₂.next i₂)))).obj (K₃.X i₃))
          (NatTrans.app (G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ (c₂.next i₂)))) (K₃.X i₃))
          (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ (c₂.next i₂) i₃ j) :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j) =
    0
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
    (d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
    (0 :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
dsimp [d₂]

Premises used: HomologicalComplex.mapBifunctor₁₂.d₂
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ i₂' : ι₂
h₂ : c₂.Rel i₂ i₂'
i₃ : ι₃
j : ι₄
obtain :
  ∀ (h₂ : c₂.Rel i₂ (c₂.next i₂)),
    d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
      HSMul.hSMul (β :=
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
        (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂))
        (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X (c₂.next i₂)))).obj (K₃.X i₃))
            (NatTrans.app (G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ (c₂.next i₂)))) (K₃.X i₃))
            (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ (c₂.next i₂) i₃ j) :
          (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
            X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
⊢ d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      ((G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))).app (K₃.X i₃) ≫ ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂' i₃ j :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
obtain rfl := c₂.next_eq' h₂

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂))
      (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X (c₂.next i₂)))).obj (K₃.X i₃))
          (NatTrans.app (G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ (c₂.next i₂)))) (K₃.X i₃))
          (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ (c₂.next i₂) i₃ j) :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₃.Rel i₃ (c₃.next i₃)
dsimp :
  HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃))
      (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X (c₃.next i₃)))
          ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ (c₃.next i₃)))
          (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ (c₃.next i₃) j) :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j) =
    0
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
    (d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
    (0 :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
dsimp [d₃]

Premises used: HomologicalComplex.mapBifunctor₁₂.d₃
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ i₃' : ι₃
h₃ : c₃.Rel i₃ i₃'
j : ι₄
obtain :
  ∀ (h₃ : c₃.Rel i₃ (c₃.next i₃)),
    d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
      HSMul.hSMul (β :=
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
        (c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃))
        (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X (c₃.next i₃)))
            ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ (c₃.next i₃)))
            (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ (c₃.next i₃) j) :
          (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
            X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
⊢ d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃))
      ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ i₃') ≫ ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃' j :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
obtain rfl := c₃.next_eq' h₃

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h₃ : c₃.Rel i₃ (c₃.next i₃)
⊢ d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j =
    HSMul.hSMul (β :=
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
      (c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃))
      (CategoryStruct.comp (Y := (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X (c₃.next i₃)))
          ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ (c₃.next i₃)))
          (ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ (c₃.next i₃) j) :
        (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_5} C₃
inst_3 : Category.{v_4, u_6} C₄
inst_4 : Category.{v_5, u_3} C₁₂
inst_5 : HasZeroMorphisms.{v_1, u_1} C₁
inst_6 : HasZeroMorphisms.{v_2, u_2} C₂
inst_7 : HasZeroMorphisms.{v_3, u_5} C₃
inst_8 : Preadditive.{v_5, u_3} C₁₂
inst_9 : Preadditive.{v_4, u_6} C₄
F₁₂ : C₁ ⥤ CategoryTheory.Functor.{v_2, v_5, u_2, u_3} C₂ C₁₂
G : C₁₂ ⥤ CategoryTheory.Functor.{v_3, v_4, u_5, u_6} C₃ C₄
inst_10 : F₁₂.PreservesZeroMorphisms
inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_12 : G.Additive
inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst_14 : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex.{v_1, u_1, u_7} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_8} C₂ c₂
K₃ : HomologicalComplex.{v_3, u_5, u_9} C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_18 : DecidableEq ι₁₂
inst_19 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
      X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j')
    (CategoryStruct.comp (Y := X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
        (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h :
          (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
            X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j)
        (D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' :
          X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j ⟶
            X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j') :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j')
    (d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j' :
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
        X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j')

Tactic:
simp [D₁]

Premises used: HomologicalComplex.mapBifunctor₁₂.D₁