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
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
            (c.next j) :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
      (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
have neg : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
  (CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
      (0 :
        X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
          (HomologicalComplex₂.toGradedObject
                (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
            (c₁.π c₂ c) (c.next j))
      (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
  (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
Tactic: rw [HomologicalComplex₂.d₂_eq_zero _ _ _ _ _ h₄, zero_comp]
-- 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
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
neg :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (0 :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
      (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (CategoryStruct.comp (Y := (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X).mapObj (c₁.π c₂ c) (c.next j))
        (HomologicalComplex₂.d₂ (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) c i₁ i₂
            (c.next j) :
          X (X (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂) i₁) i₂ ⟶
            (HomologicalComplex₂.toGradedObject
                  (Functor.obj (Functor.obj (F.mapBifunctorHomologicalComplex c₁ c₂) K₁) K₂)).mapObj
              (c₁.π c₂ c) (c.next j))
        (hom₁ h₁ f₂ F c (c.next j) j : X (K₁.mapBifunctor K₂ F c) (c.next j) ⟶ X (L₁.mapBifunctor L₂ F c) j) :
      (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
    (0 : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ X (L₁.mapBifunctor L₂ F c) j)
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 [HomologicalComplex₂.d₂_eq_zero _ _ _ _ _ h₄, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_2, u_2, 0} C₂ ℤ ⥤ CochainComplex.{v_3, u_3, 0} D ℤ)
      (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁)
      (obj F.map₂CochainComplex L₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
    (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n) ≫
      whiskerRight (map F.map₂CochainComplex f) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
    (whiskerLeft (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) (map F.map₂CochainComplex f) ≫
      Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n))
have w : ∀ (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ) (d : ℤ),
  Eq (α :=
    X (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁) K₂) d ⟶
      X (obj (obj F.map₂CochainComplex L₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₂) d)
    (Hom.f
      (NatTrans.app
        (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n) ≫
          whiskerRight (map F.map₂CochainComplex f) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
        K₂)
      d)
    (Hom.f
      (NatTrans.app
        (whiskerLeft (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) (map F.map₂CochainComplex f) ≫
          Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n))
        K₂)
      d)
Tactic: ext K₂ d
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ L₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
d : ℤ
⊢ Eq (α :=
    X (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n ⋙ obj F.map₂CochainComplex K₁) K₂) d ⟶
      X (obj (obj F.map₂CochainComplex L₁ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₂) d)
    (Hom.f
      (NatTrans.app
        (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n) ≫
          whiskerRight (map F.map₂CochainComplex f) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
        K₂)
      d)
    (Hom.f
      (NatTrans.app
        (whiskerLeft (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) (map F.map₂CochainComplex f) ≫
          Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n))
        K₂)
      d)
have w : Eq (α :=
  X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
    X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
  (CategoryStruct.comp (Y := X (mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)) (d + n))
      (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex K₁) n)) K₂) d)
      (Hom.f (mapBifunctorMap f (𝟙 K₂) F (ComplexShape.up ℤ)) (d + n)) :
    X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
      X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
  (CategoryStruct.comp (Y :=
      X (mapBifunctor L₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
      (Hom.f (mapBifunctorMap f (𝟙 (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂)) F (ComplexShape.up ℤ))
        d)
      (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj F.map₂CochainComplex L₁) n)) K₂) d) :
    X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d ⟶
      X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext K₂ n
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂_1 : CochainComplex.{v_2, u_2, 0} C₂ ℤ
K₂ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
n : ℤ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have w : Eq (α :=
  X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ)) n ⟶
    X (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)) (n + 0))
  (Hom.f (Iso.hom (K₂.mapBifunctorShift₁Iso K₂_1 F 0)) n :
    X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ))
        n ⟶
      X (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0) (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
        n)
  (Hom.f (NatTrans.app (Iso.hom (CommShift.isoZero (obj (Functor.flip F.map₂CochainComplex) K₂_1) ℤ)) K₂) n :
    X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ))
        n ⟶
      X (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0) (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
        n)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
a b : ℤ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext K₂ n
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂_1 : CochainComplex.{v_2, u_2, 0} C₂ ℤ
a b : ℤ
K₂ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
n : ℤ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂_1 : CochainComplex.{v_2, u_2, 0} C₂ ℤ
a b : ℤ
K₂ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
n : ℤ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext p q h
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_1, u_1, 0} C₁ ℤ ⥤ CochainComplex.{v_3, u_3, 0} D ℤ)
      (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n ⋙ obj (Functor.flip F.map₂CochainComplex) K₂)
      (obj (Functor.flip F.map₂CochainComplex) L₂ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
    (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) n) ≫
      whiskerRight (map (Functor.flip F.map₂CochainComplex) g) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
    (whiskerLeft (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) (map (Functor.flip F.map₂CochainComplex) g) ≫
      Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) L₂) n))
