[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
⊢ F.map ed.s' ≫ NatTrans.app (((whiskering C D).obj F).obj X).hom (op [0]) =
    𝟙 (point.obj (((whiskering C D).obj F).obj X))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
⊢ F.map ed.s' ≫ F.map (NatTrans.app X.hom (op [0])) ≫ 𝟙 (F.obj X.right) = 𝟙 (F.obj X.right)
[PROOFSTEP]
erw [comp_id, ← F.map_comp, ed.s'_comp_ε, F.map_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
⊢ (fun n => F.map (s ed n)) 0 ≫ SimplicialObject.δ (((whiskering C D).obj F).obj X).left 1 =
    NatTrans.app (((whiskering C D).obj F).obj X).hom (op [0]) ≫ F.map ed.s'
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
⊢ F.map (s ed 0) ≫ SimplicialObject.δ (((SimplicialObject.whiskering C D).obj F).obj X.left) 1 =
    (F.map (NatTrans.app X.hom (op [0])) ≫ 𝟙 (F.obj X.right)) ≫ F.map ed.s'
[PROOFSTEP]
erw [comp_id, ← F.map_comp, ← F.map_comp, ed.s₀_comp_δ₁]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
⊢ (fun n => F.map (s ed n)) n ≫ SimplicialObject.δ (((whiskering C D).obj F).obj X).left 0 =
    𝟙 ((drop.obj (((whiskering C D).obj F).obj X)).obj (op [n]))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
⊢ F.map (s ed n) ≫ SimplicialObject.δ (((SimplicialObject.whiskering C D).obj F).obj X.left) 0 =
    𝟙 (F.obj (X.left.obj (op [n])))
[PROOFSTEP]
erw [← F.map_comp, ed.s_comp_δ₀, F.map_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
i : Fin (n + 2)
⊢ (fun n => F.map (s ed n)) (n + 1) ≫ SimplicialObject.δ (((whiskering C D).obj F).obj X).left (Fin.succ i) =
    SimplicialObject.δ (((whiskering C D).obj F).obj X).left i ≫ (fun n => F.map (s ed n)) n
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
i : Fin (n + 2)
⊢ F.map (s ed (n + 1)) ≫ SimplicialObject.δ (((SimplicialObject.whiskering C D).obj F).obj X.left) (Fin.succ i) =
    SimplicialObject.δ (((SimplicialObject.whiskering C D).obj F).obj X.left) i ≫ F.map (s ed n)
[PROOFSTEP]
erw [← F.map_comp, ← F.map_comp, ed.s_comp_δ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
i : Fin (n + 2)
⊢ F.map (SimplicialObject.δ X.left i ≫ s ed n) = F.map (X.left.map (SimplexCategory.δ i).op ≫ s ed n)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
i : Fin (n + 1)
⊢ (fun n => F.map (s ed n)) n ≫ SimplicialObject.σ (((whiskering C D).obj F).obj X).left (Fin.succ i) =
    SimplicialObject.σ (((whiskering C D).obj F).obj X).left i ≫ (fun n => F.map (s ed n)) (n + 1)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
i : Fin (n + 1)
⊢ F.map (s ed n) ≫ SimplicialObject.σ (((SimplicialObject.whiskering C D).obj F).obj X.left) (Fin.succ i) =
    SimplicialObject.σ (((SimplicialObject.whiskering C D).obj F).obj X.left) i ≫ F.map (s ed (n + 1))
[PROOFSTEP]
erw [← F.map_comp, ← F.map_comp, ed.s_comp_σ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.93209, u_1} C
D : Type u_2
inst✝ : Category.{?u.93216, u_2} D
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
F : C ⥤ D
n : ℕ
i : Fin (n + 1)
⊢ F.map (SimplicialObject.σ X.left i ≫ s ed (n + 1)) = F.map (X.left.map (SimplexCategory.σ i).op ≫ s ed (n + 1))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
⊢ ((point.mapIso e).inv ≫ ed.s' ≫ NatTrans.app (drop.mapIso e).hom (op [0])) ≫ NatTrans.app Y.hom (op [0]) =
    𝟙 (point.obj Y)
[PROOFSTEP]
simpa only [Functor.mapIso, assoc, w₀, ed.s'_comp_ε_assoc] using (point.mapIso e).inv_hom_id
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) 0 ≫
      SimplicialObject.δ Y.left 1 =
    NatTrans.app Y.hom (op [0]) ≫ (point.mapIso e).inv ≫ ed.s' ≫ NatTrans.app (drop.mapIso e).hom (op [0])
[PROOFSTEP]
have h := w₀ e.inv
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
h : NatTrans.app (drop.map e.inv) (op [0]) ≫ NatTrans.app X.hom (op [0]) = NatTrans.app Y.hom (op [0]) ≫ point.map e.inv
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) 0 ≫
      SimplicialObject.δ Y.left 1 =
    NatTrans.app Y.hom (op [0]) ≫ (point.mapIso e).inv ≫ ed.s' ≫ NatTrans.app (drop.mapIso e).hom (op [0])
[PROOFSTEP]
dsimp at h ⊢
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
h : NatTrans.app e.inv.left (op [0]) ≫ NatTrans.app X.hom (op [0]) = NatTrans.app Y.hom (op [0]) ≫ e.inv.right
⊢ (NatTrans.app e.inv.left (op [0]) ≫ s ed 0 ≫ NatTrans.app e.hom.left (op [0 + 1])) ≫ SimplicialObject.δ Y.left 1 =
    NatTrans.app Y.hom (op [0]) ≫ e.inv.right ≫ ed.s' ≫ NatTrans.app e.hom.left (op [0])
[PROOFSTEP]
simp only [assoc, ← SimplicialObject.δ_naturality, ed.s₀_comp_δ₁_assoc, reassoc_of% h]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) n ≫
      SimplicialObject.δ Y.left 0 =
    𝟙 ((drop.obj Y).obj (op [n]))
[PROOFSTEP]
have h := ed.s_comp_δ₀
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
h : ∀ (n : ℕ), s ed n ≫ SimplicialObject.δ X.left 0 = 𝟙 ((drop.obj X).obj (op [n]))
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) n ≫
      SimplicialObject.δ Y.left 0 =
    𝟙 ((drop.obj Y).obj (op [n]))
[PROOFSTEP]
dsimp at h ⊢
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
h : ∀ (n : ℕ), s ed n ≫ SimplicialObject.δ X.left 0 = 𝟙 (X.left.obj (op [n]))
⊢ (NatTrans.app e.inv.left (op [n]) ≫ s ed n ≫ NatTrans.app e.hom.left (op [n + 1])) ≫ SimplicialObject.δ Y.left 0 =
    𝟙 (Y.left.obj (op [n]))
[PROOFSTEP]
simpa only [assoc, ← SimplicialObject.δ_naturality, reassoc_of% h] using congr_app (drop.mapIso e).inv_hom_id (op [n])
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
i : Fin (n + 2)
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1]))
        (n + 1) ≫
      SimplicialObject.δ Y.left (Fin.succ i) =
    SimplicialObject.δ Y.left i ≫
      (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) n
