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