[GOAL]
α : Type u
⊢ Inhabited (FreeRing α)
[PROOFSTEP]
dsimp only [FreeRing]
[GOAL]
α : Type u
⊢ Inhabited (FreeAbelianGroup (FreeMonoid α))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ C (FreeAbelianGroup.of (a :: m))
[PROOFSTEP]
convert hm _ _ (hb a) ih
[GOAL]
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = of a * FreeAbelianGroup.of m
[PROOFSTEP]
rw [of, ← FreeAbelianGroup.of_mul]
[GOAL]
case h.e'_1
α : Type u
C : FreeRing α → Prop
z : FreeRing α
hn1 : C (-1)
hb : ∀ (b : α), C (of b)
ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)
hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)
hn : ∀ (x : FreeRing α), C x → C (-x)
h1 : C 1
m✝ : FreeMonoid α
a : α
m : List α
ih : C (FreeAbelianGroup.of m)
⊢ FreeAbelianGroup.of (a :: m) = FreeAbelianGroup.of (FreeMonoid.of a * m)
[PROOFSTEP]
rfl


[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a b c : F ⟶ G), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ c✝ : F ⟶ G
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ c✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ + b✝ + c✝) x✝ = NatTrans.app (a✝ + (b✝ + c✝)) x✝
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a : F ⟶ G), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
⊢ 0 + a✝ = a✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (0 + a✝) x✝ = NatTrans.app a✝ x✝
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
⊢ a✝ + 0 = a✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ + 0) x✝ = NatTrans.app a✝ x✝
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a b : F ⟶ G), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ - b✝) x✝ = NatTrans.app (a✝ + -b✝) x✝
[PROOFSTEP]
apply sub_eq_add_neg
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a : F ⟶ G), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (-a✝ + a✝) x✝ = NatTrans.app 0 x✝
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
⊢ ∀ (a b : F ⟶ G), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
a✝ b✝ : F ⟶ G
x✝ : C
⊢ NatTrans.app (a✝ + b✝) x✝ = NatTrans.app (b✝ + a✝) x✝
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
⊢ ∀ (P Q R : C ⥤ D) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
x✝ : C
⊢ NatTrans.app ((f✝ + f'✝) ≫ g✝) x✝ = NatTrans.app (f✝ ≫ g✝ + f'✝ ≫ g✝) x✝
[PROOFSTEP]
apply add_comp
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
⊢ ∀ (P Q R : C ⥤ D) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.38, u_1} C
inst✝¹ : Category.{?u.42, u_2} D
inst✝ : Preadditive D
P✝ Q✝ R✝ : C ⥤ D
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
x✝ : C
⊢ NatTrans.app (f✝ ≫ (g✝ + g'✝)) x✝ = NatTrans.app (f✝ ≫ g✝ + f✝ ≫ g'✝) x✝
[PROOFSTEP]
apply comp_add
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_5, u_1} C
inst✝¹ : Category.{u_4, u_2} D
inst✝ : Preadditive D
F G : C ⥤ D
ι : Type u_3
s : Finset ι
X : C
α : ι → (F ⟶ G)
⊢ app (∑ i in s, α i) X = ∑ i in s, app (α i) X
[PROOFSTEP]
simp only [← appHom_apply, map_sum]


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ HomologicalComplex.Hom.f J.ι 0 ≫ descFZero f I J ≫ HomologicalComplex.d I.cocomplex 0 1 = 0
[PROOFSTEP]
simp [← Category.assoc, descFZero]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ HomologicalComplex.d J.cocomplex 0 1 ≫ descFOne f I J = descFZero f I J ≫ HomologicalComplex.d I.cocomplex 0 1
[PROOFSTEP]
simp [descFZero, descFOne]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
n : ℕ
g : HomologicalComplex.X J.cocomplex n ⟶ HomologicalComplex.X I.cocomplex n
g' : HomologicalComplex.X J.cocomplex (n + 1) ⟶ HomologicalComplex.X I.cocomplex (n + 1)
w : HomologicalComplex.d J.cocomplex n (n + 1) ≫ g' = g ≫ HomologicalComplex.d I.cocomplex n (n + 1)
⊢ HomologicalComplex.d J.cocomplex n (n + 1) ≫ g' ≫ HomologicalComplex.d I.cocomplex (n + 1) (n + 2) = 0
[PROOFSTEP]
simp [← Category.assoc, w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
n : ℕ
g : HomologicalComplex.X J.cocomplex n ⟶ HomologicalComplex.X I.cocomplex n
g' : HomologicalComplex.X J.cocomplex (n + 1) ⟶ HomologicalComplex.X I.cocomplex (n + 1)
w : HomologicalComplex.d J.cocomplex n (n + 1) ≫ g' = g ≫ HomologicalComplex.d I.cocomplex n (n + 1)
⊢ HomologicalComplex.d J.cocomplex (n + 1) (n + 2) ≫
      Exact.desc (g' ≫ HomologicalComplex.d I.cocomplex (n + 1) (n + 2)) (HomologicalComplex.d J.cocomplex n (n + 1))
        (HomologicalComplex.d J.cocomplex (n + 1) (n + 2))
        (_ :
          Exact (HomologicalComplex.d J.cocomplex (n + 1) (n + 2)).op (HomologicalComplex.d J.cocomplex n (n + 1)).op)
        (_ : HomologicalComplex.d J.cocomplex n (n + 1) ≫ g' ≫ HomologicalComplex.d I.cocomplex (n + 1) (n + 2) = 0) =
    g' ≫ HomologicalComplex.d I.cocomplex (n + 1) (n + 2)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ J.ι ≫ desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ HomologicalComplex.Hom.f (J.ι ≫ desc f I J) 0 = HomologicalComplex.Hom.f ((CochainComplex.single₀ C).map f ≫ I.ι) 0
[PROOFSTEP]
simp [desc, descFOne, descFZero]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ HomologicalComplex.d I.cocomplex 0 1 ≫
      (HomologicalComplex.Hom.f f 1 - descHomotopyZeroZero f comm ≫ HomologicalComplex.d J.cocomplex 0 1) =
    0
[PROOFSTEP]
simp [descHomotopyZeroZero, ← Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : HomologicalComplex.X I.cocomplex (n + 1) ⟶ HomologicalComplex.X J.cocomplex n
g' : HomologicalComplex.X I.cocomplex (n + 2) ⟶ HomologicalComplex.X J.cocomplex (n + 1)
w :
  HomologicalComplex.Hom.f f (n + 1) =
    HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' + g ≫ HomologicalComplex.d J.cocomplex n (n + 1)
⊢ HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫
      (HomologicalComplex.Hom.f f (n + 2) - g' ≫ HomologicalComplex.d J.cocomplex (n + 1) (n + 2)) =
    0
[PROOFSTEP]
simp [Preadditive.comp_sub, ← Category.assoc, Preadditive.sub_comp,
  show I.cocomplex.d (n + 1) (n + 2) ≫ g' = f.f (n + 1) - g ≫ J.cocomplex.d n (n + 1)
    by
    rw [w]
    simp only [add_sub_cancel]]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : HomologicalComplex.X I.cocomplex (n + 1) ⟶ HomologicalComplex.X J.cocomplex n
g' : HomologicalComplex.X I.cocomplex (n + 2) ⟶ HomologicalComplex.X J.cocomplex (n + 1)
w :
  HomologicalComplex.Hom.f f (n + 1) =
    HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' + g ≫ HomologicalComplex.d J.cocomplex n (n + 1)
⊢ HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' =
    HomologicalComplex.Hom.f f (n + 1) - g ≫ HomologicalComplex.d J.cocomplex n (n + 1)
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : HomologicalComplex.X I.cocomplex (n + 1) ⟶ HomologicalComplex.X J.cocomplex n
g' : HomologicalComplex.X I.cocomplex (n + 2) ⟶ HomologicalComplex.X J.cocomplex (n + 1)
w :
  HomologicalComplex.Hom.f f (n + 1) =
    HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' + g ≫ HomologicalComplex.d J.cocomplex n (n + 1)
⊢ HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' =
    HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' + g ≫ HomologicalComplex.d J.cocomplex n (n + 1) -
      g ≫ HomologicalComplex.d J.cocomplex n (n + 1)
[PROOFSTEP]
simp only [add_sub_cancel]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ HomologicalComplex.Hom.f f 0 = HomologicalComplex.d I.cocomplex 0 1 ≫ descHomotopyZeroZero f comm
[PROOFSTEP]
simp [descHomotopyZeroZero]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ HomologicalComplex.Hom.f f 1 =
    descHomotopyZeroZero f comm ≫ HomologicalComplex.d J.cocomplex 0 1 +
      HomologicalComplex.d I.cocomplex 1 2 ≫ descHomotopyZeroOne f comm
[PROOFSTEP]
simp [descHomotopyZeroOne]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x✝ :
  (f_1 : HomologicalComplex.X I.cocomplex (n + 1) ⟶ HomologicalComplex.X J.cocomplex n) ×'
    (f' : HomologicalComplex.X I.cocomplex (n + 2) ⟶ HomologicalComplex.X J.cocomplex (n + 1)) ×'
      HomologicalComplex.Hom.f f (n + 1) =
        f_1 ≫ HomologicalComplex.d J.cocomplex n (n + 1) + HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ f'
g : HomologicalComplex.X I.cocomplex (n + 1) ⟶ HomologicalComplex.X J.cocomplex n
g' : HomologicalComplex.X I.cocomplex (n + 2) ⟶ HomologicalComplex.X J.cocomplex (n + 1)
w :
  HomologicalComplex.Hom.f f (n + 1) =
    g ≫ HomologicalComplex.d J.cocomplex n (n + 1) + HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g'
⊢ HomologicalComplex.Hom.f f (n + 1) =
    HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' + g ≫ HomologicalComplex.d J.cocomplex n (n + 1)
[PROOFSTEP]
simp only [w, add_comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x✝ :
  (f_1 : HomologicalComplex.X I.cocomplex (n + 1) ⟶ HomologicalComplex.X J.cocomplex n) ×'
    (f' : HomologicalComplex.X I.cocomplex (n + 2) ⟶ HomologicalComplex.X J.cocomplex (n + 1)) ×'
      HomologicalComplex.Hom.f f (n + 1) =
        f_1 ≫ HomologicalComplex.d J.cocomplex n (n + 1) + HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ f'
g : HomologicalComplex.X I.cocomplex (n + 1) ⟶ HomologicalComplex.X J.cocomplex n
g' : HomologicalComplex.X I.cocomplex (n + 2) ⟶ HomologicalComplex.X J.cocomplex (n + 1)
w :
  HomologicalComplex.Hom.f f (n + 1) =
    g ≫ HomologicalComplex.d J.cocomplex n (n + 1) + HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g'
⊢ HomologicalComplex.Hom.f f (n + 2) =
    { fst := g, snd := { fst := g', snd := w } }.snd.fst ≫ HomologicalComplex.d J.cocomplex (n + 1) (n + 2) +
      HomologicalComplex.d I.cocomplex (n + 2) (n + 3) ≫
        descHomotopyZeroSucc f n g g'
          (_ :
            HomologicalComplex.Hom.f f (n + 1) =
              HomologicalComplex.d I.cocomplex (n + 1) (n + 2) ≫ g' + g ≫ HomologicalComplex.d J.cocomplex n (n + 1))
[PROOFSTEP]
simp [descHomotopyZeroSucc, w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
I : InjectiveResolution Y
J : InjectiveResolution Z
g h : I.cocomplex ⟶ J.cocomplex
g_comm : I.ι ≫ g = (CochainComplex.single₀ C).map f ≫ J.ι
h_comm : I.ι ≫ h = (CochainComplex.single₀ C).map f ≫ J.ι
⊢ I.ι ≫ (g - h) = 0
[PROOFSTEP]
simp [g_comm, h_comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)
[PROOFSTEP]
apply descHomotopy (𝟙 X)
[GOAL]
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ desc (𝟙 X) I I = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι
[PROOFSTEP]
simp
[GOAL]
case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I : InjectiveResolution X
⊢ I.ι ≫ 𝟙 I.cocomplex = (CochainComplex.single₀ C).map (𝟙 X) ≫ I.ι
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J)
[PROOFSTEP]
apply descHomotopy (f ≫ g)
[GOAL]
case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc (f ≫ g) K I = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι
[PROOFSTEP]
simp
[GOAL]
case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution X
J : InjectiveResolution Y
K : InjectiveResolution Z
⊢ I.ι ≫ desc f J I ≫ desc g K J = (CochainComplex.single₀ C).map (f ≫ g) ≫ K.ι
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) I I) (𝟙 I.cocomplex)
[PROOFSTEP]
simpa [Category.id_comp] using descIdHomotopy _ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) J J) (𝟙 J.cocomplex)
[PROOFSTEP]
simpa [Category.id_comp] using descIdHomotopy _ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ I.ι ≫ (homotopyEquiv I J).hom = J.ι
[PROOFSTEP]
simp [homotopyEquiv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
I J : InjectiveResolution X
⊢ J.ι ≫ (homotopyEquiv I J).inv = I.ι
[PROOFSTEP]
simp [homotopyEquiv]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X),
          map := fun {X Y} f => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X),
            map := fun {X Y} f =>
              (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f) }.obj
        X)
[PROOFSTEP]
rw [← (HomotopyCategory.quotient _ _).map_id]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X),
          map := fun {X Y} f => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f) }.map
      (𝟙 X) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (𝟙 (injectiveResolution X))
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ Homotopy (injectiveResolution.desc (𝟙 X)) (𝟙 (injectiveResolution X))
[PROOFSTEP]
apply InjectiveResolution.descIdHomotopy
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X),
          map := fun {X Y} f => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f) }.map
      (f ≫ g) =
    { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X),
            map := fun {X Y} f =>
              (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f) }.map
        f ≫
      { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X),
            map := fun {X Y} f =>
              (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f) }.map
        g
