ι : Type ?u.413991
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P (_ : i + 1 = i + 1)).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst ≫ (xPrevIso Q (_ : i + 1 = i + 1)).hom
ι : Type ?u.413991
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (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.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst ≫ (xPrevIso Q h).hom
subst j
no goals
ι : Type ?u.413991
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P (_ : i + 1 = i + 1)).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst ≫ (xPrevIso Q (_ : i + 1 = i + 1)).hom
rcases i with (_ | _ | i) <;> simp [mkCoinductiveAux₂]