[PROOFSTEP]
have h := ed.s_comp_δ n i
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
i : Fin (n + 2)
h : s ed (n + 1) ≫ SimplicialObject.δ X.left (Fin.succ i) = SimplicialObject.δ X.left i ≫ s ed n
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1]))
        (n + 1) ≫
      SimplicialObject.δ Y.left (Fin.succ i) =
    SimplicialObject.δ Y.left i ≫
      (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) n
[PROOFSTEP]
dsimp at h ⊢
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
i : Fin (n + 2)
h : s ed (n + 1) ≫ SimplicialObject.δ X.left (Fin.succ i) = SimplicialObject.δ X.left i ≫ s ed n
⊢ (NatTrans.app e.inv.left (op [n + 1]) ≫ s ed (n + 1) ≫ NatTrans.app e.hom.left (op [n + 1 + 1])) ≫
      SimplicialObject.δ Y.left (Fin.succ i) =
    SimplicialObject.δ Y.left i ≫ NatTrans.app e.inv.left (op [n]) ≫ s ed n ≫ NatTrans.app e.hom.left (op [n + 1])
[PROOFSTEP]
simp only [assoc, ← SimplicialObject.δ_naturality, reassoc_of% h, ← SimplicialObject.δ_naturality_assoc]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
i : Fin (n + 1)
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) n ≫
      SimplicialObject.σ Y.left (Fin.succ i) =
    SimplicialObject.σ Y.left i ≫
      (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1]))
        (n + 1)
[PROOFSTEP]
have h := ed.s_comp_σ n i
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
i : Fin (n + 1)
h : s ed n ≫ SimplicialObject.σ X.left (Fin.succ i) = SimplicialObject.σ X.left i ≫ s ed (n + 1)
⊢ (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1])) n ≫
      SimplicialObject.σ Y.left (Fin.succ i) =
    SimplicialObject.σ Y.left i ≫
      (fun n => NatTrans.app (drop.mapIso e).inv (op [n]) ≫ s ed n ≫ NatTrans.app (drop.mapIso e).hom (op [n + 1]))
        (n + 1)
[PROOFSTEP]
dsimp at h ⊢
[GOAL]
C : Type u_1
inst✝ : Category.{?u.102374, u_1} C
X Y : SimplicialObject.Augmented C
e : X ≅ Y
ed : ExtraDegeneracy X
n : ℕ
i : Fin (n + 1)
h : s ed n ≫ SimplicialObject.σ X.left (Fin.succ i) = SimplicialObject.σ X.left i ≫ s ed (n + 1)
⊢ (NatTrans.app e.inv.left (op [n]) ≫ s ed n ≫ NatTrans.app e.hom.left (op [n + 1])) ≫
      SimplicialObject.σ Y.left (Fin.succ i) =
    SimplicialObject.σ Y.left i ≫
      NatTrans.app e.inv.left (op [n + 1]) ≫ s ed (n + 1) ≫ NatTrans.app e.hom.left (op [n + 1 + 1])
[PROOFSTEP]
simp only [assoc, ← SimplicialObject.σ_naturality, reassoc_of% h, ← SimplicialObject.σ_naturality_assoc]
[GOAL]
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ shiftFun f (Fin.succ i) = f i
[PROOFSTEP]
dsimp [shiftFun]
[GOAL]
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
⊢ (if x : Fin.succ i = 0 then 0 else f (Fin.pred (Fin.succ i) x)) = f i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : Fin.succ i = 0
⊢ 0 = f i
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : Fin.succ i = 0
⊢ False
[PROOFSTEP]
simp only [Fin.ext_iff, Fin.val_succ, Fin.val_zero, add_eq_zero, and_false] at h
[GOAL]
case neg
n : ℕ
X : Type u_1
inst✝ : Zero X
f : Fin n → X
i : Fin n
h : ¬Fin.succ i = 0
⊢ f (Fin.pred (Fin.succ i) h) = f i
[PROOFSTEP]
simp only [Fin.pred_succ]
[GOAL]
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₂
[PROOFSTEP]
by_cases h₁ : i₁ = 0
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
h₁ : i₁ = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₂
[PROOFSTEP]
subst h₁
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : 0 ≤ i₂
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) 0 ≤ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₂
[PROOFSTEP]
simp only [shiftFun_0, Fin.zero_le]
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₂
[PROOFSTEP]
have h₂ : i₂ ≠ 0 := by
  intro h₂
  subst h₂
  exact h₁ (le_antisymm hi (Fin.zero_le _))
