awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ C.X j)
      ((match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x) i 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 i j :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ C.X j)
      (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d i j ≫
          match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x) j 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 i ⟶ C.X j)
have zero : (ComplexShape.up ℕ).Rel i 0 →
  Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X i ⟶ C.X 0)
    ((match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x) i with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1))) ≫
        C.d i 0 :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X i ⟶ C.X 0)
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).d i 0)
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x) 0 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1))) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X i ⟶ C.X 0)
Tactic: rcases j with (_ | _ | j)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
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 0 →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ C.X 0)
      ((match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x) i 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 i 0 :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ C.X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d i 0)
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x) 0 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 i ⟶ C.X 0)
have zero : (ComplexShape.up ℕ).Rel 0 0 →
  Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X 0)
    (CategoryStruct.comp (Y := C.X 0)
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x) 0 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1)))
        (C.d 0 0) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X 0)
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).d 0 0)
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x) 0 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1))) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X 0)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
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 (HAdd.hAdd (α := ℕ) 0 1) →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1))
      ((match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x) i 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 i (HAdd.hAdd (α := ℕ) 0 1) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d i (HAdd.hAdd (α := ℕ) 0 1))
          (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x)
            HAdd.hAdd (α := ℕ) 0 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 i ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1))
have succ : (ComplexShape.up ℕ).Rel 0 (HAdd.hAdd (α := ℕ) 0 1) →
  Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1))
    (CategoryStruct.comp (Y := C.X 0)
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x) 0 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1)))
        (C.d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1))
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (HAdd.hAdd (α := ℕ) 0 1))
        (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).d 0 (HAdd.hAdd (α := ℕ) 0 1))
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x)
          HAdd.hAdd (α := ℕ) 0 1 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1))) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X (HAdd.hAdd (α := ℕ) 0 1))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ C.X (j + 1 + 1))
      ((match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x ⟶ C.X x) i 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 i (j + 1 + 1) :
        ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X i ⟶ 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 i (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 i ⟶ C.X (j + 1 + 1))
have succ : (ComplexShape.up ℕ).Rel 0 (j + 1 + 1) →
  Eq.{v + 1} (α := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X (j + 1 + 1))
    (CategoryStruct.comp (Y := C.X 0)
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x) 0 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1)))
        (C.d 0 (j + 1 + 1)) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X (j + 1 + 1))
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (j + 1 + 1))
        (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).d 0 (j + 1 + 1))
        (match (motive := (x : ℕ) → ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x ⟶ C.X x)
          j + 1 + 1 with
        | 0 => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        | n.succ => 𝟙 (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (n + 1))) :
      ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0 ⟶ C.X (j + 1 + 1))
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j →
    Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X j)
      ((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 :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X j)
      (C.d i j ≫
          match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) j 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)
have zero : (ComplexShape.up ℕ).Rel i 0 →
  Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
    ((match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).d i 0 :
      C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).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) sorry).X 0)
Tactic: rcases j with (_ | _ | j)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i j : ℕ
zero :
  (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)
⊢ (ComplexShape.up ℕ).Rel i j →
    Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X j)
      ((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 :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X j)
      (C.d i j ≫
          match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) j 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)
have succ : (ComplexShape.up ℕ).Rel i (HAdd.hAdd (α := ℕ) 0 1) →
  Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (HAdd.hAdd (α := ℕ) 0 1))
    ((match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).d i (HAdd.hAdd (α := ℕ) 0 1) :
      C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (HAdd.hAdd (α := ℕ) 0 1))
    (CategoryStruct.comp (Y := C.X (HAdd.hAdd (α := ℕ) 0 1)) (C.d i (HAdd.hAdd (α := ℕ) 0 1))
        (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x)
          HAdd.hAdd (α := ℕ) 0 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) sorry).X (HAdd.hAdd (α := ℕ) 0 1))
Tactic: rcases j with (_ | _ | j)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
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 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)
have 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) sorry).X 0)
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).d 0 0) :
      C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).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) sorry).X 0)
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
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)
⊢ (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)
have 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) sorry).X 0)
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (i + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).d (i + 1) 0) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).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) sorry).X 0)
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
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 (HAdd.hAdd (α := ℕ) 0 1) →
    Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (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) 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 (HAdd.hAdd (α := ℕ) 0 1) :
        C.X i ⟶ ((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 (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 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (HAdd.hAdd (α := ℕ) 0 1))
have succ : (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) sorry).X (HAdd.hAdd (α := ℕ) 0 1))
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
      C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).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) sorry).X (HAdd.hAdd (α := ℕ) 0 1))
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i j : ℕ
⊢ (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))
have 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) sorry).X (j + 1 + 1))
    (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X 0)
        (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).d 0 (j + 1 + 1)) :
      C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).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) sorry).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) sorry).X (j + 1 + 1))
Tactic: rcases i with - | i
Cleared hypotheses: i