ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ d P 0 (ComplexShape.next (ComplexShape.down ℕ) 0) ≫ f (ComplexShape.next (ComplexShape.down ℕ) 0) 0 = 0
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ↑(dNext 0) f = 0
dsimp [dNext]
case a
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 (ComplexShape.next (ComplexShape.down ℕ) 0)
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ d P 0 (ComplexShape.next (ComplexShape.down ℕ) 0) ≫ f (ComplexShape.next (ComplexShape.down ℕ) 0) 0 = 0
rw [P.shape, zero_comp]
case a
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 0
case a
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 (ComplexShape.next (ComplexShape.down ℕ) 0)
rw [ChainComplex.next_nat_zero]
case a
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬0 + 1 = 0
case a
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 0
dsimp
no goals
case a
ι : Type ?u.313500
V : Type u
inst✝¹ : Category V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬0 + 1 = 0
decide