[GOAL]
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ i₂ ≠ 0
[PROOFSTEP]
intro h₂
[GOAL]
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ = 0
⊢ False
[PROOFSTEP]
subst h₂
[GOAL]
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ : Fin (SimplexCategory.len [n + 1] + 1)
h₁ : ¬i₁ = 0
hi : i₁ ≤ 0
⊢ False
[PROOFSTEP]
exact h₁ (le_antisymm hi (Fin.zero_le _))
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₂
[PROOFSTEP]
cases' Fin.eq_succ_of_ne_zero h₁ with j₁ hj₁
[GOAL]
case neg.intro
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
j₁ : Fin (SimplexCategory.len [n + 1])
hj₁ : i₁ = Fin.succ j₁
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₂
[PROOFSTEP]
cases' Fin.eq_succ_of_ne_zero h₂ with j₂ hj₂
[GOAL]
case neg.intro.intro
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
i₁ i₂ : Fin (SimplexCategory.len [n + 1] + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
h₂ : i₂ ≠ 0
j₁ : Fin (SimplexCategory.len [n + 1])
hj₁ : i₁ = Fin.succ j₁
j₂ : Fin (SimplexCategory.len [n + 1])
hj₂ : i₂ = Fin.succ j₂
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) i₂
[PROOFSTEP]
substs hj₁ hj₂
[GOAL]
case neg.intro.intro
n : ℕ
Δ : SimplexCategory
f : [n] ⟶ Δ
j₁ j₂ : Fin (SimplexCategory.len [n + 1])
h₁ : ¬Fin.succ j₁ = 0
h₂ : Fin.succ j₂ ≠ 0
hi : Fin.succ j₁ ≤ Fin.succ j₂
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) (Fin.succ j₁) ≤
    shiftFun (↑(SimplexCategory.Hom.toOrderHom f)) (Fin.succ j₂)
[PROOFSTEP]
simpa only [shiftFun_succ] using f.toOrderHom.monotone (Fin.succ_le_succ_iff.mp hi)
[GOAL]
Δ : SimplexCategory
⊢ (fun x => SimplexCategory.Hom.mk (↑(OrderHom.const (Fin (SimplexCategory.len (op [0]).unop + 1))) 0)) ≫
      NatTrans.app (standardSimplex.obj Δ).hom (op [0]) =
    𝟙 (point.obj (standardSimplex.obj Δ))
[PROOFSTEP]
dsimp
[GOAL]
Δ : SimplexCategory
⊢ (fun x => SimplexCategory.Hom.mk (↑(OrderHom.const (Fin (0 + 1))) 0)) ≫
      NatTrans.app (standardSimplex.obj Δ).hom (op [0]) =
    𝟙 (⊤_ Type)
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
Δ : SimplexCategory
⊢ (fun n f => shift f) 0 ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 1 =
    NatTrans.app (standardSimplex.obj Δ).hom (op [0]) ≫ fun x =>
      SimplexCategory.Hom.mk (↑(OrderHom.const (Fin (SimplexCategory.len (op [0]).unop + 1))) 0)
[PROOFSTEP]
ext1 x
[GOAL]
case h
Δ : SimplexCategory
x : (drop.obj (standardSimplex.obj Δ)).obj (op [0])
⊢ ((fun n f => shift f) 0 ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 1) x =
    (NatTrans.app (standardSimplex.obj Δ).hom (op [0]) ≫ fun x =>
        SimplexCategory.Hom.mk (↑(OrderHom.const (Fin (SimplexCategory.len (op [0]).unop + 1))) 0))
      x
[PROOFSTEP]
apply SimplexCategory.Hom.ext
[GOAL]
case h.a
Δ : SimplexCategory
x : (drop.obj (standardSimplex.obj Δ)).obj (op [0])
⊢ SimplexCategory.Hom.toOrderHom (((fun n f => shift f) 0 ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 1) x) =
    SimplexCategory.Hom.toOrderHom
      ((NatTrans.app (standardSimplex.obj Δ).hom (op [0]) ≫ fun x =>
          SimplexCategory.Hom.mk (↑(OrderHom.const (Fin (SimplexCategory.len (op [0]).unop + 1))) 0))
        x)
[PROOFSTEP]
ext j
[GOAL]
case h.a.h.h.h
Δ : SimplexCategory
x : (drop.obj (standardSimplex.obj Δ)).obj (op [0])
j : Fin (SimplexCategory.len (op [0]).unop + 1)
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (((fun n f => shift f) 0 ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 1) x))
        j) =
    ↑(↑(SimplexCategory.Hom.toOrderHom
            ((NatTrans.app (standardSimplex.obj Δ).hom (op [0]) ≫ fun x =>
                SimplexCategory.Hom.mk (↑(OrderHom.const (Fin (SimplexCategory.len (op [0]).unop + 1))) 0))
              x))
        j)
[PROOFSTEP]
fin_cases j
[GOAL]
case h.a.h.h.h.head
Δ : SimplexCategory
x : (drop.obj (standardSimplex.obj Δ)).obj (op [0])
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (((fun n f => shift f) 0 ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 1) x))
        { val := 0, isLt := (_ : 0 < SimplexCategory.len (op [0]).unop + 1) }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom
            ((NatTrans.app (standardSimplex.obj Δ).hom (op [0]) ≫ fun x =>
                SimplexCategory.Hom.mk (↑(OrderHom.const (Fin (SimplexCategory.len (op [0]).unop + 1))) 0))
              x))
        { val := 0, isLt := (_ : 0 < SimplexCategory.len (op [0]).unop + 1) })
[PROOFSTEP]
rfl
[GOAL]
Δ : SimplexCategory
n : ℕ
⊢ (fun n f => shift f) n ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 0 =
    𝟙 ((drop.obj (standardSimplex.obj Δ)).obj (op [n]))
[PROOFSTEP]
ext1 φ
[GOAL]
case h
Δ : SimplexCategory
n : ℕ
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
⊢ ((fun n f => shift f) n ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 0) φ =
    𝟙 ((drop.obj (standardSimplex.obj Δ)).obj (op [n])) φ
[PROOFSTEP]
apply SimplexCategory.Hom.ext
[GOAL]
case h.a
Δ : SimplexCategory
n : ℕ
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
⊢ SimplexCategory.Hom.toOrderHom (((fun n f => shift f) n ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 0) φ) =
    SimplexCategory.Hom.toOrderHom (𝟙 ((drop.obj (standardSimplex.obj Δ)).obj (op [n])) φ)
[PROOFSTEP]
ext i : 2
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
i : Fin (SimplexCategory.len (op [n]).unop + 1)
⊢ ↑(SimplexCategory.Hom.toOrderHom (((fun n f => shift f) n ≫ SimplicialObject.δ (standardSimplex.obj Δ).left 0) φ)) i =
    ↑(SimplexCategory.Hom.toOrderHom (𝟙 ((drop.obj (standardSimplex.obj Δ)).obj (op [n])) φ)) i
