no goals
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.next (ComplexShape.down ℕ) 0 = 0
classical
  refine' dif_neg _
  push_neg
  intro
  apply Nat.noConfusion
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
⊢ ¬∃ j, ComplexShape.Rel (ComplexShape.down ℕ) 0 j
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.next (ComplexShape.down ℕ) 0 = 0
refine' dif_neg _
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
⊢ ∀ (j : ℕ), ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
⊢ ¬∃ j, ComplexShape.Rel (ComplexShape.down ℕ) 0 j
push_neg
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
j✝ : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j✝
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
⊢ ∀ (j : ℕ), ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j
intro
no goals
ι : Type ?u.6212
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
j✝ : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j✝
apply Nat.noConfusion