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