ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ f 0 (ComplexShape.prev (ComplexShape.up ℕ) 0) ≫ d Q (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 = 0
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ↑(prevD 0) f = 0
dsimp [prevD]
case a
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ f 0 (ComplexShape.prev (ComplexShape.up ℕ) 0) ≫ d Q (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 = 0
rw [Q.shape, comp_zero]
case a
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 0
case a
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0
rw [CochainComplex.prev_nat_zero]
case a
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬0 + 1 = 0
case a
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 0
dsimp
no goals
case a
ι : Type ?u.383391
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 : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬0 + 1 = 0
decide