-- Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
theorem σ_comp_πSummand_id_eq_zero {n : ℕ} (i : Fin (n + 1)) :
    X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
⊢ ∀ (A : IndexSet (op ⦋n⦌)),
    (s.cofan (op ⦋n⦌)).inj A ≫ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = (s.cofan (op ⦋n⦌)).inj A ≫ 0

Tactic:
intro A

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = (s.cofan (op ⦋n⦌)).inj A ≫ 0

Proof state:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ A.epiComp (SimplexCategory.σ i).op ≠ IndexSet.id (op ⦋n + 1⦌)

Tactic:
change ¬(A.epiComp (SimplexCategory.σ i).op).EqId

Result:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(A.epiComp (SimplexCategory.σ i).op).EqId

Proof state:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop A.fst).len ≤ (unop (op ⦋n⦌)).len
⊢ ¬(unop (A.epiComp (SimplexCategory.σ i).op).fst).len = (unop (op ⦋n + 1⦌)).len

Tactic:
dsimp at h ⊢

Result:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop A.fst).len ≤ n
⊢ ¬(unop A.fst).len = n + 1

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) =
    (s.cofan (op ⦋n⦌)).inj A ≫ 0

Tactic:
rw [comp_zero, s.cofan_inj_epi_naturality_assoc A (SimplexCategory.σ i).op,
  cofan_inj_πSummand_eq_zero]

Result:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ IndexSet.id (op ⦋n + 1⦌) ≠ A.epiComp (SimplexCategory.σ i).op

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = (s.cofan (op ⦋n⦌)).inj A ≫ 0

Tactic:
dsimp only [SimplicialObject.σ]

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) =
    (s.cofan (op ⦋n⦌)).inj A ≫ 0

Proof state:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(A.epiComp (SimplexCategory.σ i).op).EqId

Tactic:
rw [IndexSet.eqId_iff_len_eq]

Result:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(unop (A.epiComp (SimplexCategory.σ i).op).fst).len = (unop (op ⦋n + 1⦌)).len

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = 0

Tactic:
apply s.hom_ext'

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
⊢ ∀ (A : IndexSet (op ⦋n⦌)),
    (s.cofan (op ⦋n⦌)).inj A ≫ X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌)) = (s.cofan (op ⦋n⦌)).inj A ≫ 0

Proof state:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop A.fst).len ≤ n
⊢ ¬(unop A.fst).len = n + 1

Tactic:
omega

Result:
no goals

Proof state:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ ¬(unop (A.epiComp (SimplexCategory.σ i).op).fst).len = (unop (op ⦋n + 1⦌)).len

Tactic:
have h := SimplexCategory.len_le_of_epi (inferInstance : Epi A.e)

Result:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop A.fst).len ≤ (unop (op ⦋n⦌)).len
⊢ ¬(unop (A.epiComp (SimplexCategory.σ i).op).fst).len = (unop (op ⦋n + 1⦌)).len

Proof state:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ IndexSet.id (op ⦋n + 1⦌) ≠ A.epiComp (SimplexCategory.σ i).op

Tactic:
rw [ne_comm]

Result:
case h.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
n : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ A.epiComp (SimplexCategory.σ i).op ≠ IndexSet.id (op ⦋n + 1⦌)