awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i : I₁
i_1 : I₂
⊢ Eq.{v_3 + 1} (α :=
    HomologicalComplex.X.{v_3, u_3, u_5}
        (HomologicalComplex.X
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
          i)
        i_1 ⟶
      HomologicalComplex.X.{v_3, u_3, u_5}
        (HomologicalComplex.X
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
          i)
        i_1)
    (HomologicalComplex.Hom.f
      (HomologicalComplex.Hom.f
        (HomologicalComplex₂.homMk
          (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (HomologicalComplex.Hom.f (𝟙 K₂))) ⋯ ⋯)
        i)
      i_1)
    (HomologicalComplex.Hom.f
      (HomologicalComplex.Hom.f
        (𝟙
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
        i)
      i_1)
have h : (F.obj (K₁.X i)).map (𝟙 (K₂.X i_1)) = 𝟙 ((F.obj (K₁.X i)).obj (K₂.X i_1))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i : I₁
i_1 : I₂
⊢ (F.obj (K₁.X i)).map (𝟙 (K₂.X i_1)) = 𝟙 ((F.obj (K₁.X i)).obj (K₂.X i_1))
have h : Eq.{v_3 + 1} (α := (F.obj (K₁.X i)).obj (K₂.X i_1) ⟶ (F.obj (K₁.X i)).obj (K₂.X i_1))
  (𝟙 ((F.obj (K₁.X i)).obj (K₂.X i_1))) (𝟙 ((F.obj (K₁.X i)).obj (K₂.X i_1)))
Tactic: rw [Functor.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
X Y Z : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f : X ⟶ Y
g : Y ⟶ Z
i : I₁
i_1 : I₂
⊢ Eq.{v_3 + 1} (α :=
    HomologicalComplex.X.{v_3, u_3, u_5}
        (HomologicalComplex.X
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj X.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (X.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (X.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
          i)
        i_1 ⟶
      HomologicalComplex.X.{v_3, u_3, u_5}
        (HomologicalComplex.X
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj Z.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (Z.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (Z.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
          i)
        i_1)
    (HomologicalComplex.Hom.f
      (HomologicalComplex.Hom.f
        (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).f) ⋯ ⋯) i)
      i_1)
    (HomologicalComplex.Hom.f
      (HomologicalComplex.Hom.f
        (CategoryStruct.comp (Y :=
          HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj Y.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (Y.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (Y.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
          (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map f.f) ⋯ ⋯)
          (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map g.f) ⋯ ⋯))
        i)
      i_1)
have h : (F.obj (K₁.X i)).map (f.f i_1 ≫ g.f i_1) = (F.obj (K₁.X i)).map (f.f i_1) ≫ (F.obj (K₁.X i)).map (g.f i_1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
X Y Z : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f : X ⟶ Y
g : Y ⟶ Z
i : I₁
i_1 : I₂
⊢ (F.obj (K₁.X i)).map (f.f i_1 ≫ g.f i_1) = (F.obj (K₁.X i)).map (f.f i_1) ≫ (F.obj (K₁.X i)).map (g.f i_1)
have h : (F.obj (K₁.X i)).map (f.f i_1) ≫ (F.obj (K₁.X i)).map (g.f i_1) =
  (F.obj (K₁.X i)).map (f.f i_1) ≫ (F.obj (K₁.X i)).map (g.f i_1)
Tactic: rw [Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ K₁' : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f : K₁ ⟶ K₁'
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
i₂ : I₂
h : c₁.Rel i₁ i₁'
⊢ Eq.{v_3 + 1} (α :=
    HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) (i₁, i₂) ⟶
      HomologicalComplex.X (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) i₁') i₂)
    (((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁, i₂) ≫
        HomologicalComplex.Hom.f (HomologicalComplex.d (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) i₁ i₁')
          i₂ :
      HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) (i₁, i₂) ⟶
        HomologicalComplex.X (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) i₁') i₂)
    (HomologicalComplex.Hom.f (HomologicalComplex.d (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) i₁ i₁') i₂ ≫
        ((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁', i₂) :
      HomologicalComplex.X (HomologicalComplex.X (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) i₁) i₂ ⟶
        HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁') K₂) (i₁', i₂))
have dsimp : Eq (α :=
  HomologicalComplex₂.toGradedObject (obj (F.mapBifunctorHomologicalComplexObj c₂ K₁) K₂) (i₁, i₂) ⟶
    (F.obj (K₁'.X i₁')).obj (K₂.X i₂))
  ((F.map (f.f i₁)).app (K₂.X i₂) ≫ (F.map (K₁'.d i₁ i₁')).app (K₂.X i₂))
  ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (f.f i₁')).app (K₂.X i₂))
Tactic: dsimp
-- 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_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₃) = j
have rw : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (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₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₁₂ : ι₁₂
j : ι₄
h₁₂ : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h : c₁₂.π c₃ c₄ (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₂ 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)
have 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 sorry :
      (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₂)) sorry)) (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: subst h₁₂
Cleared hypotheses: i₁₂, 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₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ 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)
have 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
Tactic: dsimp [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₄
i₁ : ι₁
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₃) * 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
have rw : 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 0) (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
Tactic: rw [shape _ _ _ h, Functor.map_zero, zero_app, 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₄
i₁ i₁' : ι₁
h₁ : c₁.Rel i₁ i₁'
i₂ : ι₂
i₃ : ι₃
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)
have 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)
Tactic: obtain rfl := c₁.next_eq' h₁
Cleared hypotheses: i₁', 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₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 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)
have 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
Tactic: dsimp [d₂]