-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
lemma ofCocomplex_exactAt_succ (n : ℕ) :
    (ofCocomplex Z).ExactAt (n + 1)

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

Tactic:
apply exact_f_d ((CochainComplex.mkAux _ _ _
(d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)

Result:
no goals

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

Tactic:
match n with
| 0 => apply exact_f_d ((CochainComplex.mkAux _ _ _
    (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)
| n+1 => apply exact_f_d ((CochainComplex.mkAux _ _ _
    (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n+1)).f)

Result:
no goals

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

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

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

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      ((CochainComplex.of
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).X₁)
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f)
            ⋯).d
        n (n + 1))
      ((CochainComplex.of
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).X₁)
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f)
            ⋯).d
        (n + 1) (n + 1 + 1))
      ⋯).Exact

Tactic:
simp only [CochainComplex.of_d]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
          (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f
      (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
          (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).f
      ⋯).Exact

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

Tactic:
apply exact_f_d ((CochainComplex.mkAux _ _ _
(d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n+1)).f)

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
dsimp [ofCocomplex, CochainComplex.mk', CochainComplex.mk, HomologicalComplex.sc',
    HomologicalComplex.shortComplexFunctor']

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ (ShortComplex.mk
      ((CochainComplex.of
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).X₁)
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f)
            ⋯).d
        n (n + 1))
      ((CochainComplex.of
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).X₁)
            (fun n =>
              (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z)))
                  (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f)
            ⋯).d
        (n + 1) (n + 1 + 1))
      ⋯).Exact

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

Tactic:
simp

Result:
no goals