awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
⊢ i + 1 = (ComplexShape.down ℕ).prev i

Tactic:
simp only [ChainComplex.prev]

Premises used: ChainComplex.prev
-- Module: Mathlib.Algebra.Homology.Homotopy
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).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) =
    (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

Tactic:
simp [xPrevIso, comp_id]

Premises used: CategoryTheory.Category.comp_id, HomologicalComplex.xPrevIso
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
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)
⊢ (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)

Tactic:
dsimp [dNext]

Premises used: dNext
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
⊢ (ComplexShape.up ℕ).next j = j + 1

Tactic:
have : (ComplexShape.up ℕ).next j = j + 1 := CochainComplex.next ℕ j
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
this : (ComplexShape.up ℕ).next j = j + 1
⊢ 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:
congr 2
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
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))
⊢ 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))

Tactic:
dsimp [prevD]

Premises used: prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
⊢ (ComplexShape.up ℕ).prev (i + 1) = i

Tactic:
have : (ComplexShape.up ℕ).prev (i + 1) = i := CochainComplex.prev_nat_succ i
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
this : (ComplexShape.up ℕ).prev (i + 1) = 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))

Tactic:
congr 2
-- Module: Mathlib.Algebra.Homology.Homotopy
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
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
⊢ 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)

Tactic:
dsimp [prevD]

Premises used: prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
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
a : ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
⊢ 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:
rw [Q.shape, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Homotopy
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
a : ¬(ComplexShape.up ℕ).Rel 0 0
⊢ ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0

Tactic:
rw [CochainComplex.prev_nat_zero]

Premises used: CochainComplex.prev_nat_zero
-- Module: Mathlib.Algebra.Homology.Homotopy
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 (α := ℕ) 1 0

Tactic:
decide
-- Module: Mathlib.Algebra.Homology.Homotopy
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''
⊢ e.f 0 = 0 ≫ dTo Q 0 + dFrom P 0 ≫ Iso.hom (xNextIso P ⋯) ≫ zero

Tactic:
simpa using comm_zero
-- Module: Mathlib.Algebra.Homology.Homotopy
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 : ℕ
I : (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' :=
  mkCoinductiveAux₁ e zero one comm_one succ n
⊢ e.f (n + 1) =
    (I.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 ⋯)) ≫
        dTo Q (n + 1) +
      dFrom P (n + 1) ≫
        Iso.hom (xNextIso P ⋯) ≫
          I.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) =
              I.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')

Tactic:
simpa using I.2.2

Premises used: PSigma.snd
-- Module: Mathlib.Algebra.Homology.Homotopy
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''
⊢ mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 =
    PSigma.mk (β := 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') 0
      (PSigma.mk (β := fun (f' : xNext P 0 ⟶ Q.X 0) ↦ e.f 0 = 0 ≫ dTo Q 0 + dFrom P 0 ≫ f')
        (Iso.hom (xNextIso P ⋯) ≫ zero) ⋯)

Tactic:
rfl

Premises used: Homotopy.mkCoinductiveAux₂, rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
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''
n : ℕ
⊢ mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
    PSigma.mk (β := 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 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.mk (β := fun (f' : xNext P (n + 1) ⟶ Q.X (n + 1)) ↦
        e.f (n + 1) =
          ((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 ⋯)) ≫
              dTo Q (n + 1) +
            dFrom P (n + 1) ≫ f')
        (Iso.hom (xNextIso P ⋯) ≫
          (mkCoinductiveAux₁ e zero one comm_one succ n).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) =
              (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') ≫
                  Q.d n (n + 1) +
                P.d (n + 1) (n + 2) ≫ f'))
        ⋯)

Tactic:
rfl

Premises used: Homotopy.mkCoinductiveAux₂, rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
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
subst :
  (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
⊢ (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

Tactic:
subst j
-- Module: Mathlib.Algebra.Homology.Homotopy
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''
⊢ (xNextIso P ⋯).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 ⋯).hom

Tactic:
simp [mkCoinductiveAux₂]

Premises used: Homotopy.mkCoinductiveAux₂
-- Module: Mathlib.Algebra.Homology.Homotopy
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''
⊢ (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ↦
        e.f (HAdd.hAdd (α := ℕ) 0 1) =
          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)) ≫
              dTo Q (HAdd.hAdd (α := ℕ) 0 1) +
            dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f')
        (PSigma.snd (β := 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))) =
    PSigma.fst (β := fun (f : P.X (HAdd.hAdd (α := ℕ) 0 1 + 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1 + 1)) ↦
        (f' : xNext P (HAdd.hAdd (α := ℕ) 0 1 + 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ×'
          e.f (HAdd.hAdd (α := ℕ) 0 1 + 1) =
            f ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1 + 1) + dFrom P (HAdd.hAdd (α := ℕ) 0 1 + 1) ≫ f')
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1 + 1)) ≫
      (xPrevIso Q ⋯).hom

Tactic:
simp [mkCoinductiveAux₂]

Premises used: Homotopy.mkCoinductiveAux₂