awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ Hom.f (nullHomotopicMap fun (i j : ι) ↦ dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) ↦ 0) k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
have rw : (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun (x : ¬c.Rel k₁ k₀) ↦ 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
Tactic: rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun (x : ¬c.Rel k₁ k₀) ↦ 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
have split_ifs : C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₀ = 0
have dsimp : CategoryStruct.comp (Y := C.X (c.next k₀)) (C.d k₀ (c.next k₀)) (hom (c.next k₀) k₀) +
    CategoryStruct.comp (Y := D.X (c.prev k₀)) (hom k₀ (c.prev k₀)) (D.d (c.prev k₀) k₀) =
  0
Tactic: dsimp [nullHomotopicMap, dNext, prevD]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ CategoryStruct.comp (Y := C.X (c.next k₀)) (C.d k₀ (c.next k₀)) (hom (c.next k₀) k₀) +
      CategoryStruct.comp (Y := D.X (c.prev k₀)) (hom k₀ (c.prev k₀)) (D.d (c.prev k₀) k₀) =
    0
have a : ¬c.Rel (c.prev k₀) k₀
Tactic: rw [C.shape, D.shape, zero_comp, comp_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
a : ¬c.Rel (c.prev k₀) k₀
⊢ CategoryStruct.comp (Y := C.X (c.next k₀)) (C.d k₀ (c.next k₀)) (hom (c.next k₀) k₀) +
      CategoryStruct.comp (Y := D.X (c.prev k₀)) (hom k₀ (c.prev k₀)) (D.d (c.prev k₀) k₀) =
    0
have a₁ : ¬c.Rel k₀ (c.next k₀)
Tactic: rw [C.shape, D.shape, zero_comp, comp_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ (prevD j : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X j ⟶ Q.X j) f =
    CategoryStruct.comp (Y := Q.X (j + 1)) (f j (j + 1)) (Q.d (j + 1) j)
have dsimp : CategoryStruct.comp (Y := Q.X ((ComplexShape.down ℕ).prev j)) (f j ((ComplexShape.down ℕ).prev j))
    (Q.d ((ComplexShape.down ℕ).prev j) j) =
  CategoryStruct.comp (Y := Q.X (j + 1)) (f j (j + 1)) (Q.d (j + 1) j)
Tactic: dsimp [prevD]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (hypothesis)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ CategoryStruct.comp (Y := Q.X ((ComplexShape.down ℕ).prev j)) (f j ((ComplexShape.down ℕ).prev j))
      (Q.d ((ComplexShape.down ℕ).prev j) j) =
    CategoryStruct.comp (Y := Q.X (j + 1)) (f j (j + 1)) (Q.d (j + 1) j)
have this : (ComplexShape.down ℕ).prev j = j + 1
Tactic: have : (ComplexShape.down ℕ).prev j = j + 1 := ChainComplex.prev ℕ j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
    ((dNext (i + 1) : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X (i + 1) ⟶ Q.X (i + 1)) f : P.X (i + 1) ⟶ Q.X (i + 1))
    (P.d (i + 1) i ≫ f i (i + 1) : P.X (i + 1) ⟶ Q.X (i + 1))
have dsimp : Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
  (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next (i + 1)))
    (P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1))) (f ((ComplexShape.down ℕ).next (i + 1)) (i + 1)))
  (P.d (i + 1) i ≫ f i (i + 1))
Tactic: dsimp [dNext]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (hypothesis)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
    (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next (i + 1)))
      (P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1))) (f ((ComplexShape.down ℕ).next (i + 1)) (i + 1)))
    (P.d (i + 1) i ≫ f i (i + 1))
have this : (ComplexShape.down ℕ).next (i + 1) = i
Tactic: have : (ComplexShape.down ℕ).next (i + 1) = i := ChainComplex.next_nat_succ _
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ Eq (α := P.X 0 ⟶ Q.X 0) ((dNext 0 : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X 0 ⟶ Q.X 0) f : P.X 0 ⟶ Q.X 0)
    (0 : P.X 0 ⟶ Q.X 0)
