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_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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
pos :
  ∀ (h₃ : c₁.Rel i₁ (c₁.next i₁)),
    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₃))
        (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
          ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
      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₃))
      (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have neg : ∀ (h₃ : ¬c₁.Rel i₁ (c₁.next i₁)),
  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₃))
      (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₁ F₁₂ G K₁ K₂ K₃ 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 (hypothesis)
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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ 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₃))
      (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have h₄ : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))
Tactic: have h₄ := (ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂).symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))
⊢ c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) = j'
have rw : 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₂, ← h₄]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ 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₃))
      (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have neg : 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₃))
    (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
      ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
  0
Tactic: rw [d₁_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₃,
            mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₃,
            Functor.map_zero, zero_app, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : ¬c₁.Rel i₁ (c₁.next i₁)
neg :
  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₃))
      (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    0
⊢ 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₃))
      (NatTrans.app (G.map (mapBifunctor.d₁ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have neg₁ : 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₃))
    (NatTrans.app (G.map 0) (K₃.X i₃) ≫
      ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
  0
Tactic: rw [d₁_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₃,
            mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₃,
            Functor.map_zero, zero_app, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next 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₃))
      (NatTrans.app (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)) (K₃.X i₃) ≫
        NatTrans.app (G.map (mapBifunctor.D₂ K₁ K₂ F₁₂ c₁₂ (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)))))
            (K₃.X i₃) ≫
          ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have pos : 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₃))
    (NatTrans.app (G.map (mapBifunctor.d₂ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
      ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
  d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
Tactic: rw [← NatTrans.comp_app_assoc, ← Functor.map_comp,
          mapBifunctor.ι_D₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorAssociator (goal)
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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next 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₃))
      (NatTrans.app (G.map (mapBifunctor.d₂ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have pos : ∀ (h₃ : c₂.Rel i₂ (c₂.next i₂)),
  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₃))
      (NatTrans.app (G.map (mapBifunctor.d₂ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₂ F₁₂ G K₁ K₂ K₃ 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_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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
pos :
  ∀ (h₃ : c₂.Rel i₂ (c₂.next i₂)),
    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₃))
        (NatTrans.app (G.map (mapBifunctor.d₂ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
          ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
      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₃))
      (NatTrans.app (G.map (mapBifunctor.d₂ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have neg : ∀ (h₃ : ¬c₂.Rel i₂ (c₂.next i₂)),
  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₃))
      (NatTrans.app (G.map (mapBifunctor.d₂ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₂ F₁₂ G K₁ K₂ K₃ 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 (hypothesis)
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₄
j j' : ι₄
inst_20 : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
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₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
⊢ 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₃))
      (NatTrans.app (G.map (mapBifunctor.d₂ K₁ K₂ F₁₂ c₁₂ i₁ i₂ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))))) (K₃.X i₃) ≫
        ιMapBifunctor (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))) i₃ j' h₂) =
    d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
have h₄ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))
Tactic: have h₄ := (ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃).symm