awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := P.X 0 ⟶ Q.X 0) ((prevD 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 := Q.X ((ComplexShape.up ℕ).prev 0)) (f 0 ((ComplexShape.up ℕ).prev 0))
    (Q.d ((ComplexShape.up ℕ).prev 0) 0))
  0
Tactic: dsimp [prevD]
-- 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
⊢ Eq (α := P.X 0 ⟶ Q.X 0)
    (CategoryStruct.comp (Y := Q.X ((ComplexShape.up ℕ).prev 0)) (f 0 ((ComplexShape.up ℕ).prev 0))
      (Q.d ((ComplexShape.up ℕ).prev 0) 0))
    0
have a : ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
Tactic: rw [Q.shape, comp_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 : CochainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
have a : ¬(ComplexShape.up ℕ).Rel 0 0
Tactic: rw [CochainComplex.prev_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 : CochainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
        e.f (n + 2) =
          p.snd (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                    (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f').fst
                (β := fun (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ↦
                e.f (n + 1) =
                  p.fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                          e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
                      Q.d n (n + 1) +
                    P.d (n + 1) (n + 2) ≫ f') ≫
              Q.d (n + 1) (n + 2) +
            P.d (n + 2) (n + 3) ≫ f''
i j : ℕ
h : i + 1 = j
⊢ (xNextIso P h).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : P.X i ⟶ xPrev Q i) ↦
            (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f').fst
        (β := fun (f' : xNext P i ⟶ Q.X i) ↦
        e.f i =
          (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : P.X i ⟶ xPrev Q i) ↦
                (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f') ≫
              dTo Q i +
            dFrom P i ≫ f') =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
        (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
      (xPrevIso Q h).hom
have subst : (xNextIso P sorry).inv ≫
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : P.X i ⟶ xPrev Q i) ↦
          (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f').fst
      (β := fun (f' : xNext P i ⟶ Q.X i) ↦
      e.f i =
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : P.X i ⟶ xPrev Q i) ↦
              (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f') ≫
            dTo Q i +
          dFrom P i ≫ f') =
  PSigma.fst (β := fun (f : P.X (i + 1) ⟶ xPrev Q (i + 1)) ↦
      (f' : xNext P (i + 1) ⟶ Q.X (i + 1)) ×' e.f (i + 1) = f ≫ dTo Q (i + 1) + dFrom P (i + 1) ≫ f')
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)) ≫
    (xPrevIso Q sorry).hom
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 : CochainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
        e.f (n + 2) =
          p.snd (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                    (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f').fst
                (β := fun (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ↦
                e.f (n + 1) =
                  p.fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                          e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
                      Q.d n (n + 1) +
                    P.d (n + 1) (n + 2) ≫ f') ≫
              Q.d (n + 1) (n + 2) +
            P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P ⋯).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : P.X i ⟶ xPrev Q i) ↦
            (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f').fst
        (β := fun (f' : xNext P i ⟶ Q.X i) ↦
        e.f i =
          (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : P.X i ⟶ xPrev Q i) ↦
                (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f') ≫
              dTo Q i +
            dFrom P i ≫ f') =
    PSigma.fst (β := fun (f : P.X (i + 1) ⟶ xPrev Q (i + 1)) ↦
        (f' : xNext P (i + 1) ⟶ Q.X (i + 1)) ×' e.f (i + 1) = f ≫ dTo Q (i + 1) + dFrom P (i + 1) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)) ≫
      (xPrevIso Q ⋯).hom
have zero₁ : (xNextIso P sorry).inv ≫
    PSigma.fst (β := fun (f' : xNext P 0 ⟶ Q.X 0) ↦
      e.f 0 =
        PSigma.fst (β := fun (f : P.X 0 ⟶ xPrev Q 0) ↦ (f' : xNext P 0 ⟶ Q.X 0) ×' e.f 0 = f ≫ dTo Q 0 + dFrom P 0 ≫ f')
              (mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0) ≫
            dTo Q 0 +
          dFrom P 0 ≫ f')
      (PSigma.snd (β := fun (f : P.X 0 ⟶ xPrev Q 0) ↦ (f' : xNext P 0 ⟶ Q.X 0) ×' e.f 0 = f ≫ dTo Q 0 + dFrom P 0 ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0)) =
  PSigma.fst (β := fun (f : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ↦
      (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ×'
        e.f (HAdd.hAdd (α := ℕ) 0 1) = f ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1) + dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f')
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1)) ≫
    (xPrevIso Q sorry).hom
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 : CochainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
        e.f (n + 2) =
          p.snd (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                    (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f').fst
                (β := fun (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ↦
                e.f (n + 1) =
                  p.fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                          e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
                      Q.d n (n + 1) +
                    P.d (n + 1) (n + 2) ≫ f') ≫
              Q.d (n + 1) (n + 2) +
            P.d (n + 2) (n + 3) ≫ f''
i j : ℕ
w : ¬(ComplexShape.up ℕ).Rel j i
⊢ Eq.{v + 1} (α := P.X i ⟶ Q.X j)
    (if h : j + 1 = i then
      (xNextIso P h).inv ≫
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd (β := fun (f : P.X j ⟶ xPrev Q j) ↦
              (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f').fst
          (β := fun (f' : xNext P j ⟶ Q.X j) ↦
          e.f j =
            (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                  (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
                dTo Q j +
              dFrom P j ≫ f')
    else 0)
    0
have hnc : ¬j + 1 = i
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 : CochainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
        e.f (n + 2) =
          p.snd (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                    (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f').fst
                (β := fun (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ↦
                e.f (n + 1) =
                  p.fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                          e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
                      Q.d n (n + 1) +
                    P.d (n + 1) (n + 2) ≫ f') ≫
              Q.d (n + 1) (n + 2) +
            P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : P.X i ⟶ xPrev Q i) ↦
      (f' : xNext P i ⟶ Q.X i) ×' e.f i = f ≫ dTo Q i + dFrom P i ≫ f') =
    (toPrev i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X i ⟶ xPrev Q i) fun (i j : ℕ) ↦
      if h : j + 1 = i then
        (xNextIso P h).inv ≫
          (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f').fst
            (β := fun (f' : xNext P j ⟶ Q.X j) ↦
            e.f j =
              (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                    (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
                  dTo Q j +
                dFrom P j ≫ f')
      else 0
have e_a : Eq (α := P.X 0 ⟶ xPrev Q 0)
  (PSigma.fst (β := fun (f : P.X 0 ⟶ xPrev Q 0) ↦ (f' : xNext P 0 ⟶ Q.X 0) ×' e.f 0 = f ≫ dTo Q 0 + dFrom P 0 ≫ f')
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0))
  ((toPrev 0 : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X 0 ⟶ xPrev Q 0) fun (i j : ℕ) ↦
    if h : j + 1 = i then
      (xNextIso P h).inv ≫
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd (β := fun (f : P.X j ⟶ xPrev Q j) ↦
              (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f').fst
          (β := fun (f' : xNext P j ⟶ Q.X j) ↦
          e.f j =
            (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : P.X j ⟶ xPrev Q j) ↦
                  (f' : xNext P j ⟶ Q.X j) ×' e.f j = f ≫ dTo Q j + dFrom P j ≫ f') ≫
                dTo Q j +
              dFrom P j ≫ f')
    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 : CochainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
        e.f (n + 2) =
          p.snd (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                    (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f').fst
                (β := fun (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ↦
                e.f (n + 1) =
                  p.fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                          e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
                      Q.d n (n + 1) +
                    P.d (n + 1) (n + 2) ≫ f') ≫
              Q.d (n + 1) (n + 2) +
            P.d (n + 2) (n + 3) ≫ f''
n : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
      Iso.inv (xPrevIso Q ⋯) =
    PSigma.fst (β := fun (f : P.X (n + 1) ⟶ xPrev Q (n + 1)) ↦
        (f' : xNext P (n + 1) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ dTo Q (n + 1) + dFrom P (n + 1) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1)) ≫
      (xPrevIso Q ⋯).hom
have e_a : (mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
      (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
    eqToHom sorry =
  ((mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
      eqToHom sorry) ≫
    𝟙 (xPrev Q (n + 1))
Tactic: dsimp [xPrevIso]
-- 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 : CochainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
        e.f (n + 2) =
          p.snd (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                    (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f').fst
                (β := fun (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ↦
                e.f (n + 1) =
                  p.fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
                        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                          e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
                      Q.d n (n + 1) +
                    P.d (n + 1) (n + 2) ≫ f') ≫
              Q.d (n + 1) (n + 2) +
            P.d (n + 2) (n + 3) ≫ f''
n : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
        (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
      eqToHom ⋯ =
    ((mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
        eqToHom ⋯) ≫
      𝟙 (xPrev Q (n + 1))
have e_a : (mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
      (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
    eqToHom sorry =
  (mkCoinductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X (n + 1) ⟶ Q.X n) ↦
      (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') ≫
    eqToHom sorry
Tactic: rw [comp_id]
-- 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_1 g_1 : C ⟶ D
h_1 k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ F.map (h.hom i j) = 0
have rw : Eq (α := F.obj (C.X i) ⟶ F.obj (D.X j)) (F.map 0) 0
Tactic: rw [h.zero i j w, F.map_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 E : HomologicalComplex.{v, u, u_1} V c
f_1 g_1 : C ⟶ D
h_1 k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬c.Rel j i
rw : Eq (α := F.obj (C.X i) ⟶ F.obj (D.X j)) (F.map 0) 0
⊢ F.map (h.hom i j) = 0
have rw₁ : Eq.{v_1 + 1} (α := F.obj (C.X i) ⟶ F.obj (D.X j)) 0 0
Tactic: rw [h.zero i j w, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (hypothesis)
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_1 g_1 : C ⟶ D
h_1 k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ Hom.f (map (F.mapHomologicalComplex c) f) i =
    HAdd.hAdd (α := X (obj (F.mapHomologicalComplex c) C) i ⟶ X (obj (F.mapHomologicalComplex c) D) i)
        ((dNext i :
            (a : (i j : ι) → ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X j) →
              ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X i)
          fun (i j : ι) ↦ F.map (h.hom i j))
        ((prevD i :
            (a : (i j : ι) → ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X j) →
              ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X i)
          fun (i j : ι) ↦ F.map (h.hom i j)) +
      Hom.f (map (F.mapHomologicalComplex c) g) i
have H : f.f i =
  HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) +
    g.f i
Tactic: have H := h.comm 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_1 g_1 : C ⟶ D
h_1 k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
f g : C ⟶ D
h : Homotopy f g
i : ι
H :
  f.f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) h.hom : C.X i ⟶ D.X i) +
      g.f i
⊢ Hom.f (map (F.mapHomologicalComplex c) f) i =
    HAdd.hAdd (α := X (obj (F.mapHomologicalComplex c) C) i ⟶ X (obj (F.mapHomologicalComplex c) D) i)
        ((dNext i :
            (a : (i j : ι) → ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X j) →
              ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X i)
          fun (i j : ι) ↦ F.map (h.hom i j))
        ((prevD i :
            (a : (i j : ι) → ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X j) →
              ((F.mapHomologicalComplex c).obj C).X i ⟶ ((F.mapHomologicalComplex c).obj D).X i)
          fun (i j : ι) ↦ F.map (h.hom i j)) +
      Hom.f (map (F.mapHomologicalComplex c) g) i
have dsimp : F.map (f.f i) =
  CategoryStruct.comp (Y := F.obj (C.X (c.next i))) (F.map (C.d i (c.next i))) (F.map (h.hom (c.next i) i)) +
      CategoryStruct.comp (Y := F.obj (D.X (c.prev i))) (F.map (h.hom i (c.prev i))) (F.map (D.d (c.prev i) i)) +
    F.map (g.f i)
Tactic: dsimp [dNext, prevD] at H ⊢
-- 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_1 k : D ⟶ E
i : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
h : HomotopyEquiv C D
⊢ Homotopy (C := obj (F.mapHomologicalComplex c) C)
    (map (F.mapHomologicalComplex c) h.hom ≫ map (F.mapHomologicalComplex c) h.inv)
    (𝟙 (obj (F.mapHomologicalComplex c) C))
have rw : Homotopy (C := obj (F.mapHomologicalComplex c) C) (map (F.mapHomologicalComplex c) (h.hom ≫ h.inv))
  (map (F.mapHomologicalComplex c) (𝟙 C))
Tactic: rw [← (F.mapHomologicalComplex c).map_comp, ← (F.mapHomologicalComplex c).map_id]
-- 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_1 k : D ⟶ E
i : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
F : Functor.{v, v_1, u, u_2} V W
inst_4 : F.Additive
h : HomotopyEquiv C D
⊢ Homotopy (C := obj (F.mapHomologicalComplex c) D)
    (map (F.mapHomologicalComplex c) h.inv ≫ map (F.mapHomologicalComplex c) h.hom)
    (𝟙 (obj (F.mapHomologicalComplex c) D))
have rw : Homotopy (C := obj (F.mapHomologicalComplex c) D) (map (F.mapHomologicalComplex c) (h.inv ≫ h.hom))
  (map (F.mapHomologicalComplex c) (𝟙 D))
Tactic: rw [← (F.mapHomologicalComplex c).map_comp, ← (F.mapHomologicalComplex c).map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
⊢ (if c.Rel (c.prev i) i then
        CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
          (L.d (c.prev (c.prev i)) (c.prev i))
      else
        HSub.hSub (α := K.X (c.prev i) ⟶ L.X (c.prev i)) (f.f (c.prev i)) (g.f (c.prev i)) -
          K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫
      (Functor.obj (shortComplexFunctor C c i) L).f =
    0
have pos : ∀ (h : c.Rel (c.prev i) i),
  Eq (α := (Functor.obj (shortComplexFunctor C c i) K).X₁ ⟶ (Functor.obj (shortComplexFunctor C c i) L).X₂)
    (CategoryStruct.comp (Y := L.X (c.prev (c.prev i))) (ho.hom (c.prev i) (c.prev (c.prev i)))
        (L.d (c.prev (c.prev i)) (c.prev i)) ≫
      (Functor.obj (shortComplexFunctor C c i) L).f)
    0
Tactic: split_ifs with h