[PROOFSTEP]
dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.standardSimplex]
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
i : Fin (SimplexCategory.len (op [n]).unop + 1)
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.succ i) = ↑(SimplexCategory.Hom.toOrderHom φ) i
[PROOFSTEP]
simp only [shiftFun_succ]
[GOAL]
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
⊢ (fun n f => shift f) (n + 1) ≫ SimplicialObject.δ (standardSimplex.obj Δ).left (Fin.succ i) =
    SimplicialObject.δ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) n
[PROOFSTEP]
ext1 φ
[GOAL]
case h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
⊢ ((fun n f => shift f) (n + 1) ≫ SimplicialObject.δ (standardSimplex.obj Δ).left (Fin.succ i)) φ =
    (SimplicialObject.δ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) n) φ
[PROOFSTEP]
apply SimplexCategory.Hom.ext
[GOAL]
case h.a
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
⊢ SimplexCategory.Hom.toOrderHom
      (((fun n f => shift f) (n + 1) ≫ SimplicialObject.δ (standardSimplex.obj Δ).left (Fin.succ i)) φ) =
    SimplexCategory.Hom.toOrderHom ((SimplicialObject.δ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) n) φ)
[PROOFSTEP]
ext j : 2
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
⊢ ↑(SimplexCategory.Hom.toOrderHom
          (((fun n f => shift f) (n + 1) ≫ SimplicialObject.δ (standardSimplex.obj Δ).left (Fin.succ i)) φ))
      j =
    ↑(SimplexCategory.Hom.toOrderHom ((SimplicialObject.δ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) n) φ)) j
[PROOFSTEP]
dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.standardSimplex]
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.succAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ ↑(Fin.succAboveEmb i)) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.succAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ ↑(Fin.succAboveEmb i)) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case pos
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
h : j = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.succAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ ↑(Fin.succAboveEmb i)) j
[PROOFSTEP]
subst h
[GOAL]
case pos
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.succAbove (Fin.succ i) 0) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ ↑(Fin.succAboveEmb i)) 0
[PROOFSTEP]
simp only [Fin.succ_succAbove_zero, shiftFun_0]
[GOAL]
case neg
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
h : ¬j = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.succAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ ↑(Fin.succAboveEmb i)) j
[PROOFSTEP]
obtain ⟨_, rfl⟩ := Fin.eq_succ_of_ne_zero <| h
[GOAL]
case neg.intro
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n + 1])
w✝ : Fin (SimplexCategory.len (op [n + 1]).unop)
h : ¬Fin.succ w✝ = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.succAbove (Fin.succ i) (Fin.succ w✝)) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ ↑(Fin.succAboveEmb i)) (Fin.succ w✝)
[PROOFSTEP]
simp only [Fin.succ_succAbove_succ, shiftFun_succ, Function.comp_apply, Fin.succAboveEmb_apply]
[GOAL]
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
⊢ (fun n f => shift f) n ≫ SimplicialObject.σ (standardSimplex.obj Δ).left (Fin.succ i) =
    SimplicialObject.σ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) (n + 1)
[PROOFSTEP]
ext1 φ
[GOAL]
case h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
⊢ ((fun n f => shift f) n ≫ SimplicialObject.σ (standardSimplex.obj Δ).left (Fin.succ i)) φ =
    (SimplicialObject.σ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) (n + 1)) φ
[PROOFSTEP]
apply SimplexCategory.Hom.ext
[GOAL]
case h.a
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
⊢ SimplexCategory.Hom.toOrderHom
      (((fun n f => shift f) n ≫ SimplicialObject.σ (standardSimplex.obj Δ).left (Fin.succ i)) φ) =
    SimplexCategory.Hom.toOrderHom
      ((SimplicialObject.σ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) (n + 1)) φ)
[PROOFSTEP]
ext j : 2
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)
⊢ ↑(SimplexCategory.Hom.toOrderHom
          (((fun n f => shift f) n ≫ SimplicialObject.σ (standardSimplex.obj Δ).left (Fin.succ i)) φ))
      j =
    ↑(SimplexCategory.Hom.toOrderHom
          ((SimplicialObject.σ (standardSimplex.obj Δ).left i ≫ (fun n f => shift f) (n + 1)) φ))
      j
[PROOFSTEP]
dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.standardSimplex]
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.predAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ Fin.predAbove i) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case h.a.h.h
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.predAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ Fin.predAbove i) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case pos
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)
h : j = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.predAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ Fin.predAbove i) j
[PROOFSTEP]
subst h
[GOAL]
case pos
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.predAbove (Fin.succ i) 0) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ Fin.predAbove i) 0
[PROOFSTEP]
simp only [shiftFun_0]
[GOAL]
case pos
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.predAbove (Fin.succ i) 0) = 0
[PROOFSTEP]
exact shiftFun_0 φ.toOrderHom
[GOAL]
case neg
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)
h : ¬j = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.predAbove (Fin.succ i) j) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ Fin.predAbove i) j
[PROOFSTEP]
obtain ⟨_, rfl⟩ := Fin.eq_succ_of_ne_zero h
[GOAL]
case neg.intro
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (drop.obj (standardSimplex.obj Δ)).obj (op [n])
w✝ : Fin (SimplexCategory.len (op [n + 1 + 1]).unop)
h : ¬Fin.succ w✝ = 0
⊢ shiftFun (↑(SimplexCategory.Hom.toOrderHom φ)) (Fin.predAbove (Fin.succ i) (Fin.succ w✝)) =
    shiftFun (↑(SimplexCategory.Hom.toOrderHom φ) ∘ Fin.predAbove i) (Fin.succ w✝)
[PROOFSTEP]
simp only [Fin.succ_predAbove_succ, shiftFun_succ, Function.comp_apply]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.220931, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
⊢ (fun i =>
          if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
          else WidePullback.π (fun x => f.hom) (Fin.pred i x))
        i ≫
      f.hom =
    WidePullback.base fun x => f.hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.220931, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
