case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
⊢ ∀ (A : IndexSet [n].op),
    ιSummand s A ≫ SimplicialObject.σ X i ≫ πSummand s (IndexSet.id [n + 1].op) = ιSummand s A ≫ 0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
⊢ SimplicialObject.σ X i ≫ πSummand s (IndexSet.id [n + 1].op) = 0
apply s.hom_ext'
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ιSummand s A ≫ SimplicialObject.σ X i ≫ πSummand s (IndexSet.id [n + 1].op) = ιSummand s A ≫ 0
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
⊢ ∀ (A : IndexSet [n].op),
    ιSummand s A ≫ SimplicialObject.σ X i ≫ πSummand s (IndexSet.id [n + 1].op) = ιSummand s A ≫ 0
intro A
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ιSummand s A ≫ X.map (SimplexCategory.σ i).op ≫ πSummand s (IndexSet.id [n + 1].op) = ιSummand s A ≫ 0
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ιSummand s A ≫ SimplicialObject.σ X i ≫ πSummand s (IndexSet.id [n + 1].op) = ιSummand s A ≫ 0
dsimp only [SimplicialObject.σ]
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ IndexSet.id [n + 1].op ≠ IndexSet.epiComp A (SimplexCategory.σ i).op
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ιSummand s A ≫ X.map (SimplexCategory.σ i).op ≫ πSummand s (IndexSet.id [n + 1].op) = ιSummand s A ≫ 0
rw [comp_zero, s.ιSummand_epi_naturality_assoc A (SimplexCategory.σ i).op, ι_πSummand_eq_zero]
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ IndexSet.epiComp A (SimplexCategory.σ i).op ≠ IndexSet.id [n + 1].op
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ IndexSet.id [n + 1].op ≠ IndexSet.epiComp A (SimplexCategory.σ i).op
rw [ne_comm]
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ¬IndexSet.EqId (IndexSet.epiComp A (SimplexCategory.σ i).op)
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ IndexSet.epiComp A (SimplexCategory.σ i).op ≠ IndexSet.id [n + 1].op
change ¬(A.epiComp (SimplexCategory.σ i).op).EqId
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ¬SimplexCategory.len (IndexSet.epiComp A (SimplexCategory.σ i).op).fst.unop = SimplexCategory.len [n + 1].op.unop
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ¬IndexSet.EqId (IndexSet.epiComp A (SimplexCategory.σ i).op)
rw [IndexSet.eqId_iff_len_eq]
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
h : SimplexCategory.len A.fst.unop ≤ SimplexCategory.len [n].op.unop
⊢ ¬SimplexCategory.len (IndexSet.epiComp A (SimplexCategory.σ i).op).fst.unop = SimplexCategory.len [n + 1].op.unop
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
⊢ ¬SimplexCategory.len (IndexSet.epiComp A (SimplexCategory.σ i).op).fst.unop = SimplexCategory.len [n + 1].op.unop
have h := SimplexCategory.len_le_of_epi (inferInstance : Epi A.e)
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
h : SimplexCategory.len A.fst.unop ≤ n
⊢ ¬SimplexCategory.len A.fst.unop = n + 1
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
h : SimplexCategory.len A.fst.unop ≤ SimplexCategory.len [n].op.unop
⊢ ¬SimplexCategory.len (IndexSet.epiComp A (SimplexCategory.σ i).op).fst.unop = SimplexCategory.len [n + 1].op.unop
dsimp at h ⊢
no goals
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet [n].op
h : SimplexCategory.len A.fst.unop ≤ n
⊢ ¬SimplexCategory.len A.fst.unop = n + 1
linarith