awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
j n : ℕ
⊢ (ComplexShape.up ℕ).Rel (n + 1) (j + 1 + 1) →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (n + 1) ⟶ C.X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (n + 1))
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x)
            n + 1 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (n + 1)))
          (C.d (n + 1) (j + 1 + 1)) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (n + 1) ⟶ C.X (j + 1 + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d (n + 1) (j + 1 + 1))
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x)
            j + 1 + 1 with
          | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (n + 1))) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (n + 1) ⟶ C.X (j + 1 + 1))

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i : ℕ
zero :
  (ComplexShape.up ℕ).Rel 0 0 →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d 0 0) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d 0 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
zero₁ :
  ∀ (i : ℕ),
    (ComplexShape.up ℕ).Rel (i + 1) 0 →
      Eq.{v + 1} (α := C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
        (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (i + 1))
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
              i + 1 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1)))
            (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d (i + 1) 0) :
          C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
        (CategoryStruct.comp (Y := C.X 0) (C.d (i + 1) 0)
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1))) :
          C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
⊢ (ComplexShape.up ℕ).Rel i 0 →
    Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      ((match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) i with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) ≫
          ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d i 0 :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d i 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)

Tactic:
rcases i with - | i
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i j : ℕ
succ :
  (ComplexShape.up ℕ).Rel 0 (j + 1 + 1) →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d 0 (j + 1 + 1)) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d 0 (j + 1 + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            j + 1 + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
succ₁ :
  ∀ (i : ℕ),
    (ComplexShape.up ℕ).Rel (i + 1) (j + 1 + 1) →
      Eq.{v + 1} (α := C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
        (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (i + 1))
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
              i + 1 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1)))
            (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d (i + 1) (j + 1 + 1)) :
          C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
        (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d (i + 1) (j + 1 + 1))
            (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
              j + 1 + 1 with
            | 0 => 𝟙 (C.X 0)
            | n.succ => 𝟙 (C.X (n + 1))) :
          C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      ((match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) i with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) ≫
          ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d i (j + 1 + 1) :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d i (j + 1 + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            j + 1 + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))

Tactic:
rcases i with - | i
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
⊢ (ComplexShape.up ℕ).Rel 0 0 →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d 0 0) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d 0 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel (i + 1) 0 →
    Eq.{v + 1} (α := C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (i + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            i + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d (i + 1) 0) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
      (CategoryStruct.comp (Y := C.X 0) (C.d (i + 1) 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
⊢ (ComplexShape.up ℕ).Rel 0 (HAdd.hAdd (α := ℕ) 0 1) →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))
      (CategoryStruct.comp (Y := C.X (HAdd.hAdd (α := ℕ) 0 1)) (C.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            HAdd.hAdd (α := ℕ) 0 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel (i + 1) (HAdd.hAdd (α := ℕ) 0 1) →
    Eq.{v + 1} (α :=
      C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (i + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            i + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d (i + 1) (HAdd.hAdd (α := ℕ) 0 1)) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))
      (CategoryStruct.comp (Y := C.X (HAdd.hAdd (α := ℕ) 0 1)) (C.d (i + 1) (HAdd.hAdd (α := ℕ) 0 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            HAdd.hAdd (α := ℕ) 0 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
j : ℕ
⊢ (ComplexShape.up ℕ).Rel 0 (j + 1 + 1) →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d 0 (j + 1 + 1)) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d 0 (j + 1 + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            j + 1 + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
j i : ℕ
⊢ (ComplexShape.up ℕ).Rel (i + 1) (j + 1 + 1) →
    Eq.{v + 1} (α := C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (i + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            i + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d (i + 1) (j + 1 + 1)) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d (i + 1) (j + 1 + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            j + 1 + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
⊢ Eq (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0 ⟶ C.X 0) (C.augmentTruncate.hom.f 0)
    (𝟙 (C.X 0))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ Eq (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (i + 1) ⟶ C.X (i + 1))
    (C.augmentTruncate.hom.f (i + 1)) (𝟙 (C.X (i + 1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
⊢ C.augmentTruncate.inv.f 0 = 𝟙 (C.X 0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Augment
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i : ℕ
⊢ C.augmentTruncate.inv.f (i + 1) = 𝟙 (C.X (i + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
dsimp :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) 0
⊢ Eq.{v_3 + 1} (α :=
    ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂) ⟶
      ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁', i₂))
    ((fun (i₁ i₁' : I₁) (i₂ : I₂) ↦
        ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)))
      i₁ i₁' i₂)
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
rw₁ :
  Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) (NatTrans.app 0 (K₂.X i₂)) 0
rw₂ rw₃ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) 0 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) 0

Tactic:
rw [K₁.shape _ _ h₁, Functor.map_zero, zero_app]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.zero_app, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ : I₁
i₂ i₂' : I₂
h₂ : ¬c₂.Rel i₂ i₂'
dsimp : (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') = 0
⊢ Eq.{v_3 + 1} (α :=
    ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂) ⟶
      ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂'))
    ((fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) i₁ i₂ i₂') 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ : I₁
i₂ i₂' : I₂
h₂ : ¬c₂.Rel i₂ i₂'
rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂')) ((F.obj (K₁.X i₁)).map 0) 0
rw₁ rw₂ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂')) 0 0
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') = 0

Tactic:
rw [K₂.shape _ _ h₂, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
dsimp :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
⊢ Eq.{v_3 + 1} (α :=
    ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁, i₂) ⟶
      ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁'', i₂))
    (CategoryStruct.comp (Y := ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X (i₁', i₂))
      ((fun (i₁ i₁' : I₁) (i₂ : I₂) ↦
          ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)))
        i₁ i₁' i₂)
      ((fun (i₁ i₁' : I₁) (i₂ : I₂) ↦
          ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) : (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)))
        i₁' i₁'' i₂))
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Bifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
rw :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁') ≫ F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
rw₁ :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁' ≫ K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
rw₂ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
rw₃ :
  Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) (NatTrans.app 0 (K₂.X i₂)) 0
rw₄ rw₅ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) 0 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0

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

Premises used: CategoryTheory.Functor.map_zero, HomologicalComplex.d_comp_d, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.zero_app, CategoryTheory.NatTrans.comp_app