⊢ (if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
      else WidePullback.π (fun x => f.hom) (Fin.pred i x)) ≫
      f.hom =
    WidePullback.base fun x => f.hom
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.220931, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
h : i = 0
⊢ ((WidePullback.base fun x => f.hom) ≫ S.section_) ≫ f.hom = WidePullback.base fun x => f.hom
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.220931, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ ((WidePullback.base fun x => f.hom) ≫ S.section_) ≫ f.hom = WidePullback.base fun x => f.hom
[PROOFSTEP]
simp only [assoc, SplitEpi.id, comp_id]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{?u.220931, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (SimplexCategory.len (op [n + 1]).unop + 1)
h : ¬i = 0
⊢ WidePullback.π (fun x => f.hom) (Fin.pred i h) ≫ f.hom = WidePullback.base fun x => f.hom
[PROOFSTEP]
simp only [WidePullback.π_arrow]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ s f S n ≫ WidePullback.π (fun x => f.hom) 0 = (WidePullback.base fun x => f.hom) ≫ S.section_
[PROOFSTEP]
dsimp [ExtraDegeneracy.s]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i =>
          if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
          else WidePullback.π (fun x => f.hom) (Fin.pred i x))
        (_ :
          ∀ (i : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            (fun i =>
                    if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
                    else WidePullback.π (fun x => f.hom) (Fin.pred i x))
                  i ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.π (fun x => f.hom) 0 =
    (WidePullback.base fun x => f.hom) ≫ S.section_
[PROOFSTEP]
simp only [WidePullback.lift_π]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ (if h : True then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred 0 (_ : ¬0 = 0))) =
    (WidePullback.base fun x => f.hom) ≫ S.section_
[PROOFSTEP]
rfl
  -- porting note: @[simp] removed as the linter complains the LHS is not in normal form
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.succ i) = WidePullback.π (fun x => f.hom) i
[PROOFSTEP]
dsimp [ExtraDegeneracy.s]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i =>
          if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
          else WidePullback.π (fun x => f.hom) (Fin.pred i x))
        (_ :
          ∀ (i : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            (fun i =>
                    if x : i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
                    else WidePullback.π (fun x => f.hom) (Fin.pred i x))
                  i ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.π (fun x => f.hom) (Fin.succ i) =
    WidePullback.π (fun x => f.hom) i
[PROOFSTEP]
simp only [WidePullback.lift_π]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (if x : Fin.succ i = 0 then (WidePullback.base fun x => f.hom) ≫ S.section_
    else WidePullback.π (fun x => f.hom) (Fin.pred (Fin.succ i) x)) =
    WidePullback.π (fun x => f.hom) i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
h : Fin.succ i = 0
⊢ (WidePullback.base fun x => f.hom) ≫ S.section_ = WidePullback.π (fun x => f.hom) i
[PROOFSTEP]
simp only [Fin.ext_iff, Fin.val_succ, Fin.val_zero, add_eq_zero, and_false] at h
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
h : ¬Fin.succ i = 0
⊢ WidePullback.π (fun x => f.hom) (Fin.pred (Fin.succ i) h) = WidePullback.π (fun x => f.hom) i
[PROOFSTEP]
simp only [Fin.pred_succ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ (s f S n ≫ WidePullback.base fun x => f.hom) = WidePullback.base fun x => f.hom
[PROOFSTEP]
apply WidePullback.lift_base
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
i : Fin (SimplexCategory.len (op [0]).unop + 1)
⊢ (fun x => 𝟙 ((𝟭 C).obj f.left)) i ≫ f.hom = f.hom
[PROOFSTEP]
rw [id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
⊢ (S.section_ ≫
        WidePullback.lift f.hom (fun x => 𝟙 ((𝟭 C).obj f.left))
          (_ :
            ∀ (i : Fin (SimplexCategory.len (op [0]).unop + 1)), (fun x => 𝟙 ((𝟭 C).obj f.left)) i ≫ f.hom = f.hom)) ≫
      NatTrans.app (augmentedCechNerve f).hom (op [0]) =
    𝟙 (point.obj (augmentedCechNerve f))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
⊢ ((S.section_ ≫ WidePullback.lift f.hom (fun x => 𝟙 f.left) (_ : Fin (0 + 1) → 𝟙 f.left ≫ f.hom = f.hom)) ≫
      WidePullback.base fun x => f.hom) =
    𝟙 f.right
[PROOFSTEP]
simp only [augmentedCechNerve_hom_app, assoc, WidePullback.lift_base, SplitEpi.id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
⊢ (fun n => ExtraDegeneracy.s f S n) 0 ≫ SimplicialObject.δ (augmentedCechNerve f).left 1 =
    NatTrans.app (augmentedCechNerve f).hom (op [0]) ≫
      S.section_ ≫
        WidePullback.lift f.hom (fun x => 𝟙 ((𝟭 C).obj f.left))
          (_ : ∀ (i : Fin (SimplexCategory.len (op [0]).unop + 1)), (fun x => 𝟙 ((𝟭 C).obj f.left)) i ≫ f.hom = f.hom)
[PROOFSTEP]
dsimp [cechNerve, SimplicialObject.δ, SimplexCategory.δ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
⊢ ExtraDegeneracy.s f S 0 ≫
      WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i => WidePullback.π (fun x => f.hom) (Fin.succAbove 1 i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [0]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb 1))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) =
    (WidePullback.base fun x => f.hom) ≫
      S.section_ ≫ WidePullback.lift f.hom (fun x => 𝟙 f.left) (_ : Fin (0 + 1) → 𝟙 f.left ≫ f.hom = f.hom)
[PROOFSTEP]
ext j
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
j : Fin (0 + 1)
⊢ (ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i => WidePullback.π (fun x => f.hom) (Fin.succAbove 1 i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [0]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb 1))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.π (fun x => f.hom) j =
    ((WidePullback.base fun x => f.hom) ≫
        S.section_ ≫ WidePullback.lift f.hom (fun x => 𝟙 f.left) (_ : Fin (0 + 1) → 𝟙 f.left ≫ f.hom = f.hom)) ≫
      WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.head
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
⊢ (ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i => WidePullback.π (fun x => f.hom) (Fin.succAbove 1 i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [0]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb 1))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.π (fun x => f.hom) { val := 0, isLt := (_ : 0 < 0 + 1) } =
    ((WidePullback.base fun x => f.hom) ≫
        S.section_ ≫ WidePullback.lift f.hom (fun x => 𝟙 f.left) (_ : Fin (0 + 1) → 𝟙 f.left ≫ f.hom = f.hom)) ≫
      WidePullback.π (fun x => f.hom) { val := 0, isLt := (_ : 0 < 0 + 1) }
[PROOFSTEP]
simpa only [assoc, WidePullback.lift_π, comp_id] using ExtraDegeneracy.s_comp_π_0 f S 0
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i => WidePullback.π (fun x => f.hom) (Fin.succAbove 1 i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [0]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb 1))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.base fun x => f.hom) =
    ((WidePullback.base fun x => f.hom) ≫
        S.section_ ≫ WidePullback.lift f.hom (fun x => 𝟙 f.left) (_ : Fin (0 + 1) → 𝟙 f.left ≫ f.hom = f.hom)) ≫
      WidePullback.base fun x => f.hom
[PROOFSTEP]
simpa only [assoc, WidePullback.lift_base, SplitEpi.id, comp_id] using ExtraDegeneracy.s_comp_base f S 0
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ (fun n => ExtraDegeneracy.s f S n) n ≫ SimplicialObject.δ (augmentedCechNerve f).left 0 =
    𝟙 ((drop.obj (augmentedCechNerve f)).obj (op [n]))
[PROOFSTEP]
dsimp [cechNerve, SimplicialObject.δ, SimplexCategory.δ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ ExtraDegeneracy.s f S n ≫
      WidePullback.lift (WidePullback.base fun x => f.hom) (fun i => WidePullback.π (fun x => f.hom) (Fin.succ i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb 0))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) =
    𝟙 (widePullback f.right (fun x => f.left) fun x => f.hom)
[PROOFSTEP]
ext j
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
j : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x => f.hom) (fun i => WidePullback.π (fun x => f.hom) (Fin.succ i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb 0))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.π (fun x => f.hom) j =
    𝟙 (widePullback f.right (fun x => f.left) fun x => f.hom) ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
simpa only [assoc, WidePullback.lift_π, id_comp] using ExtraDegeneracy.s_comp_π_succ f S n j
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
⊢ ((ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x => f.hom) (fun i => WidePullback.π (fun x => f.hom) (Fin.succ i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb 0))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.base fun x => f.hom) =
    𝟙 (widePullback f.right (fun x => f.left) fun x => f.hom) ≫ WidePullback.base fun x => f.hom
[PROOFSTEP]
simpa only [assoc, WidePullback.lift_base, id_comp] using ExtraDegeneracy.s_comp_base f S n
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (fun n => ExtraDegeneracy.s f S n) (n + 1) ≫ SimplicialObject.δ (augmentedCechNerve f).left (Fin.succ i) =
    SimplicialObject.δ (augmentedCechNerve f).left i ≫ (fun n => ExtraDegeneracy.s f S n) n
[PROOFSTEP]
dsimp [cechNerve, SimplicialObject.δ, SimplexCategory.δ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ ExtraDegeneracy.s f S (n + 1) ≫
      WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb (Fin.succ i)))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n
