awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow
              ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Δ[n + 1 + 2].map
                        (Quiver.Hom.op (mkOfSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))))) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
                ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow
              ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Δ[n + 1 + 2].map
                        (Quiver.Hom.op (mkOfSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))))) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
                ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow
              ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))
    ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Δ[n + 1 + 2].map
                        (Quiver.Hom.op (mkOfSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))))) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
                ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow
              ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))
    ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Δ[n + 1 + 2].map
                        (Quiver.Hom.op (mkOfSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))))) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
                ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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ₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)

Tactic:
have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by grind) =
          X.spine 2 (σ₀.app _ triangle) := by
        ext m
        dsimp [spine_arrow, Path.map_interval, Path.map_arrow]
        rw [← dsimp% σ₀.naturality_apply]
        apply congr_arg
        apply Subtype.ext
        ext a : 1
        fin_cases a <;> fin_cases m <;> rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
h :
  sx.spineToDiagonal (n := 2)
      (X.spine 2
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
          triangle)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (horn.face i j hj)
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1 + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋n + 1 + 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face i j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))

Tactic:
rw [← spine_arrow, spine_δ_arrow_eq sx _ heq, hi]

Premises used: SSet.StrictSegal.spine_δ_arrow_eq, SSet.spine_arrow
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (diag 2))) : (a : X _⦋2⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
              (a : Λ[n + 1 + 2, i].toSSet _⦋2⦌) → X _⦋2⦌)
            triangle :
          X _⦋2⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : Λ[n + 1 + 2, i].toSSet _⦋n + 1 + 1⦌) → X _⦋1⦌)
        (horn.face i j hj) :
      X _⦋1⦌)
⊢ sx.spineToDiagonal (n := 2)
      (X.spine 2
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
          triangle)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (horn.face i j hj)

Tactic:
simp only [spineToDiagonal, diagonal, spineToSimplex_spine_apply]

Premises used: SSet.StrictSegal.spineToDiagonal, CategoryTheory.SimplicialObject.diagonal, SSet.StrictSegal.spineToSimplex_spine_apply
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (Quiver.Hom.op (diag 2))) :
              (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) →
                (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋1⦌))
            triangle :
          (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋1⦌)) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : Λ[n + 1 + 2, i].toSSet _⦋n + 1 + 1⦌) → X _⦋1⦌)
        (horn.face i j hj) :
      X _⦋1⦌)
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (diag 2))) : (a : X _⦋2⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
              (a : Λ[n + 1 + 2, i].toSSet _⦋2⦌) → X _⦋2⦌)
            triangle :
          X _⦋2⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : Λ[n + 1 + 2, i].toSSet _⦋n + 1 + 1⦌) → X _⦋1⦌)
        (horn.face i j hj) :
      X _⦋1⦌)

Tactic:
rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]

Premises used: CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.app, CategoryTheory.types_comp_apply
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        (Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (Quiver.Hom.op (diag 2))) :
                (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
            ⋯ :
          { x : Δ[n + 1 + 2] _⦋1⦌ //
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x }) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        (Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑(horn.face i j hj) : Δ[n + 1 + 2] _⦋n + 1 + 1⦌))
            ⋯ :
          { x : Δ[n + 1 + 2] _⦋1⦌ //
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x }) :
      X _⦋1⦌)
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (Quiver.Hom.op (diag 2))) :
              (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) →
                (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋1⦌))
            triangle :
          (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋1⦌)) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : Λ[n + 1 + 2, i].toSSet _⦋n + 1 + 1⦌) → X _⦋1⦌)
        (horn.face i j hj) :
      X _⦋1⦌)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
h :
  Eq (α := Δ[n + 1 + 2] _⦋1⦌)
    ((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (Quiver.Hom.op (diag 2))) :
                (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
            ⋯) :
        Δ[n + 1 + 2] _⦋1⦌) :
      Δ[n + 1 + 2] _⦋1⦌)
    ((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑(horn.face i j hj) : Δ[n + 1 + 2] _⦋n + 1 + 1⦌))
            ⋯) :
        Δ[n + 1 + 2] _⦋1⦌) :
      Δ[n + 1 + 2] _⦋1⦌)
⊢ Eq (α :=
    { x : Δ[n + 1 + 2] _⦋1⦌ //
      Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x })
    (Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
        Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (Quiver.Hom.op (diag 2))) :
            (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
          (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
        ⋯ :
      { x : Δ[n + 1 + 2] _⦋1⦌ //
        Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x })
    (Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
        Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc k).op) :
            (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Δ[n + 1 + 2] _⦋1⦌)
          (↑(horn.face i j hj) : Δ[n + 1 + 2] _⦋n + 1 + 1⦌))
        ⋯ :
      { x : Δ[n + 1 + 2] _⦋1⦌ //
        Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x })

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
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 : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
h :
  ∀ (z : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    Eq (α := Fin (n + 1 + 2 + 1))
      ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                    Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (Quiver.Hom.op (diag 2))) :
                        (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                      (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
                    ⋯) :
                Δ[n + 1 + 2] _⦋1⦌) :
              Δ[n + 1 + 2] _⦋1⦌) :
            (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
          z :
        Fin (n + 1 + 2 + 1))
      ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                    Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc k).op) :
                        (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Δ[n + 1 + 2] _⦋1⦌)
                      (↑(horn.face i j hj) : Δ[n + 1 + 2] _⦋n + 1 + 1⦌))
                    ⋯) :
                Δ[n + 1 + 2] _⦋1⦌) :
              Δ[n + 1 + 2] _⦋1⦌) :
            (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
          z :
        Fin (n + 1 + 2 + 1))
⊢ Eq (α := Δ[n + 1 + 2] _⦋1⦌)
    ((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (Quiver.Hom.op (diag 2))) :
                (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
            ⋯) :
        Δ[n + 1 + 2] _⦋1⦌) :
      Δ[n + 1 + 2] _⦋1⦌)
    ((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑(horn.face i j hj) : Δ[n + 1 + 2] _⦋n + 1 + 1⦌))
            ⋯) :
        Δ[n + 1 + 2] _⦋1⦌) :
      Δ[n + 1 + 2] _⦋1⦌)

Tactic:
ext z : 1