Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case «0».«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨0, ⋯⟩)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨0, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «0».«1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨1, ⋯⟩)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨1, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1».«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨0, ⋯⟩)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨0, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case «1».«1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨1, ⋯⟩)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨1, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0».«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨0, ⋯⟩)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨0, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨1, ⋯⟩)) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨1, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨0, ⋯⟩)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨0, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow ((fun i ↦ i) ⟨1, ⋯⟩)) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc ((fun i ↦ i) ⟨1, ⋯⟩)).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)