[PROOFSTEP]
rw [← (HomotopyCategory.quotient _ _).map_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X),
          map := fun {X Y} f => (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f) }.map
      (f ≫ g) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map (injectiveResolution.desc f ≫ injectiveResolution.desc g)
[PROOFSTEP]
apply HomotopyCategory.eq_of_homotopy
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Homotopy (injectiveResolution.desc (f ≫ g)) (injectiveResolution.desc f ≫ injectiveResolution.desc g)
[PROOFSTEP]
apply InjectiveResolution.descCompHomotopy
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ f ≫ d f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
⊢ (kernel.ι (d f) ≫ cokernel.π f) ≫ ι (cokernel f) = 0
[PROOFSTEP]
rw [Category.assoc, kernel.condition]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫ HomologicalComplex.d (ofCocomplex Z) 0 1 =
    HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) 0 1 ≫ 0
[PROOFSTEP]
simp only [ofCocomplex_d, eq_self_iff_true, eqToHom_refl, Category.comp_id, dite_eq_ite, if_true, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫
      (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
          (d (d (Injective.ι Z)))
          (_ :
            { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
                {
                      fst :=
                        syzygies
                          { fst := under Z,
                                snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := under Z,
                                    snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                          snd :=
                            (_ :
                              { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                  d
                                    { fst := under Z,
                                          snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                                0) } }.snd.fst =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
          0).d₀ =
    0
[PROOFSTEP]
exact (exact_f_d (Injective.ι Z)).w
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Exact (HomologicalComplex.d (ofCocomplex Z) 0 (0 + 1)) (HomologicalComplex.d (ofCocomplex Z) (0 + 1) (0 + 2))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Exact
    (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
        (d (d (Injective.ι Z)))
        (_ :
          { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
              {
                    fst :=
                      syzygies
                        { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := under Z,
                                  snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                        snd :=
                          (_ :
                            { fst := under Z,
                                      snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                d
                                  { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                              0) } }.snd.fst =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
        0).d₀
    (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
        (d (d (Injective.ι Z)))
        (_ :
          { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
              {
                    fst :=
                      syzygies
                        { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := under Z,
                                  snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                        snd :=
                          (_ :
                            { fst := under Z,
                                      snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                d
                                  { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                              0) } }.snd.fst =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
        (0 + 1)).d₀
[PROOFSTEP]
apply exact_f_d
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n m : ℕ
⊢ Exact (HomologicalComplex.d (ofCocomplex Z) (m + 1) (m + 1 + 1))
    (HomologicalComplex.d (ofCocomplex Z) (m + 1 + 1) (m + 1 + 2))
[PROOFSTEP]
simp only [ofCocomplex_X, ComplexShape.up_Rel, not_true, ofCocomplex_d, eqToHom_refl, Category.comp_id, dite_eq_ite,
  ite_true]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n m : ℕ
⊢ Exact
    (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
        (d (d (Injective.ι Z)))
        (_ :
          { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
              {
                    fst :=
                      syzygies
                        { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := under Z,
                                  snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                        snd :=
                          (_ :
                            { fst := under Z,
                                      snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                d
                                  { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                              0) } }.snd.fst =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
        (m + 1)).d₀
    (if m + 1 + 1 + 1 = m + 1 + 2 then
      (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
          (d (d (Injective.ι Z)))
          (_ :
            { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
                {
                      fst :=
                        syzygies
                          { fst := under Z,
                                snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := under Z,
                                    snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                          snd :=
                            (_ :
                              { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                  d
                                    { fst := under Z,
                                          snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                                0) } }.snd.fst =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
          (m + 1 + 1)).d₀
    else 0)
[PROOFSTEP]
erw [if_pos (c := m + 1 + 1 + 1 = m + 2 + 1) rfl]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n m : ℕ
⊢ Exact
    (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
        (d (d (Injective.ι Z)))
        (_ :
          { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
              {
                    fst :=
                      syzygies
                        { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := under Z,
                                  snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                        snd :=
                          (_ :
                            { fst := under Z,
                                      snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                d
                                  { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                              0) } }.snd.fst =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
        (m + 1)).d₀
    (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z))
        (d (d (Injective.ι Z)))
        (_ :
          { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.snd.snd ≫
              {
                    fst :=
                      syzygies
                        { fst := under Z, snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := under Z,
                                  snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd,
                        snd :=
                          (_ :
                            { fst := under Z,
                                      snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd ≫
                                d
                                  { fst := under Z,
                                        snd := { fst := syzygies (Injective.ι Z), snd := d (Injective.ι Z) } }.2.snd =
                              0) } }.snd.fst =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : t.snd.snd.snd.snd.fst ≫ d t.snd.snd.snd.snd.fst = 0) } })
        (m + 1 + 1)).d₀
[PROOFSTEP]
apply exact_f_d
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
x✝ :
  (f : HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) n ⟶ HomologicalComplex.X (ofCocomplex Z) n) ×'
    (f' :
      HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (n + 1) ⟶ HomologicalComplex.X (ofCocomplex Z) (n + 1)) ×'
      f ≫ HomologicalComplex.d (ofCocomplex Z) n (n + 1) =
        HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) n (n + 1) ≫ f'
⊢ (f'' :
    HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (n + 2) ⟶ HomologicalComplex.X (ofCocomplex Z) (n + 2)) ×'
    x✝.snd.fst ≫ HomologicalComplex.d (ofCocomplex Z) (n + 1) (n + 2) =
      HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) (n + 1) (n + 2) ≫ f''
[PROOFSTEP]
use 0
[GOAL]
case snd
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
x✝ :
  (f : HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) n ⟶ HomologicalComplex.X (ofCocomplex Z) n) ×'
    (f' :
      HomologicalComplex.X ((CochainComplex.single₀ C).obj Z) (n + 1) ⟶ HomologicalComplex.X (ofCocomplex Z) (n + 1)) ×'
      f ≫ HomologicalComplex.d (ofCocomplex Z) n (n + 1) =
        HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) n (n + 1) ≫ f'
⊢ x✝.snd.fst ≫ HomologicalComplex.d (ofCocomplex Z) (n + 1) (n + 2) =
    HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) (n + 1) (n + 2) ≫ 0
[PROOFSTEP]
apply HasZeroObject.from_zero_ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ ∀ (n : ℕ), Injective (HomologicalComplex.X (ofCocomplex Z) n)
[PROOFSTEP]
rintro (_ | _ | _ | n)
[GOAL]
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective (HomologicalComplex.X (ofCocomplex Z) Nat.zero)
[PROOFSTEP]
apply Injective.injective_under
[GOAL]
case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective (HomologicalComplex.X (ofCocomplex Z) (Nat.succ Nat.zero))
[PROOFSTEP]
apply Injective.injective_under
[GOAL]
case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective (HomologicalComplex.X (ofCocomplex Z) (Nat.succ (Nat.succ Nat.zero)))
[PROOFSTEP]
apply Injective.injective_under
[GOAL]
case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ Injective (HomologicalComplex.X (ofCocomplex Z) (Nat.succ (Nat.succ (Nat.succ n))))
[PROOFSTEP]
apply Injective.injective_under
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Exact
    (HomologicalComplex.Hom.f
      (CochainComplex.mkHom ((CochainComplex.single₀ C).obj Z) (ofCocomplex Z) (Injective.ι Z) 0
        (_ :
          Injective.ι Z ≫ HomologicalComplex.d (ofCocomplex Z) 0 1 =
            HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) 0 1 ≫ 0)
        fun n x =>
        { fst := 0,
          snd :=
            (_ :
              x.snd.fst ≫ HomologicalComplex.d (ofCocomplex Z) (n + 1) (n + 2) =
                HomologicalComplex.d ((CochainComplex.single₀ C).obj Z) (n + 1) (n + 2) ≫ 0) })
      0)
    (HomologicalComplex.d (ofCocomplex Z) 0 1)
[PROOFSTEP]
simpa using exact_f_d (Injective.ι Z)