[PROOFSTEP]
ext j
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb (Fin.succ i)))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.π (fun x => f.hom) j =
    (WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom) ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
simp only [assoc, WidePullback.lift_π]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
⊢ ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
⊢ ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
h : j = 0
⊢ ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) 0) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) 0
[PROOFSTEP]
erw [Fin.succ_succAbove_zero, ExtraDegeneracy.s_comp_π_0, ExtraDegeneracy.s_comp_π_0]
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (WidePullback.base fun x => f.hom) ≫ S.section_ =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      (WidePullback.base fun x => f.hom) ≫ S.section_
[PROOFSTEP]
dsimp
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (WidePullback.base fun x => f.hom) ≫ S.section_ =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      (WidePullback.base fun x => f.hom) ≫ S.section_
[PROOFSTEP]
simp only [WidePullback.lift_base_assoc]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
h : ¬j = 0
⊢ ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
cases' Fin.eq_succ_of_ne_zero h with k hk
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
h : ¬j = 0
k : Fin (n + 1)
hk : j = Fin.succ k
⊢ ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
subst hk
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
k : Fin (n + 1)
h : ¬Fin.succ k = 0
⊢ ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) (Fin.succ k)) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.succ k)
[PROOFSTEP]
erw [Fin.succ_succAbove_succ, ExtraDegeneracy.s_comp_π_succ, ExtraDegeneracy.s_comp_π_succ]
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
k : Fin (n + 1)
h : ¬Fin.succ k = 0
⊢ WidePullback.π (fun x => f.hom) (Fin.succAbove i k) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.π (fun x => f.hom) k
[PROOFSTEP]
simp only [WidePullback.lift_π]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ ((ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove (Fin.succ i) i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb (Fin.succ i)))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.base fun x => f.hom) =
    (WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom) ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.base fun x => f.hom
[PROOFSTEP]
simp only [assoc, WidePullback.lift_base]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S n ≫ WidePullback.base fun x => f.hom
[PROOFSTEP]
erw [ExtraDegeneracy.s_comp_base, ExtraDegeneracy.s_comp_base]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.base fun x => f.hom
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.succAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk (OrderEmbedding.toOrderHom (Fin.succAboveEmb i))).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.base fun x => f.hom
[PROOFSTEP]
simp only [WidePullback.lift_base]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (fun n => ExtraDegeneracy.s f S n) n ≫ SimplicialObject.σ (augmentedCechNerve f).left (Fin.succ i) =
    SimplicialObject.σ (augmentedCechNerve f).left i ≫ (fun n => ExtraDegeneracy.s f S n) (n + 1)
