C : Type ?u.724
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : ComplexShape.Rel c 0 j
⊢ False
C : Type ?u.724
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
⊢ ¬ComplexShape.Rel c 0 j
intro hj
C : Type ?u.724
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : j + 1 = 0
⊢ False
C : Type ?u.724
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : ComplexShape.Rel c 0 j
⊢ False
dsimp at hj
C : Type ?u.724
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : j + 1 = 0
⊢ Nat.succ j ≤ 0
C : Type ?u.724
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : j + 1 = 0
⊢ False
apply Nat.not_succ_le_zero j
no goals
C : Type ?u.724
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : j + 1 = 0
⊢ Nat.succ j ≤ 0
rw [Nat.succ_eq_add_one, hj]