have dsimp : Eq (α := P.X 0 ⟶ Q.X 0)
  (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next 0)) (P.d 0 ((ComplexShape.down ℕ).next 0))
    (f ((ComplexShape.down ℕ).next 0) 0))
  0
Tactic: dsimp [dNext]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ Eq (α := P.X 0 ⟶ Q.X 0)
    (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next 0)) (P.d 0 ((ComplexShape.down ℕ).next 0))
      (f ((ComplexShape.down ℕ).next 0) 0))
    0
have a : ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)
Tactic: rw [P.shape, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)
have a : ¬(ComplexShape.down ℕ).Rel 0 0
Tactic: rw [ChainComplex.next_nat_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
i j : ℕ
h : i + 1 = j
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
            (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
        (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
        e.f i =
          dFrom P i ≫
              (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
            f' ≫ dTo Q i) ≫
      (xPrevIso Q h).hom =
    (xNextIso P h).inv ≫
      (mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : xNext P j ⟶ Q.X j) ↦
        (f' : P.X j ⟶ xPrev Q j) ×' e.f j = dFrom P j ≫ f + f' ≫ dTo Q j)
have subst : (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
          (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
      (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
      e.f i =
        dFrom P i ≫
            (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
              (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
          f' ≫ dTo Q i) ≫
    (xPrevIso Q sorry).hom =
  (xNextIso P sorry).inv ≫
    PSigma.fst (β := fun (f : xNext P (i + 1) ⟶ Q.X (i + 1)) ↦
      (f' : P.X (i + 1) ⟶ xPrev Q (i + 1)) ×' e.f (i + 1) = dFrom P (i + 1) ≫ f + f' ≫ dTo Q (i + 1))
      (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1))
Tactic: subst j
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
            (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
        (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
        e.f i =
          dFrom P i ≫
              (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
            f' ≫ dTo Q i) ≫
      (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f : xNext P (i + 1) ⟶ Q.X (i + 1)) ↦
        (f' : P.X (i + 1) ⟶ xPrev Q (i + 1)) ×' e.f (i + 1) = dFrom P (i + 1) ≫ f + f' ≫ dTo Q (i + 1))
        (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1))
have zero₁ : PSigma.fst (β := fun (f' : P.X 0 ⟶ xPrev Q 0) ↦
      e.f 0 =
        dFrom P 0 ≫
            PSigma.fst (β := fun (f : xNext P 0 ⟶ Q.X 0) ↦
              (f' : P.X 0 ⟶ xPrev Q 0) ×' e.f 0 = dFrom P 0 ≫ f + f' ≫ dTo Q 0)
              (mkInductiveAux₂ e zero comm_zero one comm_one succ 0) +
          f' ≫ dTo Q 0)
      (PSigma.snd (β := fun (f : xNext P 0 ⟶ Q.X 0) ↦ (f' : P.X 0 ⟶ xPrev Q 0) ×' e.f 0 = dFrom P 0 ≫ f + f' ≫ dTo Q 0)
        (mkInductiveAux₂ e zero comm_zero one comm_one succ 0)) ≫
    (xPrevIso Q sorry).hom =
  (xNextIso P sorry).inv ≫
    PSigma.fst (β := fun (f : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ↦
      (f' : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ×'
        e.f (HAdd.hAdd (α := ℕ) 0 1) = dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f + f' ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1))
      (mkInductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1))
Tactic: rcases i with (_ | _ | i)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i_1 : ι
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel j i
⊢ Eq.{v + 1} (α := P.X i ⟶ Q.X j)
    (if h : i + 1 = j then
      (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
              (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
          (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
          e.f i =
            dFrom P i ≫
                (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                  (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
              f' ≫ dTo Q i) ≫
        (xPrevIso Q h).hom
    else 0)
    0
have hnc : ¬i + 1 = j
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i_1 : ι
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
      (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) =
    (fromNext i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → xNext P i ⟶ Q.X i) fun (i j : ℕ) ↦
      if h : i + 1 = j then
        (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
                (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
            (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
            e.f i =
              dFrom P i ≫
                  (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                    (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
                f' ≫ dTo Q i) ≫
          (xPrevIso Q h).hom
      else 0
have e_a : Eq (α := xNext P 0 ⟶ Q.X 0)
  (PSigma.fst (β := fun (f : xNext P 0 ⟶ Q.X 0) ↦ (f' : P.X 0 ⟶ xPrev Q 0) ×' e.f 0 = dFrom P 0 ≫ f + f' ≫ dTo Q 0)
    (mkInductiveAux₂ e zero comm_zero one comm_one succ 0))
  ((fromNext 0 : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → xNext P 0 ⟶ Q.X 0) fun (i j : ℕ) ↦
    if h : i + 1 = j then
      (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
              (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
          (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
          e.f i =
            dFrom P i ≫
                (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                  (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
              f' ≫ dTo Q i) ≫
        (xPrevIso Q h).hom
    else 0)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
n : ℕ
⊢ Iso.hom (xNextIso P ⋯) ≫
      (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) =
    (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f : xNext P (n + 1) ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1) ⟶ xPrev Q (n + 1)) ×' e.f (n + 1) = dFrom P (n + 1) ≫ f + f' ≫ dTo Q (n + 1))
        (mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1))
have e_a : eqToHom sorry ≫
    (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
      (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) =
  𝟙 (xNext P (n + 1)) ≫
    eqToHom sorry ≫
      (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1))
Tactic: dsimp [xNextIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
n : ℕ
⊢ eqToHom ⋯ ≫
      (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) =
    𝟙 (xNext P (n + 1)) ≫
      eqToHom ⋯ ≫
        (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1))
have e_a : eqToHom sorry ≫
    (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
      (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) =
  eqToHom sorry ≫
    (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
      (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1))
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ (dNext j : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X j ⟶ Q.X j) f =
    CategoryStruct.comp (Y := P.X (j + 1)) (P.d j (j + 1)) (f (j + 1) j)
have dsimp : CategoryStruct.comp (Y := P.X ((ComplexShape.up ℕ).next j)) (P.d j ((ComplexShape.up ℕ).next j))
    (f ((ComplexShape.up ℕ).next j) j) =
  CategoryStruct.comp (Y := P.X (j + 1)) (P.d j (j + 1)) (f (j + 1) j)
Tactic: dsimp [dNext]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (hypothesis)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ CategoryStruct.comp (Y := P.X ((ComplexShape.up ℕ).next j)) (P.d j ((ComplexShape.up ℕ).next j))
      (f ((ComplexShape.up ℕ).next j) j) =
    CategoryStruct.comp (Y := P.X (j + 1)) (P.d j (j + 1)) (f (j + 1) j)
have this : (ComplexShape.up ℕ).next j = j + 1
Tactic: have : (ComplexShape.up ℕ).next j = j + 1 := CochainComplex.next ℕ j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
    ((prevD (i + 1) : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X (i + 1) ⟶ Q.X (i + 1)) f : P.X (i + 1) ⟶ Q.X (i + 1))
    (f (i + 1) i ≫ Q.d i (i + 1) : P.X (i + 1) ⟶ Q.X (i + 1))
have dsimp : Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
  (CategoryStruct.comp (Y := Q.X ((ComplexShape.up ℕ).prev (i + 1))) (f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)))
    (Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1)))
  (f (i + 1) i ≫ Q.d i (i + 1))
Tactic: dsimp [prevD]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (hypothesis)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
    (CategoryStruct.comp (Y := Q.X ((ComplexShape.up ℕ).prev (i + 1))) (f (i + 1) ((ComplexShape.up ℕ).prev (i + 1)))
      (Q.d ((ComplexShape.up ℕ).prev (i + 1)) (i + 1)))
    (f (i + 1) i ≫ Q.d i (i + 1))
have this : (ComplexShape.up ℕ).prev (i + 1) = i
Tactic: have : (ComplexShape.up ℕ).prev (i + 1) = i := CochainComplex.prev_nat_succ i