awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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
⊢ 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')
have 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')
Tactic: ext i₁ i₂ h'
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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
⊢ 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')
have 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)
Tactic: dsimp [hom₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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
⊢ 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)
have 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
Tactic: rw [comp_zero, HomologicalComplex₂.ι_totalDesc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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
⊢ 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
have 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
Tactic: by_cases h₃ : c₁.Rel (c₁.prev i₁) i₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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
⊢ 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
have 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
Tactic: by_cases h₃ : c₁.Rel (c₁.prev i₁) i₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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₁
⊢ 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
have pos : c₁.π c₂ c (c₁.prev i₁, i₂) ≠ j'
Tactic: rw [ιMapBifunctorOrZero_eq_zero, comp_zero, comp_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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'
⊢ False
have pos : c.Rel j' j
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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 j' j
have pos : c.Rel (c₁.π c₂ c (c₁.prev i₁, i₂)) (c₁.π c₂ c (i₁, i₂))
Tactic: rw [← h', ← h₄]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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₁
⊢ 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
have neg : 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 0) (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 [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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₁
neg :
  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 0) (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
have neg₁ : 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 0 (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 [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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₁
neg :
  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 0) (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₁ :
  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 0 (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
have neg₂ : 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₂))
    (0 ≫ (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
  0
Tactic: rw [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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₁
neg :
  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 0) (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₁ :
  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 0 (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₂ :
  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₂))
      (0 ≫ (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
have neg₃ : 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₂)) 0 = 0
Tactic: rw [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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₁
neg :
  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 0) (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₁ :
  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 0 (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₂ :
  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₂))
      (0 ≫ (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ j') =
    0
neg₃ :
  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₂)) 0 = 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
have neg₄ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j') 0 0
Tactic: rw [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorHomotopy (goal)
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₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
⊢ c₁.π c₂ c (i₁, i₂') = j
have rw : c₁.π c₂ c (i₁, i₂') = c₁.π c₂ c (i₁', i₂)
Tactic: rw [← hj, ← ComplexShape.next_π₂ c₁ c i₁ hi₂, ComplexShape.next_π₁ c₂ c hi₁ i₂]