have w : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (d : ℤ),
  Eq (α :=
    X (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n ⋙ obj (Functor.flip F.map₂CochainComplex) K₂) K₁) d ⟶
      X (obj (obj (Functor.flip F.map₂CochainComplex) L₂ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₁) d)
    (Hom.f
      (NatTrans.app
        (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) n) ≫
          whiskerRight (map (Functor.flip F.map₂CochainComplex) g) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
        K₁)
      d)
    (Hom.f
      (NatTrans.app
        (whiskerLeft (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) (map (Functor.flip F.map₂CochainComplex) g) ≫
          Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) L₂) n))
        K₁)
      d)
Tactic: ext K₁ d
-- Lean 4 proof step from Mathlib.Algebra.Homology.BifunctorShift (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 : Preadditive.{v_1, u_1} C₁
inst_4 : Preadditive.{v_2, u_2} C₂
inst_5 : Preadditive.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : F.Additive
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst_8 : ∀ (K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ) (K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
K₁ : CochainComplex.{v_1, u_1, 0} C₁ ℤ
d : ℤ
⊢ Eq (α :=
    X (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n ⋙ obj (Functor.flip F.map₂CochainComplex) K₂) K₁) d ⟶
      X (obj (obj (Functor.flip F.map₂CochainComplex) L₂ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₁) d)
    (Hom.f
      (NatTrans.app
        (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) n) ≫
          whiskerRight (map (Functor.flip F.map₂CochainComplex) g) (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n))
        K₁)
      d)
    (Hom.f
      (NatTrans.app
        (whiskerLeft (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) (map (Functor.flip F.map₂CochainComplex) g) ≫
          Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) L₂) n))
        K₁)
      d)
have w : Eq (α :=
  X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) K₂ F (ComplexShape.up ℤ)) d ⟶
    X (mapBifunctor K₁ L₂ F (ComplexShape.up ℤ)) (d + n))
  (CategoryStruct.comp (Y := X (mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)) (d + n))
      (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) n)) K₁) d)
      (Hom.f (mapBifunctorMap (𝟙 K₁) g F (ComplexShape.up ℤ)) (d + n)) :
    X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) K₂ F (ComplexShape.up ℤ)) d ⟶
      X (mapBifunctor K₁ L₂ F (ComplexShape.up ℤ)) (d + n))
  (CategoryStruct.comp (Y :=
      X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) L₂ F (ComplexShape.up ℤ)) d)
      (Hom.f (mapBifunctorMap (𝟙 (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁)) g F (ComplexShape.up ℤ))
        d)
      (Hom.f (NatTrans.app (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) L₂) n)) K₁) d) :
    X (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n) K₁) K₂ F (ComplexShape.up ℤ)) d ⟶
      X (mapBifunctor K₁ L₂ F (ComplexShape.up ℤ)) (d + n))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
p q : ℤ
hpq : ¬(ComplexShape.up ℤ).Rel q p
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor (opEquivalence C)) (op L)).X p ⟶
      (Functor.obj (Equivalence.functor (opEquivalence C)) (op K)).X q)
    (Quiver.Hom.op (h.hom (-q) (-p))) 0
have a : ¬(ComplexShape.up ℤ).Rel (-p) (-q)
Tactic: rw [h.zero, op_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.CochainComplexOpposite (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
    (Quiver.Hom.op ((prevD (-n) : (a : (i j : ℤ) → K.X i ⟶ L.X j) → K.X (-n) ⟶ L.X (-n)) h.hom) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
    (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
              (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
              (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
            ((i j : ℤ) →
                ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
                  ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
              (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
                ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
          (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
        fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)) :
      op (L.X (-n)) ⟶ op (K.X (-n)))
have e_a : Eq (α := op (L.X (-n)) ⟶ op (K.X (-n)))
  (Quiver.Hom.op (CategoryStruct.comp (Y := L.X (-(n + 1))) (h.hom (-n) (-(n + 1))) (L.d (-(n + 1)) (-n))))
  (((dNext.{v_1, u_1, 0} (V := Cᵒᵖ) (c := ComplexShape.up ℤ) (C :=
          (HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt) (D :=
          (HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt) n :
        ((i j : ℤ) →
            ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X i ⟶
              ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X j) →+
          (((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).X n ⟶
            ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).X n)) :
      (a : (i j : ℤ) → op (L.X (-i)) ⟶ op (K.X (-j))) → op (L.X (-n)) ⟶ op (K.X (-n)))
    fun (p q : ℤ) ↦ Quiver.Hom.op (h.hom (-q) (-p)))
Tactic: rw [prevD_eq _ (j' := - (n + 1)) (by simp)]