case h
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝ : Δ ⟶ Δ'
inst✝¹ : Mono i✝
n : ℕ
i : [n] ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len [n]) =
    HomologicalComplex.Hom.f PInfty (len Δ') ≫ X.map i.op
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len Δ) =
    HomologicalComplex.Hom.f PInfty (len Δ') ≫ X.map i.op
induction' Δ using SimplexCategory.rec with n
case h.h
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len [n]) =
    HomologicalComplex.Hom.f PInfty (len [n']) ≫ X.map i.op
case h
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝ : Δ ⟶ Δ'
inst✝¹ : Mono i✝
n : ℕ
i : [n] ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len [n]) =
    HomologicalComplex.Hom.f PInfty (len Δ') ≫ X.map i.op
induction' Δ' using SimplexCategory.rec with n'
case h.h
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
case h.h
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty (len [n]) =
    HomologicalComplex.Hom.f PInfty (len [n']) ≫ X.map i.op
dsimp
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op

case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
case h.h
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
by_cases n = n'
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op

case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
by_cases hi : Isδ₀ i
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : n = n'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
subst h
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ 𝟙 (HomologicalComplex.X K[X] (len [n])) ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (X.obj [n].op)
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n ≫ X.map i.op
simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ 𝟙 (X.obj [n].op) ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (X.obj [n].op)
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ 𝟙 (HomologicalComplex.X K[X] (len [n])) ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (X.obj [n].op)
dsimp
no goals
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n]
inst✝¹ : Mono i✝
i : [n] ⟶ [n]
inst✝ : Mono i
⊢ 𝟙 (X.obj [n].op) ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (X.obj [n].op)
simp only [id_comp, comp_id]
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : Isδ₀ i
h' : n' = n + 1
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
have h' : n' = n + 1 := hi.left
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : Isδ₀ i
h' : n' = n + 1
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
subst h'
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.d K[X] (len [n + 1]) (len [n]) ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.d K[X] (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.d K[X] (len [n + 1]) (len [n]) ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
dsimp
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ (HomologicalComplex.Hom.f PInfty (n + 1) ≫ Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X i) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.d K[X] (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ (Finset.sum Finset.univ fun j => HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑j • SimplicialObject.δ X j)) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ (HomologicalComplex.Hom.f PInfty (n + 1) ≫ Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X i) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
simp only [eq_self_iff_true, id_comp, if_true, Preadditive.comp_sum]
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op

case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ (b : Fin (n + 2)),
    b ∈ Finset.univ → b ≠ 0 → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0

case pos.h₁
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ¬0 ∈ Finset.univ → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) = 0
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ (Finset.sum Finset.univ fun j => HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑j • SimplicialObject.δ X j)) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
rw [Finset.sum_eq_single (0 : Fin (n + 2))]
case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ (b : Fin (n + 2)),
    b ∈ Finset.univ → b ≠ 0 → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0

case pos.h₁
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ¬0 ∈ Finset.univ → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) = 0

case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op

case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ (b : Fin (n + 2)),
    b ∈ Finset.univ → b ≠ 0 → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0

case pos.h₁
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ¬0 ∈ Finset.univ → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) = 0
rotate_left
case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0
case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ (b : Fin (n + 2)),
    b ∈ Finset.univ → b ≠ 0 → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0
intro b _ hb
case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ (-1) ^ ↑b • HomologicalComplex.Hom.f PInfty (n + 1) ≫ SimplicialObject.δ X b = 0
case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑b • SimplicialObject.δ X b) = 0
rw [Preadditive.comp_zsmul]
no goals
case pos.h₀
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ (-1) ^ ↑b • HomologicalComplex.Hom.f PInfty (n + 1) ≫ SimplicialObject.δ X b = 0
erw [PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
    (by
      rw [Isδ₀.iff]
      exact hb),
  zsmul_zero]
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬b = 0
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ b)
rw [Isδ₀.iff]
no goals
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬b = 0
exact hb
no goals
case pos.h₁
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ¬0 ∈ Finset.univ → HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) = 0
simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ SimplicialObject.δ X 0 =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map (SimplexCategory.δ 0).op
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ ((-1) ^ ↑0 • SimplicialObject.δ X 0) =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map i.op
simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]
no goals
case pos
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
i✝ : Δ ⟶ [n + 1]
inst✝¹ : Mono i✝
i : [n] ⟶ [n + 1]
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ SimplicialObject.δ X 0 =
    HomologicalComplex.Hom.f PInfty (n + 1) ≫ X.map (SimplexCategory.δ 0).op
rfl
case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op

C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ [n'] ≠ [n]
case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty n = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ [n'] ≠ [n]

case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op

C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ [n'] ≠ [n]
swap
case neg.h₁
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ len [n] ≠ n'

case neg.h₂
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i
case neg
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op
rw [PInfty_comp_map_mono_eq_zero]
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : [n'] = [n]
⊢ False
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ [n'] ≠ [n]
by_contra h'
no goals
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : [n'] = [n]
⊢ False
exact h (congr_arg SimplexCategory.len h'.symm)
no goals
case neg.h₁
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ len [n] ≠ n'
exact h
case neg.h₂
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : Isδ₀ i
⊢ False
case neg.h₂
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i
by_contra h'
no goals
case neg.h₂
C : Type u_2
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i✝² : Δ ⟶ Δ'
inst✝³ : Mono i✝²
n : ℕ
i✝¹ : [n] ⟶ Δ'
inst✝² : Mono i✝¹
n' : ℕ
i✝ : Δ ⟶ [n']
inst✝¹ : Mono i✝
i : [n] ⟶ [n']
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : Isδ₀ i
⊢ False
exact hi h'