[PROOFSTEP]
dsimp [cechNerve, SimplicialObject.σ, SimplexCategory.σ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ ExtraDegeneracy.s f S n ≫
      WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove (Fin.succ i),
                                monotone' := (_ : Monotone (Fin.predAbove (Fin.succ i))) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1)
[PROOFSTEP]
ext j
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
j : Fin (n + 1 + 1 + 1)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk
                                { toFun := Fin.predAbove (Fin.succ i),
                                  monotone' := (_ : Monotone (Fin.predAbove (Fin.succ i))) }).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.π (fun x => f.hom) j =
    (WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk
                                { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom) ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
simp only [assoc, WidePullback.lift_π]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
j : Fin (n + 1 + 1 + 1)
⊢ ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
j : Fin (n + 1 + 1 + 1)
⊢ ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
by_cases j = 0
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
j : Fin (n + 1 + 1 + 1)
h : j = 0
⊢ ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) 0) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) 0
[PROOFSTEP]
erw [ExtraDegeneracy.s_comp_π_0, ExtraDegeneracy.s_comp_π_0]
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (WidePullback.base fun x => f.hom) ≫ S.section_ =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      (WidePullback.base fun x => f.hom) ≫ S.section_
[PROOFSTEP]
dsimp
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (WidePullback.base fun x => f.hom) ≫ S.section_ =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      (WidePullback.base fun x => f.hom) ≫ S.section_
[PROOFSTEP]
simp only [WidePullback.lift_base_assoc]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
j : Fin (n + 1 + 1 + 1)
h : ¬j = 0
⊢ ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
cases' Fin.eq_succ_of_ne_zero h with k hk
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
j : Fin (n + 1 + 1 + 1)
h : ¬j = 0
k : Fin (n + 2)
hk : j = Fin.succ k
⊢ ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) j) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) j
[PROOFSTEP]
subst hk
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
k : Fin (n + 2)
h : ¬Fin.succ k = 0
⊢ ExtraDegeneracy.s f S n ≫ WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) (Fin.succ k)) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.π (fun x => f.hom) (Fin.succ k)
[PROOFSTEP]
erw [Fin.succ_predAbove_succ, ExtraDegeneracy.s_comp_π_succ, ExtraDegeneracy.s_comp_π_succ]
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
k : Fin (n + 2)
h : ¬Fin.succ k = 0
⊢ WidePullback.π (fun x => f.hom) (Fin.predAbove i k) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.π (fun x => f.hom) k
[PROOFSTEP]
simp only [WidePullback.lift_π]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ ((ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove (Fin.succ i) i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n + 1 + 1]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk
                                { toFun := Fin.predAbove (Fin.succ i),
                                  monotone' := (_ : Monotone (Fin.predAbove (Fin.succ i))) }).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom)) ≫
      WidePullback.base fun x => f.hom) =
    (WidePullback.lift (WidePullback.base fun x => f.hom)
          (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
          (_ :
            ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
              WidePullback.π (fun x => f.hom)
                    (↑(SimplexCategory.Hom.toOrderHom
                          (SimplexCategory.Hom.mk
                                { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                      j) ≫
                  f.hom =
                WidePullback.base fun x => f.hom) ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.base fun x => f.hom
[PROOFSTEP]
simp only [assoc, WidePullback.lift_base]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S n ≫ WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      ExtraDegeneracy.s f S (n + 1) ≫ WidePullback.base fun x => f.hom
[PROOFSTEP]
erw [ExtraDegeneracy.s_comp_base, ExtraDegeneracy.s_comp_base]
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.base fun x => f.hom
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u_1
inst✝¹ : Category.{?u.319164, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (WidePullback.base fun x => f.hom) =
    WidePullback.lift (WidePullback.base fun x => f.hom)
        (fun i_1 => WidePullback.π (fun x => f.hom) (Fin.predAbove i i_1))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (op [n + 1]).unop + 1)),
            WidePullback.π (fun x => f.hom)
                  (↑(SimplexCategory.Hom.toOrderHom
                        (SimplexCategory.Hom.mk
                              { toFun := Fin.predAbove i, monotone' := (_ : Monotone (Fin.predAbove i)) }).op.unop)
                    j) ≫
                f.hom =
              WidePullback.base fun x => f.hom) ≫
      WidePullback.base fun x => f.hom
[PROOFSTEP]
simp only [WidePullback.lift_base]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
⊢ HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) i ⟶
    HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) j
[PROOFSTEP]
by_cases i + 1 = j
[GOAL]
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
⊢ HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) i ⟶
    HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) j
[PROOFSTEP]
by_cases i + 1 = j
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
h : i + 1 = j
⊢ HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) i ⟶
    HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) j
[PROOFSTEP]
exact (-ed.s i) ≫ eqToHom (by congr)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
h : i + 1 = j
⊢ (drop.obj X).obj (op [i + 1]) = HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) j
[PROOFSTEP]
congr
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
h : ¬i + 1 = j
⊢ HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) i ⟶
    HomologicalComplex.X (AlternatingFaceMapComplex.obj (drop.obj X)) j
[PROOFSTEP]
exact 0
[GOAL]
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
hij : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
⊢ (fun i j =>
        if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [j]))
        else 0)
      i j =
    0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
hij : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
⊢ (if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : X.left.obj (op [i + 1]) = X.left.obj (op [j])) else 0) = 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
hij : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
h : i + 1 = j
⊢ (-s ed i) ≫ eqToHom (_ : X.left.obj (op [i + 1]) = X.left.obj (op [j])) = 0
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
hij : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
h : i + 1 = j
⊢ False
[PROOFSTEP]
exact hij h
[GOAL]
case neg
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i j : ℕ
hij : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
h : ¬i + 1 = j
⊢ 0 = 0
[PROOFSTEP]
simp only [eq_self_iff_true]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i : ℕ
⊢ HomologicalComplex.Hom.f
      (NatTrans.app AlternatingFaceMapComplex.ε X ≫
        Equiv.invFun (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (drop.obj X)) (point.obj X)) ed.s')
      i =
    ((↑(dNext i) fun i j =>
          if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [j]))
          else 0) +
        ↑(prevD i) fun i j =>
          if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [j]))
          else 0) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))) i
[PROOFSTEP]
rcases i with _ | i
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
⊢ HomologicalComplex.Hom.f
      (NatTrans.app AlternatingFaceMapComplex.ε X ≫
        Equiv.invFun (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (drop.obj X)) (point.obj X)) ed.s')
      Nat.zero =
    ((↑(dNext Nat.zero) fun i j =>
          if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [j]))
          else 0) +
        ↑(prevD Nat.zero) fun i j =>
          if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [j]))
          else 0) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))) Nat.zero
