ι : Type ?u.344609
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 : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q (_ : i + 1 = i + 1)).hom =
    (xNextIso P (_ : i + 1 = i + 1)).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst
ι : Type ?u.344609
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 : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i j : ℕ
h : i + 1 = j
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom =
    (xNextIso P h).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst
subst j
no goals
ι : Type ?u.344609
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 : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q (_ : i + 1 = i + 1)).hom =
    (xNextIso P (_ : i + 1 = i + 1)).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst
rcases i with (_ | _ | i) <;> simp [mkInductiveAux₂]