case mp
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) → i = 0

case mpr
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0
constructor
case mp.intro
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
⊢ i = 0
case mp
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) → i = 0
rintro ⟨_, h₂⟩
case mp.intro
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
h : ¬i = 0
⊢ False
case mp.intro
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
⊢ i = 0
by_contra h
no goals
case mp.intro
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
left✝ : len [j + 1] = len [j] + 1
h₂ : ↑(Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
h : ¬i = 0
⊢ False
exact h₂ (Fin.succAbove_ne_zero_zero h)
case mpr
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)
case mpr
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)
rintro rfl
no goals
case mpr
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)
exact ⟨rfl, by dsimp ; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ ¬↑(Hom.toOrderHom (SimplexCategory.δ 0)) 0 = 0
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ ↑(Hom.toOrderHom (SimplexCategory.δ 0)) 0 ≠ 0
dsimp
no goals
C : Type ?u.1149
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
j : ℕ
⊢ ¬↑(Hom.toOrderHom (SimplexCategory.δ 0)) 0 = 0
exact Fin.succ_ne_zero (0 : Fin (j + 1))