[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.Hom.f I.ι (n + 1) = 0
[PROOFSTEP]
apply zero_of_source_iso_zero
[GOAL]
case i
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (n + 1) ≅ 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ Mono (HomologicalComplex.Hom.f I.ι n)
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
⊢ Mono (HomologicalComplex.Hom.f I.ι Nat.zero)
[PROOFSTEP]
apply I.mono
[GOAL]
case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono (HomologicalComplex.Hom.f I.ι (Nat.succ n✝))
[PROOFSTEP]
rw [ι_f_succ]
[GOAL]
case succ
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasEqualizers C
inst✝ : HasImages C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono 0
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n : ℕ
⊢ Injective (HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) n)
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Injective (HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) Nat.zero)
[PROOFSTEP]
dsimp
[GOAL]
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Injective Z
[PROOFSTEP]
infer_instance
[GOAL]
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n✝ : ℕ
⊢ Injective (HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (Nat.succ n✝))
[PROOFSTEP]
dsimp
[GOAL]
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n✝ : ℕ
⊢ Injective 0
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Exact (HomologicalComplex.Hom.f (𝟙 ((CochainComplex.single₀ C).obj Z)) 0)
    (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) 0 1)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Exact (𝟙 Z) 0
[PROOFSTEP]
exact exact_epi_zero _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n : ℕ
⊢ Exact (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) n (n + 1))
    (HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) (n + 1) (n + 2))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
n : ℕ
⊢ Exact 0 0
[PROOFSTEP]
exact exact_of_zero _ _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Mono (HomologicalComplex.Hom.f (𝟙 ((CochainComplex.single₀ C).obj Z)) 0)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
Z : C
inst✝ : Injective Z
⊢ Mono (𝟙 Z)
[PROOFSTEP]
infer_instance
