awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
h :
  ∀ (k : Fin (n + 1)),
    Eq.{u + 1} (α := X _⦋1⦌)
      (Path.arrow
        ((sx.spineEquiv (n + 1) : (a : X _⦋n + 1⦌) → X.Path (n + 1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
                (a : (fun (X : Type u) ↦ X) (X _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
              (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
            (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
        k)
      (Path.arrow
        ((sx.spineEquiv (n + 1) : (a : X _⦋n + 1⦌) → X.Path (n + 1))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
              (horn.face i j hj) :
            (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
        k)
⊢ Eq (α := X.Path (n + 1))
    ((sx.spineEquiv (n + 1) : (a : X _⦋n + 1⦌) → X.Path (n + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) :
      X.Path (n + 1))
    ((sx.spineEquiv (n + 1) : (a : X _⦋n + 1⦌) → X.Path (n + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
            (horn.face i j hj) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) :
      X.Path (n + 1))

Tactic:
ext k
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
              (a : Λ[n + 2, i].toSSet _⦋n + 1⦌) → X _⦋n + 1⦌)
            (horn.face i j hj) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)
⊢ Eq.{u + 1} (α := X _⦋1⦌)
    (Path.arrow
      ((sx.spineEquiv (n + 1) : (a : X _⦋n + 1⦌) → X.Path (n + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      k)
    (Path.arrow
      ((sx.spineEquiv (n + 1) : (a : X _⦋n + 1⦌) → X.Path (n + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
            (horn.face i j hj) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      k)

Tactic:
dsimp only [spineEquiv, spine_arrow, Function.comp_apply, Equiv.coe_fn_mk]

Premises used: SSet.spine_arrow, Equiv.coe_fn_mk, Function.comp_apply, SSet.StrictSegal.spineEquiv
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face i j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
              (a : Λ[n + 2, i].toSSet _⦋n + 1⦌) → X _⦋n + 1⦌)
            (horn.face i j hj) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)

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

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 + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
⊢ ksucc < j ∨ j < ksucc ∨ j = ksucc

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
h :
  ∀ (hlt : ksucc < j),
    Eq (α := X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
              (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
            X _⦋n + 1⦌) :
        X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (horn.face i j hj) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
h₁ :
  ∀ (hgt : j < ksucc),
    Eq (α := X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
              (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
            X _⦋n + 1⦌) :
        X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (horn.face i j hj) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
h₂ :
  ∀ (heq : j = ksucc),
    Eq (α := X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
              (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
            X _⦋n + 1⦌) :
        X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (horn.face i j hj) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋n + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face i j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))

Tactic:
obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by lia
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
h :
  ((horn.spineId i h₀ hₙ).map σ₀).arrow k.castSucc =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 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⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 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_lt sx _ hlt]

Premises used: SSet.StrictSegal.spine_δ_arrow_lt, SSet.spine_arrow
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) : (a : Λ[n + 2, i].toSSet _⦋1⦌) → X _⦋1⦌)
        ((horn.spineId i h₀ hₙ).arrow k.castSucc) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : Λ[n + 2, i].toSSet _⦋n + 1⦌) → X _⦋1⦌)
        (horn.face i j hj) :
      X _⦋1⦌)
⊢ ((horn.spineId i h₀ hₙ).map σ₀).arrow k.castSucc =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (horn.face i j hj)

Tactic:
dsimp only [Path.map_arrow, spine_arrow, Fin.coe_eq_castSucc]

Premises used: SSet.spine_arrow, SSet.Path.map_arrow, Fin.coe_eq_castSucc
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        ((horn.spineId i h₀ hₙ).arrow k.castSucc) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        (Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
              (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
            ⋯ :
          { x : Δ[n + 2] _⦋1⦌ // Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x }) :
      X _⦋1⦌)
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) : (a : Λ[n + 2, i].toSSet _⦋1⦌) → X _⦋1⦌)
        ((horn.spineId i h₀ hₙ).arrow k.castSucc) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : Λ[n + 2, i].toSSet _⦋n + 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 + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
h :
  (horn.spineId i h₀ hₙ).arrow k.castSucc =
    Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
      Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
          (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
        (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
      ⋯
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        ((horn.spineId i h₀ hₙ).arrow k.castSucc) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        (Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
              (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
            ⋯ :
          { x : Δ[n + 2] _⦋1⦌ // Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x }) :
      X _⦋1⦌)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
h :
  (↑((horn.spineId i h₀ hₙ).arrow k.castSucc) : Δ[n + 2] _⦋1⦌) =
    (↑(Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
          Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
              (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
            (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
          ⋯) :
      Δ[n + 2] _⦋1⦌)
⊢ (horn.spineId i h₀ hₙ).arrow k.castSucc =
    Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
      Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
          (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
        (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
      ⋯

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
h :
  Path.arrow (stdSimplex.spineId (n + 2)) k.castSucc =
    (Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 2⦌) → Δ[n + 2] _⦋1⦌)
      (mkOfSucc k.castSucc)
⊢ Path.arrow (stdSimplex.spineId (n + 2)) k.castSucc =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) : (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
      (↑((yonedaEquiv :
              (a : Δ[n + 1] ⟶ Λ[n + 1 + 1, i].toSSet) → (↑(Λ[n + 1 + 1, i].obj (Opposite.op ⦋n + 1⦌)) : Type u))
            (Subfunctor.lift (stdSimplex.map (SimplexCategory.δ j)) ⋯)) :
        Δ[n + 2] _⦋n + 1⦌)

Tactic:
rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
      Quiver.Hom.unop_op, SSet.yonedaEquiv_map, Equiv.apply_symm_apply,
      mkOfSucc_δ_lt hlt]

Premises used: Equiv.apply_symm_apply, Quiver.Hom.unop_op, SimplexCategory.mkOfSucc_δ_lt, SSet.Subcomplex.yonedaEquiv_coe, SSet.stdSimplex.map_apply, CategoryTheory.Subfunctor.lift_ι, SSet.yonedaEquiv_map
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ Path.arrow (stdSimplex.spineId (n + 2)) k.castSucc =
    (Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 2⦌) → Δ[n + 2] _⦋1⦌)
      (mkOfSucc k.castSucc)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
h :
  ((horn.spineId i h₀ hₙ).map σ₀).arrow k.succ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 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⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋n + 1 + 1⦌) → X _⦋n + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋n + 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 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_gt sx _ hgt]

Premises used: SSet.spine_arrow, SSet.StrictSegal.spine_δ_arrow_gt
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
h :
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        ((horn.spineId i h₀ hₙ).arrow k.succ) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        (Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
              (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
            ⋯ :
          { x : Δ[n + 2] _⦋1⦌ // Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x }) :
      X _⦋1⦌)
⊢ ((horn.spineId i h₀ hₙ).map σ₀).arrow k.succ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      (horn.face i j hj)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
h :
  (horn.spineId i h₀ hₙ).arrow k.succ =
    Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
      Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
          (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
        (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
      ⋯
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        ((horn.spineId i h₀ hₙ).arrow k.succ) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        (Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
            Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
              (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
            ⋯ :
          { x : Δ[n + 2] _⦋1⦌ // Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x }) :
      X _⦋1⦌)

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
h :
  (↑((horn.spineId i h₀ hₙ).arrow k.succ) : Δ[n + 2] _⦋1⦌) =
    (↑(Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
          Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
              (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
            (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
          ⋯) :
      Δ[n + 2] _⦋1⦌)
⊢ (horn.spineId i h₀ hₙ).arrow k.succ =
    Subtype.mk (p := fun (x : Δ[n + 2] _⦋1⦌) ↦
      Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 2, i].obj (Opposite.op ⦋1⦌)) x)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) :
          (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
        (↑(horn.face i j hj) : Δ[n + 2] _⦋n + 1⦌))
      ⋯

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
h :
  Path.arrow (stdSimplex.spineId (n + 2)) k.succ =
    (Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 2⦌) → Δ[n + 2] _⦋1⦌) (mkOfSucc k.succ)
⊢ Path.arrow (stdSimplex.spineId (n + 2)) k.succ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 2].map (mkOfSucc k).op) : (a : Δ[n + 2] _⦋n + 1⦌) → Δ[n + 2] _⦋1⦌)
      (↑((yonedaEquiv :
              (a : Δ[n + 1] ⟶ Λ[n + 1 + 1, i].toSSet) → (↑(Λ[n + 1 + 1, i].obj (Opposite.op ⦋n + 1⦌)) : Type u))
            (Subfunctor.lift (stdSimplex.map (SimplexCategory.δ j)) ⋯)) :
        Δ[n + 2] _⦋n + 1⦌)

Tactic:
rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
      Quiver.Hom.unop_op, SSet.yonedaEquiv_map, Equiv.apply_symm_apply,
      mkOfSucc_δ_gt hgt]

Premises used: Equiv.apply_symm_apply, Quiver.Hom.unop_op, SSet.Subcomplex.yonedaEquiv_coe, SSet.stdSimplex.map_apply, CategoryTheory.Subfunctor.lift_ι, SimplexCategory.mkOfSucc_δ_gt, SSet.yonedaEquiv_map