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_4
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 : Category.{v_6, u_4} C₂₃
inst_6 : HasZeroMorphisms.{v_1, u_1} C₁
inst_7 : HasZeroMorphisms.{v_2, u_2} C₂
inst_8 : HasZeroMorphisms.{v_3, u_5} C₃
inst_9 : Preadditive.{v_5, u_3} C₁₂
inst_10 : Preadditive.{v_6, u_4} C₂₃
inst_11 : 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₄
F : C₁ ⥤ CategoryTheory.Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ CategoryTheory.Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
inst_12 : F₁₂.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_14 : G.Additive
inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst_16 : G₂₃.PreservesZeroMorphisms
inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_18 : F.PreservesZeroMorphisms
inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst_20 : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_21 : TotalComplexShape c₁ c₂ c₁₂
inst_22 : TotalComplexShape c₁₂ c₃ c₄
inst_23 : TotalComplexShape c₂ c₃ c₂₃
inst_24 : TotalComplexShape c₁ c₂₃ c₄
inst_25 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_26 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_27 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_28 : DecidableEq ι₁₂
inst_29 : DecidableEq ι₂₃
inst_30 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
inst_31 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
⊢ (((GradedObject.mapBifunctor G ι₁₂ ι₃).obj (GradedObject.mapBifunctorMapObj F₁₂ (c₁.π c₂ c₁₂) K₁.X K₂.X)).obj
        K₃.X).HasMap
    (c₁₂.π c₃ c₄)

Tactic:
inferInstanceAs (HasMapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄)

Premises used: _private.0.HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX._proof_1
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_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 : Category.{v_6, u_4} C₂₃
inst_6 : HasZeroMorphisms.{v_1, u_1} C₁
inst_7 : HasZeroMorphisms.{v_2, u_2} C₂
inst_8 : HasZeroMorphisms.{v_3, u_5} C₃
inst_9 : Preadditive.{v_5, u_3} C₁₂
inst_10 : Preadditive.{v_6, u_4} C₂₃
inst_11 : 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₄
F : C₁ ⥤ CategoryTheory.Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ CategoryTheory.Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
inst_12 : F₁₂.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_14 : G.Additive
inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst_16 : G₂₃.PreservesZeroMorphisms
inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_18 : F.PreservesZeroMorphisms
inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst_20 : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_21 : TotalComplexShape c₁ c₂ c₁₂
inst_22 : TotalComplexShape c₁₂ c₃ c₄
inst_23 : TotalComplexShape c₂ c₃ c₂₃
inst_24 : TotalComplexShape c₁ c₂₃ c₄
inst_25 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_26 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_27 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_28 : DecidableEq ι₁₂
inst_29 : DecidableEq ι₂₃
inst_30 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
inst_31 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
⊢ (((GradedObject.mapBifunctor F ι₁ ι₂₃).obj K₁.X).obj
        (GradedObject.mapBifunctorMapObj G₂₃ (c₂.π c₃ c₂₃) K₂.X K₃.X)).HasMap
    (c₁.π c₂₃ c₄)

Tactic:
inferInstanceAs (HasMapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄)

Premises used: _private.0.HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ._proof_1
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_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 : Category.{v_6, u_4} C₂₃
inst_6 : HasZeroMorphisms.{v_1, u_1} C₁
inst_7 : HasZeroMorphisms.{v_2, u_2} C₂
inst_8 : HasZeroMorphisms.{v_3, u_5} C₃
inst_9 : Preadditive.{v_5, u_3} C₁₂
inst_10 : Preadditive.{v_6, u_4} C₂₃
inst_11 : 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₄
F : C₁ ⥤ CategoryTheory.Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ CategoryTheory.Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
inst_12 : F₁₂.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_14 : G.Additive
inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst_16 : G₂₃.PreservesZeroMorphisms
inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_18 : F.PreservesZeroMorphisms
inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst_20 : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_21 : TotalComplexShape c₁ c₂ c₁₂
inst_22 : TotalComplexShape c₁₂ c₃ c₄
inst_23 : TotalComplexShape c₂ c₃ c₂₃
inst_24 : TotalComplexShape c₁ c₂₃ c₄
inst_25 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_26 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_27 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_28 : DecidableEq ι₁₂
inst_29 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₁₂ : ι₁₂
j : ι₄
h₁₂ : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h : c₁₂.π c₃ c₄ (i₁₂, i₃) = j
rw : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃)
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j

