Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.zero.«0»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨0, ⋯⟩
hₙ : (fun i ↦ i) ⟨0, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨0, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨0, ⋯⟩) j hj)

pp: case h.inr.inr.zero.«1»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨1, ⋯⟩
hₙ : (fun i ↦ i) ⟨1, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨1, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨1, ⋯⟩) j hj)

pp: case h.inr.inr.zero.«2»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨2, ⋯⟩
hₙ : (fun i ↦ i) ⟨2, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨2, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨2, ⋯⟩) j hj)

Tactic:
<;>

Goal state after:
case h.inr.inr.zero.«0»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨0, ⋯⟩
hₙ : (fun i ↦ i) ⟨0, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨0, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨0, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨0, ⋯⟩) j hj)

case h.inr.inr.zero.«1»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨1, ⋯⟩
hₙ : (fun i ↦ i) ⟨1, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨1, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨1, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨1, ⋯⟩) j hj)

case h.inr.inr.zero.«2»
X : SSet
sx : X.StrictSegal
j : Fin (0 + 3)
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
σ₀ : Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet ⟶ X
h₀ : 0 < (fun i ↦ i) ⟨2, ⋯⟩
hₙ : (fun i ↦ i) ⟨2, ⋯⟩ < Fin.last (0 + 2)
hj : j ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j))
        (sx.spineToSimplex ((horn.spineId ((fun i ↦ i) ⟨2, ⋯⟩) h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, (fun i ↦ i) ⟨2, ⋯⟩].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌)))
      (horn.face ((fun i ↦ i) ⟨2, ⋯⟩) j hj)