ι : Type ?u.203118
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
n : ℕ
⊢ (succ (n + 0) (mkHomAux P Q zero one one_zero_comm succ (n + 0))).fst =
    (succ n
        { fst := (mkHomAux P Q zero one one_zero_comm succ n).fst,
          snd :=
            { fst := (mkHomAux P Q zero one one_zero_comm succ (n + 0)).snd.fst,
              snd :=
                (_ :
                  HomologicalComplex.Hom.f
                        (HomologicalComplex.Hom.mk fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) (n + 1) ≫
                      HomologicalComplex.d Q (n + 1) n =
                    HomologicalComplex.d P (n + 1) n ≫
                      HomologicalComplex.Hom.f
                        (HomologicalComplex.Hom.mk fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst)
                        n) } }).fst
ι : Type ?u.203118
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
n : ℕ
⊢ HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 2) =
    (succ n
        { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n,
          snd :=
            { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1),
              snd :=
                (_ :
                  HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1) ≫
                      HomologicalComplex.d Q (n + 1) n =
                    HomologicalComplex.d P (n + 1) n ≫
                      HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n) } }).fst
dsimp [mkHom, mkHomAux]
no goals
ι : Type ?u.203118
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
n : ℕ
⊢ (succ (n + 0) (mkHomAux P Q zero one one_zero_comm succ (n + 0))).fst =
    (succ n
        { fst := (mkHomAux P Q zero one one_zero_comm succ n).fst,
          snd :=
            { fst := (mkHomAux P Q zero one one_zero_comm succ (n + 0)).snd.fst,
              snd :=
                (_ :
                  HomologicalComplex.Hom.f
                        (HomologicalComplex.Hom.mk fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) (n + 1) ≫
                      HomologicalComplex.d Q (n + 1) n =
                    HomologicalComplex.d P (n + 1) n ≫
                      HomologicalComplex.Hom.f
                        (HomologicalComplex.Hom.mk fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst)
                        n) } }).fst
induction n <;> congr