awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ Eq (α :=
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) ⋯) ≫
        mapBifunctor.d₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂.π c₃ c₂₃ (i₂, i₃)) j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
have pos : ∀ (h₁ : c₁.Rel i₁ (c₁.next i₁)),
  Eq (α :=
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) sorry) ≫
        mapBifunctor.d₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂.π c₃ c₂₃ (i₂, i₃)) j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
Tactic: by_cases h₁ : c₁.Rel i₁ (c₁.next i₁)
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₁.Rel i₁ (c₁.next i₁)
⊢ Eq (α :=
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) ⋯) ≫
        mapBifunctor.d₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂.π c₃ c₂₃ (i₂, i₃)) j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
have pos : (F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) sorry) ≫
    mapBifunctor.d₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂.π c₃ c₂₃ (i₂, i₃)) j' =
  HSMul.hSMul (β :=
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (c₁.ε₁ c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)))
    (CategoryStruct.comp (Y := (F.obj (K₁.X (c₁.next i₁))).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)))
        (NatTrans.app (F.map (K₁.d i₁ (c₁.next i₁))) ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)))
        (ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ (c₁.next i₁) i₂ i₃ j') :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
Tactic: rw [d₁_eq _ _ _ _ _ _ _ _ h₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : c₁.π c₂₃ c₄ (c₁.next i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = j'
⊢ c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) = j'
have pos : c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃)
Tactic: rw [← h₂, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ Eq (α :=
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) ⋯) ≫
        mapBifunctor.d₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂.π c₃ c₂₃ (i₂, i₃)) j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' :
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
have neg : Eq (α :=
  (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶ X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
  (CategoryStruct.comp (Y := (F.obj (K₁.X i₁)).obj (X (K₂.mapBifunctor K₃ G₂₃ c₂₃) (c₂.π c₃ c₂₃ (i₂, i₃))))
      ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) sorry)) 0 :
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
  (d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' :
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
Tactic: rw [mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₁,
      d₁_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst_23 : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ c₁.π c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = j
have rw : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃)
Tactic: rw [← h, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst_23 : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
⊢ HSMul.hSMul (β :=
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
      (c₁.ε₂ c₂₃ c₄ (i₁, i₂₃))
      ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ (c₂.π c₃ c₂₃ (i₂, i₃)) ⋯) ≫
        (F.obj (K₁.X i₁)).map (mapBifunctor.D₁ K₂ K₃ G₂₃ c₂₃ i₂₃ (c₂₃.next i₂₃)) ≫
          K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂) =
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
have pos : HSMul.hSMul (β :=
    (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
      X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
    (c₁.ε₂ c₂₃ c₄ (i₁, i₂₃))
    ((F.obj (K₁.X i₁)).map (mapBifunctor.d₁ K₂ K₃ G₂₃ c₂₃ i₂ i₃ (c₂₃.next i₂₃)) ≫
      K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂) =
  d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
Tactic: rw [← Functor.map_comp_assoc, mapBifunctor.ι_D₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst_23 : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
⊢ HSMul.hSMul (β :=
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
      (c₁.ε₂ c₂₃ c₄ (i₁, i₂₃))
      ((F.obj (K₁.X i₁)).map (mapBifunctor.d₁ K₂ K₃ G₂₃ c₂₃ i₂ i₃ (c₂₃.next i₂₃)) ≫
        K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂) =
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
have pos : ∀ (h₃ : c₂.Rel i₂ (c₂.next i₂)),
  HSMul.hSMul (β :=
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
      (c₁.ε₂ c₂₃ c₄ (i₁, i₂₃))
      ((F.obj (K₁.X i₁)).map (mapBifunctor.d₁ K₂ K₃ G₂₃ c₂₃ i₂ i₃ (c₂₃.next i₂₃)) ≫
        K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂) =
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
Tactic: by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst_23 : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
pos :
  ∀ (h₃ : c₂.Rel i₂ (c₂.next i₂)),
    HSMul.hSMul (β :=
        (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
          X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
        (c₁.ε₂ c₂₃ c₄ (i₁, i₂₃))
        ((F.obj (K₁.X i₁)).map (mapBifunctor.d₁ K₂ K₃ G₂₃ c₂₃ i₂ i₃ (c₂₃.next i₂₃)) ≫
          K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂) =
      d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
⊢ HSMul.hSMul (β :=
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
      (c₁.ε₂ c₂₃ c₄ (i₁, i₂₃))
      ((F.obj (K₁.X i₁)).map (mapBifunctor.d₁ K₂ K₃ G₂₃ c₂₃ i₂ i₃ (c₂₃.next i₂₃)) ≫
        K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂) =
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
have neg : ∀ (h₃ : ¬c₂.Rel i₂ (c₂.next i₂)),
  HSMul.hSMul (β :=
      (F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶
        X (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄) j')
      (c₁.ε₂ c₂₃ c₄ (i₁, i₂₃))
      ((F.obj (K₁.X i₁)).map (mapBifunctor.d₁ K₂ K₃ G₂₃ c₂₃ i₂ i₃ (c₂₃.next i₂₃)) ≫
        K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ (c₂₃.next i₂₃) j' h₂) =
    d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
Tactic: by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
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_6, u_4} 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_6, u_4} C₂₃
inst_9 : Preadditive.{v_4, u_6} 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_10 : G₂₃.PreservesZeroMorphisms
inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst_12 : F.PreservesZeroMorphisms
inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst_15 : TotalComplexShape c₁ c₂ c₁₂
inst_16 : TotalComplexShape c₁₂ c₃ c₄
inst_17 : TotalComplexShape c₂ c₃ c₂₃
inst_18 : TotalComplexShape c₁ c₂₃ c₄
inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst_21 : DecidableEq ι₂₃
inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst_23 : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.r c₂ c₃ c₁₂ c₄ (i₁, c₂.next i₂, i₃) = j'
have dsimp : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃) = j'
Tactic: dsimp [ComplexShape.r]