Tactic:
rw [← h, ← h₁₂]
-- Module: Mathlib.Algebra.Homology.BifunctorAssociator
Goal:
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_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 : Category.{v_6, u_4} C₂₃
inst_6 : HasZeroMorphisms.{v_1, u_1} C₁
inst_7 : HasZeroMorphisms.{v_2, u_2} C₂
inst_8 : HasZeroMorphisms.{v_3, u_5} C₃
inst_9 : Preadditive.{v_5, u_3} C₁₂
inst_10 : Preadditive.{v_6, u_4} C₂₃
inst_11 : 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₄
F : C₁ ⥤ CategoryTheory.Functor.{v_6, v_4, u_4, u_6} C₂₃ C₄
G₂₃ : C₂ ⥤ CategoryTheory.Functor.{v_3, v_6, u_5, u_4} C₃ C₂₃
inst_12 : F₁₂.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst_14 : G.Additive
inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst_16 : G₂₃.PreservesZeroMorphisms
inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_18 : F.PreservesZeroMorphisms
inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst_20 : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_21 : TotalComplexShape c₁ c₂ c₁₂
inst_22 : TotalComplexShape c₁₂ c₃ c₄
inst_23 : TotalComplexShape c₂ c₃ c₂₃
inst_24 : TotalComplexShape c₁ c₂₃ c₄
inst_25 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst_26 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_27 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_28 : DecidableEq ι₁₂
inst_29 : HasMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₁₂ : ι₁₂
j : ι₄
h₁₂ : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h : c₁₂.π c₃ c₄ (i₁₂, i₃) = j
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃)

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₃ : ι₃
i₁₂ : ι₁₂
j : ι₄
h₁₂ : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h : c₁₂.π c₃ c₄ (i₁₂, i₃) = j
subst :
  ∀ (h : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = j),
    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)
      (ι 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)
      (NatTrans.app (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)) (K₃.X i₃) ≫
          ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁.π 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)
⊢ 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)
    (ι 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)
    (NatTrans.app (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ i₁₂ h₁₂)) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ 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)

Tactic:
subst h₁₂
-- 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₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = j
⊢ 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)
    (ι 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)
    (NatTrans.app (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁.π 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)

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₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ 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)
    (ι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)
    (ι 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)

Tactic:
dif_pos h

Premises used: HomologicalComplex.mapBifunctor₁₂.ιOrZero, dif_pos
-- 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₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) ≠ j
⊢ 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)
    (ι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)
    (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:
dif_neg h

Premises used: HomologicalComplex.mapBifunctor₁₂.ιOrZero, dif_neg
-- 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₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
j : ι₄
A : C₄
f g : X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j ⟶ A
hfg :
  ∀ (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 ≫ f = ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ g
⊢ f = g

Tactic:
GradedObject.mapBifunctor₁₂BifunctorMapObj_ext hfg

Premises used: CategoryTheory.GradedObject.mapBifunctorMapObj, HomologicalComplex₂.toGradedObject, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapObj, CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext
-- 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₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
j : ι₄
A : C₄
f :
  (i₁ : ι₁) →
    (i₂ : ι₂) →
      (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A)
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = 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)
      (mapBifunctor₁₂Desc f : X (mapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄) j ⟶ A) =
    f i₁ i₂ i₃ h

Tactic:
apply GradedObject.ι_mapBifunctor₁₂BifunctorDesc

Premises used: CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc