awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.BifunctorFlip
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
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
φ₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
φ₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : TotalComplexShape c₂ c₁ c
inst_10 : TotalComplexShapeSymmetry c₁ c₂ c
inst_11 : DecidableEq J
inst_12 : K₁.HasMapBifunctor K₂ F c
inst_13 : L₁.HasMapBifunctor L₂ F c
i₁ : I₁
i₂ : I₂
j : J
hj rw : c₁.π c₂ c (i₁, i₂) = j
rw₁ rw₂ : j = j
⊢ c₂.π c₁ c (i₂, i₁) = j

Tactic:
rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, hj]

Premises used: ComplexShape.π_symm
-- Module: Mathlib.Algebra.Homology.BifunctorFlip
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
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : TotalComplexShape c₂ c₁ c
inst_10 : TotalComplexShapeSymmetry c₁ c₂ c
inst_11 : DecidableEq J
inst_12 : K₁.HasMapBifunctor K₂ F c
i₁ : I₁
i₂ : I₂
j : J
hj : c₁.π c₂ c (i₁, i₂) = j
⊢ CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj)
      (Hom.f (Iso.inv (K₁.mapBifunctorFlipIso K₂ F c)) j) =
    HSMul.hSMul (β := (F.flip.obj (K₂.X i₂)).obj (K₁.X i₁) ⟶ X (K₂.mapBifunctor K₁ F.flip c) j) (c₁.σ c₂ c i₁ i₂)
      (K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j ⋯)

Tactic:
HomologicalComplex₂.ιTotal_totalFlipIso_f_inv
    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂) c i₁ i₂ j hj

Premises used: HomologicalComplex₂.ofGradedObject, CategoryTheory.Functor.mapBifunctorHomologicalComplex, HomologicalComplex₂.flip, CategoryTheory.Functor.obj, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv
-- Module: Mathlib.Algebra.Homology.BifunctorFlip
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
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst_8 : TotalComplexShape c₁ c₂ c
inst_9 : TotalComplexShape c₂ c₁ c
inst_10 : TotalComplexShapeSymmetry c₁ c₂ c
inst_11 : DecidableEq J
inst_12 : K₁.HasMapBifunctor K₂ F c
inst_13 : TotalComplexShapeSymmetry c₂ c₁ c
inst_14 : TotalComplexShapeSymmetrySymmetry c₁ c₂ c
⊢ Eq (α :=
    Iso (C := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F.flip.flip c) (K₂.mapBifunctor K₁ F.flip c))
    (K₂.mapBifunctorFlipIso K₁ F.flip c :
      Iso (C := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F.flip.flip c)
        (K₂.mapBifunctor K₁ F.flip c))
    (Iso.symm (K₁.mapBifunctorFlipIso K₂ F c) :
      Iso (C := HomologicalComplex.{v_3, u_3, u_6} D c) (K₁.mapBifunctor K₂ F c) (K₂.mapBifunctor K₁ F.flip c))

Tactic:
(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).flip_totalFlipIso c

Premises used: HomologicalComplex.mapBifunctorFlipIso, HomologicalComplex₂.ofGradedObject, CategoryTheory.Functor.mapBifunctorHomologicalComplex, HomologicalComplex₂.flip, HomologicalComplex₂.flip_totalFlipIso, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
i₂ : I₂
j j' : J
h : c₁.π c₂ c (i₁', i₂) = j
h' : c₁.prev i₁' = i₁
subst :
  CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
      (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h : (F.obj (K₁.X i₁')).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
      (hom₁ h₁ f₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') =
    HSMul.hSMul (β := (F.obj (K₁.X i₁')).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁', i₂))
      (NatTrans.app (F.map (h₁.hom i₁' (c₁.prev i₁'))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁'))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁') i₂ j')
⊢ CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
      (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h : (F.obj (K₁.X i₁')).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
      (hom₁ h₁ f₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') =
    HSMul.hSMul (β := (F.obj (K₁.X i₁')).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (i₁, i₂))
      ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j')

Tactic:
subst h'
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
i₁' : I₁
i₂ : I₂
j j' : J
h : c₁.π c₂ c (i₁', i₂) = j
⊢ CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
      (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h : (F.obj (K₁.X i₁')).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
      (hom₁ h₁ f₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') =
    HSMul.hSMul (β := (F.obj (K₁.X i₁')).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁', i₂))
      (NatTrans.app (F.map (h₁.hom i₁' (c₁.prev i₁'))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁'))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁') i₂ j')

Tactic:
simp [hom₁]

Premises used: HomologicalComplex.mapBifunctorMapHomotopy.hom₁
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
i₁ : I₁
i₂ i₂' : I₂
j j' : J
h : c₁.π c₂ c (i₁, i₂') = j
h' : c₂.prev i₂' = i₂
subst :
  CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
      (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h : (F.obj (K₁.X i₁)).obj (K₂.X i₂') ⟶ X (K₁.mapBifunctor K₂ F c) j)
      (hom₂ f₁ h₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂') ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₂ c₂ c (i₁, c₂.prev i₂'))
      ((F.map (f₁.f i₁)).app (K₂.X i₂') ≫
        CategoryStruct.comp (Y := (F.obj (L₁.X i₁)).obj (L₂.X (c₂.prev i₂')))
          ((F.obj (L₁.X i₁)).map (h₂.hom i₂' (c₂.prev i₂'))) (L₁.ιMapBifunctorOrZero L₂ F c i₁ (c₂.prev i₂') j'))
⊢ CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
      (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h : (F.obj (K₁.X i₁)).obj (K₂.X i₂') ⟶ X (K₁.mapBifunctor K₂ F c) j)
      (hom₂ f₁ h₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂') ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₂ c₂ c (i₁, i₂))
      ((F.map (f₁.f i₁)).app (K₂.X i₂') ≫
        (F.obj (L₁.X i₁)).map (h₂.hom i₂' i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j')

Tactic:
subst h'
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
i₁ : I₁
i₂' : I₂
j j' : J
h : c₁.π c₂ c (i₁, i₂') = j
⊢ CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
      (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h : (F.obj (K₁.X i₁)).obj (K₂.X i₂') ⟶ X (K₁.mapBifunctor K₂ F c) j)
      (hom₂ f₁ h₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') =
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂') ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₂ c₂ c (i₁, c₂.prev i₂'))
      ((F.map (f₁.f i₁)).app (K₂.X i₂') ≫
        CategoryStruct.comp (Y := (F.obj (L₁.X i₁)).obj (L₂.X (c₂.prev i₂')))
          ((F.obj (L₁.X i₁)).map (h₂.hom i₂' (c₂.prev i₂'))) (L₁.ιMapBifunctorOrZero L₂ F c i₁ (c₂.prev i₂') j'))

Tactic:
simp [hom₂]

Premises used: HomologicalComplex.mapBifunctorMapHomotopy.hom₂
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
h₂ :
  ∀ (i₁ : I₁) (i₂ : I₂) (h' : c₁.π c₂ c (i₁, i₂) = j),
    Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')
      (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
          (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h' : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
          (hom₁ h₁ f₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') :
        (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')
      (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h') 0 :
        (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')
⊢ Eq (α := X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j')
    (hom₁ h₁ f₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j')
    (0 : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j')

Tactic:
ext i₁ i₂ h'
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₂ :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')
    (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h')
      (HomologicalComplex₂.totalDesc (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)
        fun (i₁ : I₁) (i₂ : I₂) (x : c₁.π c₂ c (i₁, i₂) = j) ↦
        HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
          (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
            (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j')))
    (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h') 0)
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')
    (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j)
        (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h' : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (K₁.mapBifunctor K₂ F c) j)
        (hom₁ h₁ f₂ F c j j' : X (K₁.mapBifunctor K₂ F c) j ⟶ X (L₁.mapBifunctor L₂ F c) j') :
      (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')
    (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h') 0 :
      (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')

Tactic:
dsimp [hom₁]

Premises used: HomologicalComplex.mapBifunctorMapHomotopy.hom₁
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₂ :
  HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j')
    (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h')
      (HomologicalComplex₂.totalDesc (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)
        fun (i₁ : I₁) (i₂ : I₂) (x : c₁.π c₂ c (i₁, i₂) = j) ↦
        HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
          (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
            (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j')))
    (CategoryStruct.comp (Y := X (K₁.mapBifunctor K₂ F c) j) (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h') 0)

Tactic:
rw [comp_zero, HomologicalComplex₂.ι_totalDesc]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex₂.ι_totalDesc
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
pos :
  ∀ (h₃ : c₁.Rel (c₁.prev i₁) i₁),
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
        (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
      0
neg :
  ∀ (h₃ : ¬c₁.Rel (c₁.prev i₁) i₁),
    HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
        (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
      0
⊢ HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0

Tactic:
by_cases h₃ : c₁.Rel (c₁.prev i₁) i₁

Premises used: ComplexShape.prev, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
pos : c₁.π c₂ c (c₁.prev i₁, i₂) ≠ j'
⊢ HSMul.hSMul (β := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') (c₁.ε₁ c₂ c (c₁.prev i₁, i₂))
      (NatTrans.app (F.map (h₁.hom i₁ (c₁.prev i₁))) (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0

Tactic:
rw [ιMapBifunctorOrZero_eq_zero, comp_zero, comp_zero, smul_zero]

Premises used: CategoryTheory.Limits.comp_zero, smul_zero, HomologicalComplex.ιMapBifunctorOrZero_eq_zero
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₁.π c₂ c (c₁.prev i₁, i₂) = j'
pos : c.Rel j' j
⊢ False

Tactic:
apply h
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₁.π c₂ c (c₁.prev i₁, i₂) = j'
pos : c.Rel (c₁.π c₂ c (c₁.prev i₁, i₂)) (c₁.π c₂ c (i₁, i₂))
⊢ c.Rel j' j

Tactic:
rw [← h', ← h₄]
-- Module: Mathlib.Algebra.Homology.BifunctorHomotopy
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ CategoryTheory.Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst_8 : DecidableEq J
inst_9 : TotalComplexShape c₁ c₂ c
inst_10 : K₁.HasMapBifunctor K₂ F c
inst_11 : L₁.HasMapBifunctor L₂ F c
j j' : J
h : ¬c.Rel j' j
i₁ : I₁
i₂ : I₂
h' : c₁.π c₂ c (i₁, i₂) = j
h₃ : c₁.Rel (c₁.prev i₁) i₁
h₄ : c₁.π c₂ c (c₁.prev i₁, i₂) = j'
⊢ c.Rel (c₁.π c₂ c (c₁.prev i₁, i₂)) (c₁.π c₂ c (i₁, i₂))

Tactic:
ComplexShape.rel_π₁ c₂ c h₃ i₂

Premises used: ComplexShape.rel_π₁