[PROOFSTEP]
rw [Homotopy.prevD_chainComplex, Homotopy.dNext_zero_chainComplex, zero_add]
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
⊢ HomologicalComplex.Hom.f
      (NatTrans.app AlternatingFaceMapComplex.ε X ≫
        Equiv.invFun (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (drop.obj X)) (point.obj X)) ed.s')
      Nat.zero =
    (if h : Nat.zero + 1 = Nat.zero + 1 then
          (-s ed Nat.zero) ≫ eqToHom (_ : (drop.obj X).obj (op [Nat.zero + 1]) = (drop.obj X).obj (op [Nat.zero + 1]))
        else 0) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj (drop.obj X)) (Nat.zero + 1) Nat.zero +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))) Nat.zero
[PROOFSTEP]
dsimp [ChainComplex.fromSingle₀Equiv, ChainComplex.toSingle₀Equiv]
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
⊢ HomologicalComplex.Hom.f (NatTrans.app AlternatingFaceMapComplex.ε X) 0 ≫ ed.s' =
    (if 0 + 1 = 0 + 1 then (-s ed 0) ≫ 𝟙 (X.left.obj (op [0 + 1])) else 0) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj X.left) (0 + 1) 0 +
      𝟙 (X.left.obj (op [0]))
[PROOFSTEP]
simp only [comp_id, ite_true, zero_add, ComplexShape.down_Rel, not_true, AlternatingFaceMapComplex.obj_d_eq,
  Preadditive.neg_comp]
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
⊢ HomologicalComplex.Hom.f (NatTrans.app AlternatingFaceMapComplex.ε X) 0 ≫ ed.s' =
    (-s ed 0 ≫ Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X.left i) + 𝟙 (X.left.obj (op [0]))
[PROOFSTEP]
erw [Fin.sum_univ_two]
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
⊢ HomologicalComplex.Hom.f (NatTrans.app AlternatingFaceMapComplex.ε X) 0 ≫ ed.s' =
    -s ed 0 ≫ ((-1) ^ ↑0 • SimplicialObject.δ X.left 0 + (-1) ^ ↑1 • SimplicialObject.δ X.left 1) +
      𝟙 (X.left.obj (op [0]))
[PROOFSTEP]
simp only [Fin.val_zero, pow_zero, one_smul, Fin.val_one, pow_one, neg_smul, Preadditive.comp_add, s_comp_δ₀, drop_obj,
  Preadditive.comp_neg, neg_add_rev, neg_neg, neg_add_cancel_right, s₀_comp_δ₁]
[GOAL]
case zero
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
⊢ HomologicalComplex.Hom.f (NatTrans.app AlternatingFaceMapComplex.ε X) 0 ≫ ed.s' = NatTrans.app X.hom (op [0]) ≫ ed.s'
[PROOFSTEP]
rfl
[GOAL]
case succ
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i : ℕ
⊢ HomologicalComplex.Hom.f
      (NatTrans.app AlternatingFaceMapComplex.ε X ≫
        Equiv.invFun (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (drop.obj X)) (point.obj X)) ed.s')
      (Nat.succ i) =
    ((↑(dNext (Nat.succ i)) fun i j =>
          if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [j]))
          else 0) +
        ↑(prevD (Nat.succ i)) fun i j =>
          if h : i + 1 = j then (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [j]))
          else 0) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))) (Nat.succ i)
[PROOFSTEP]
rw [Homotopy.prevD_chainComplex, Homotopy.dNext_succ_chainComplex]
[GOAL]
case succ
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i : ℕ
⊢ HomologicalComplex.Hom.f
      (NatTrans.app AlternatingFaceMapComplex.ε X ≫
        Equiv.invFun (ChainComplex.fromSingle₀Equiv (AlternatingFaceMapComplex.obj (drop.obj X)) (point.obj X)) ed.s')
      (Nat.succ i) =
    (HomologicalComplex.d (AlternatingFaceMapComplex.obj (drop.obj X)) (i + 1) i ≫
          if h : i + 1 = i + 1 then
            (-s ed i) ≫ eqToHom (_ : (drop.obj X).obj (op [i + 1]) = (drop.obj X).obj (op [i + 1]))
          else 0) +
        (if h : Nat.succ i + 1 = Nat.succ i + 1 then
            (-s ed (Nat.succ i)) ≫
              eqToHom (_ : (drop.obj X).obj (op [Nat.succ i + 1]) = (drop.obj X).obj (op [Nat.succ i + 1]))
          else 0) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj (drop.obj X)) (Nat.succ i + 1) (Nat.succ i) +
      HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))) (Nat.succ i)
[PROOFSTEP]
dsimp [ChainComplex.toSingle₀Equiv, ChainComplex.fromSingle₀Equiv]
[GOAL]
case succ
C : Type u_1
inst✝² : Category.{?u.349752, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
ed : ExtraDegeneracy X
i : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app AlternatingFaceMapComplex.ε X) (Nat.succ i) ≫ 0 =
    (HomologicalComplex.d (AlternatingFaceMapComplex.obj X.left) (i + 1) i ≫
          if i + 1 = i + 1 then (-s ed i) ≫ 𝟙 (X.left.obj (op [i + 1])) else 0) +
        (if Nat.succ i + 1 = Nat.succ i + 1 then (-s ed (Nat.succ i)) ≫ 𝟙 (X.left.obj (op [Nat.succ i + 1])) else 0) ≫
          HomologicalComplex.d (AlternatingFaceMapComplex.obj X.left) (Nat.succ i + 1) (Nat.succ i) +
      𝟙 (X.left.obj (op [Nat.succ i]))
[PROOFSTEP]
simp only [comp_zero, ComplexShape.down_Rel, not_true, Preadditive.neg_comp, AlternatingFaceMapComplex.obj_d_eq,
  comp_id, ite_true, Preadditive.comp_neg, @Fin.sum_univ_succ _ _ (i + 2), Fin.val_zero, pow_zero, one_smul,
  Fin.val_succ, Preadditive.comp_add, drop_obj, s_comp_δ₀, Preadditive.sum_comp, Preadditive.zsmul_comp,
  Preadditive.comp_sum, Preadditive.comp_zsmul, zsmul_neg, ed.s_comp_δ, pow_add, pow_one, mul_neg, mul_one, neg_zsmul,
  neg_neg, neg_add_cancel_comm_assoc, add_left_neg]