awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = d
⊢ Eq (α :=
    (F.obj (K₁.X p)).obj ((obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂).X q) ⟶
      X (mapBifunctor L₁ K₂ F (ComplexShape.up ℤ)) (d + n))
    (CategoryStruct.comp (Y :=
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
      (ιMapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ) p q d h)
      (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))))
    (CategoryStruct.comp (Y :=
      X (mapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ)) d)
      (ιMapBifunctor K₁ (obj (shiftFunctor (CochainComplex.{v_2, u_2, 0} C₂ ℤ) n) K₂) F (ComplexShape.up ℤ) p q d h)
      (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)))

Tactic:
simp [commShiftIso_map₂CochainComplex_hom_app,
      CochainComplex.ι_mapBifunctorShift₂Iso_hom_f _ _ _ _ _ _ _ _ (q + n) (d + n) rfl rfl,
      CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc _ _ _ _ _ _ _ _ (q + n) (d + n) rfl rfl]

Premises used: CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, HAdd.hAdd, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app, rfl
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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₂ ℤ
w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext K₂ n
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : ℤ
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n
⊢ p = p + 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n
⊢ n = n + 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n
⊢ Eq (α :=
    (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
      X (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0) (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
        n)
    (CategoryStruct.comp (Y :=
        X
          (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F
            (ComplexShape.up ℤ))
          n)
        (ιMapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ)
            p q n h :
          (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
            X
              (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F
                (ComplexShape.up ℤ))
              n)
        (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) :
      (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
        X
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0)
            (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
          n)
    (CategoryStruct.comp (Y :=
        X
          (mapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F
            (ComplexShape.up ℤ))
          n)
        (ιMapBifunctor (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂) K₂_1 F (ComplexShape.up ℤ)
          p q n h)
        (Hom.f (NatTrans.app (Iso.hom (CommShift.isoZero (obj (Functor.flip F.map₂CochainComplex) K₂_1) ℤ)) K₂) n) :
      (F.obj ((obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) (A := ℤ) 0) K₂).X p)).obj (K₂_1.X q) ⟶
        X
          (obj (shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) (A := ℤ) 0)
            (mapBifunctor K₂ K₂_1 F (ComplexShape.up ℤ)))
          n)

Tactic:
simp [CochainComplex.ι_mapBifunctorShift₁Iso_hom_f _ _ F 0 p q n h p n
      (by lia) (by lia), CochainComplex.shiftFunctorZero_eq]

Premises used: CochainComplex.shiftFunctorZero_eq, OfNat.ofNat, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : ℤ
w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext K₂ n
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : ℤ
w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : ℤ
w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext p q h
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : p + q = n
⊢ p + a + b = p + (a + b)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : p + q = n
⊢ n + a + b = n + (a + b)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : p + q = n
⊢ p + b + q = n + b

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : p + q = n
⊢ p + a + b = p + b + a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : p + q = n
⊢ n + a + b = n + b + a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 p q : ℤ
h : p + q = n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [CochainComplex.ι_mapBifunctorShift₁Iso_hom_f _ _ F (a + b) p q n h
        (p + a + b) (n + a + b) (by lia) (by lia),
      CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc _ _ F b p q n h _ _ rfl rfl,
      CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc _ _ F a (p + b) q (n + b)
        (by lia) (p + a + b) (n + a + b) (by lia) (by lia),
      CochainComplex.shiftFunctorAdd_eq, XIsoOfEq, eqToHom_map]

Premises used: CategoryTheory.eqToHom_map, HomologicalComplex.XIsoOfEq, CochainComplex.shiftFunctorAdd_eq, HAdd.hAdd, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, rfl, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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_1, u_1, 0} C₁ ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
      (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n ⋙ obj (Functor.flip F.map₂CochainComplex) K₂) K₁)
      (obj (obj (Functor.flip F.map₂CochainComplex) K₂ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₁))
    (NatTrans.app (Iso.hom (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) n)) K₁)
    (Iso.hom (K₁.mapBifunctorShift₁Iso K₂ F n))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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_1, u_1, 0} C₁ ℤ
K₂ : CochainComplex.{v_2, u_2, 0} C₂ ℤ
n : ℤ
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_3, u_3, 0} D ℤ)
      (obj (obj (Functor.flip F.map₂CochainComplex) K₂ ⋙ shiftFunctor (CochainComplex.{v_3, u_3, 0} D ℤ) n) K₁)
      (obj (shiftFunctor (CochainComplex.{v_1, u_1, 0} C₁ ℤ) n ⋙ obj (Functor.flip F.map₂CochainComplex) K₂) K₁))
    (NatTrans.app (Iso.inv (commShiftIso (obj (Functor.flip F.map₂CochainComplex) K₂) n)) K₁)
    (Iso.inv (K₁.mapBifunctorShift₁Iso K₂ F n))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : ℤ
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)
⊢ 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))

Tactic:
ext K₁ d

Premises used: HomologicalComplex.d
-- Module: Mathlib.Algebra.Homology.BifunctorShift
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 : ℤ
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))
⊢ 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:
dsimp