-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
lemma ofComplex_exactAt_succ (n : ℕ) :
    (ofComplex Z).ExactAt (n + 1)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ComplexShape.down ℕ).prev (n + 1) = n + 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ n : ℕ
⊢ (ShortComplex.mk
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1 + 1)).g
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).g
      ⋯).Exact

Tactic:
apply exact_d_f

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (0 + 1)).g
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) 0).g
      ⋯).Exact

Tactic:
apply exact_d_f

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).g
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g
      ⋯).Exact

Tactic:
match n with
| 0 => apply exact_d_f
| n + 1 => apply exact_d_f

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt (ofComplex Z) (n + 1)

Tactic:
rw [HomologicalComplex.exactAt_iff' _ (n + 1 + 1) (n + 1) n (by simp) (by simp)]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (HomologicalComplex.sc' (ofComplex Z) (n + 1 + 1) (n + 1) n).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      ((ChainComplex.of
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).X₃)
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g)
            ⋯).d
        (n + 1 + 1) (n + 1))
      ((ChainComplex.of
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).X₃)
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g)
            ⋯).d
        (n + 1) n)
      ⋯).Exact

Tactic:
simp only [ChainComplex.of_d]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) (n + 1)).g
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g
      ⋯).Exact

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (HomologicalComplex.sc' (ofComplex Z) (n + 1 + 1) (n + 1) n).Exact

Tactic:
dsimp [ofComplex, HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor',
    ChainComplex.mk', ChainComplex.mk]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      ((ChainComplex.of
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).X₃)
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g)
            ⋯).d
        (n + 1 + 1) (n + 1))
      ((ChainComplex.of
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).X₃)
            (fun n =>
              (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z)))
                  (d (Projective.π Z)) (d (d (Projective.π Z))) ⋯ (fun S => ⟨syzygies S.f, ⟨d S.f, ⋯⟩⟩) n).g)
            ⋯).d
        (n + 1) n)
      ⋯).Exact