Lean4
/-- If `X` and `Y` are isomorphic augmented simplicial objects, then an extra
degeneracy for `X` gives also an extra degeneracy for `Y` -/
def ofIso {X Y : SimplicialObject.Augmented C} (e : X ≅ Y) (ed : ExtraDegeneracy X) : ExtraDegeneracy Y
where
s' := (point.mapIso e).inv ≫ ed.s' ≫ (drop.mapIso e).hom.app (op ⦋0⦌)
s n := (drop.mapIso e).inv.app (op ⦋n⦌) ≫ ed.s n ≫ (drop.mapIso e).hom.app (op ⦋n + 1⦌)
s'_comp_ε := by simpa only [Functor.mapIso, assoc, w₀, ed.s'_comp_ε_assoc] using (point.mapIso e).inv_hom_id
s₀_comp_δ₁ := by
have h := w₀ e.inv
dsimp at h ⊢
simp only [assoc, ← SimplicialObject.δ_naturality, ed.s₀_comp_δ₁_assoc, reassoc_of% h]
s_comp_δ₀
n := by
have h := ed.s_comp_δ₀
dsimp at h ⊢
simpa only [assoc, ← SimplicialObject.δ_naturality, reassoc_of% h] using
congr_app (drop.mapIso e).inv_hom_id (op ⦋n⦌)
s_comp_δ n
i := by
have h := ed.s_comp_δ n i
dsimp at h ⊢
simp only [assoc, ← SimplicialObject.δ_naturality, reassoc_of% h, ← SimplicialObject.δ_naturality_assoc]
s_comp_σ n
i := by
have h := ed.s_comp_σ n i
dsimp at h ⊢
simp only [assoc, ← SimplicialObject.σ_naturality, reassoc_of% h, ← SimplicialObject.σ_naturality_assoc]
