awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂ i₂' i₂'' : I₂
dsimp : (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (K₂.d i₂' i₂'') = 0
⊢ Eq.{v_3 + 1} (α :=
    ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂) ⟶
      ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂''))
    (CategoryStruct.comp (Y := ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂'))
      ((fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) i₁ i₂ i₂')
      ((fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) i₁ i₂' i₂''))
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂ i₂' i₂'' : I₂
rw : (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂' ≫ K₂.d i₂' i₂'') = 0
rw₁ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂'')) ((F.obj (K₁.X i₁)).map 0) 0
rw₂ rw₃ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂'')) 0 0
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (K₂.d i₂' i₂'') = 0

Tactic:
rw [← Functor.map_comp, HomologicalComplex.d_comp_d, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, HomologicalComplex.d_comp_d, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₁
i₂ i₂' : I₂
dsimp :
  (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') =
    (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂')
⊢ Eq.{v_3 + 1} (α :=
    ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂) ⟶
      ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁', i₂'))
    (CategoryStruct.comp (Y := ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁', i₂))
      ((fun (i₁ i₁' : I₁) (i₂ : I₂) ↦
          ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)))
        i₁ i₁' i₂)
      ((fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) i₁' i₂ i₂'))
    (CategoryStruct.comp (Y := ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂'))
      ((fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) i₁ i₂ i₂')
      ((fun (i₁ i₁' : I₁) (i₂ : I₂) ↦
          ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)))
        i₁ i₁' i₂'))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₁
i₂ i₂' : I₂
rw rw₁ :
  (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') =
    (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂')
⊢ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') =
    (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂')

Tactic:
rw [NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂ K₂' : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
φ : K₂ ⟶ K₂'
i₁ i₁' : I₁
i₂ : I₂
h : c₁.Rel i₁ i₁'
rw rw₁ :
  (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂) =
    (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂)
⊢ (F.obj (K₁.X i₁)).map (φ.f i₂) ≫ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂) =
    (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂)

Tactic:
rw [NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂ K₂' : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
φ : K₂ ⟶ K₂'
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
⊢ (F.obj (K₁.X i₁)).map (φ.f i₂) ≫ (F.obj (K₁.X i₁)).map (K₂'.d i₂ i₂') =
    (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (φ.f i₂')

Tactic:
simp only [← Functor.map_comp, φ.comm]

Premises used: CategoryTheory.Functor.map_comp, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂
dsimp :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, u_4, u_5} D c₁ c₂)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
    (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (HomologicalComplex.Hom.f (𝟙 K₂))) ⋯
      ⋯)
    (𝟙
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, u_4, u_5} D c₁ c₂)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
    (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (HomologicalComplex.Hom.f (𝟙 K₂))) ⋯
      ⋯)
    (𝟙
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂
h :
  ∀ (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)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, u_4, u_5} D c₁ c₂)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
    (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (HomologicalComplex.Hom.f (𝟙 K₂))) ⋯
      ⋯)
    (𝟙
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂
h : (F.obj (K₁.X i)).map (𝟙 (K₂.X i_1)) = 𝟙 ((F.obj (K₁.X i)).obj (K₂.X i_1))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂
h 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)))
⊢ (F.obj (K₁.X i)).map (𝟙 (K₂.X i_1)) = 𝟙 ((F.obj (K₁.X i)).obj (K₂.X i_1))

Tactic:
rw [Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Homology.Bifunctor
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
dsimp :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, u_4, u_5} D c₁ c₂)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
    (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).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) ⋯ ⋯))
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, u_4, u_5} D c₁ c₂)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (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₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
    (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (f ≫ g).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) ⋯ ⋯))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂
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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₂
h 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)
⊢ (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:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.Bifunctor
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₁'
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₂))
⊢ 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₂))

Tactic:
dsimp