awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow m) : Δ[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 (mkOfSucc m).op) :
                    (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, ⋯⟩))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩))
  ((((↑(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, sorry⟩ : Fin (⦋1⦌.len + 1)))))) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
              sorry) :
          Δ[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, sorry⟩))
Tactic: fin_cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (hypothesis)
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 (α := 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⦌))
have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 sorry =
  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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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)
⊢ 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⦌))
have 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)
Tactic: rw [← spine_arrow, spine_δ_arrow_eq sx _ heq, hi]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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)
⊢ 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)
have 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⦌)
Tactic: simp only [spineToDiagonal, diagonal, spineToSimplex_spine_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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)
⊢ 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⦌)
have 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⦌)
Tactic: rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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)
⊢ 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⦌)
have 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⦌))
          sorry :
        { 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⦌))
          sorry :
        { x : Δ[n + 1 + 2] _⦋1⦌ //
          Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x }) :
    X _⦋1⦌)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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)
⊢ 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 })
have 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⦌))
          sorry) :
      Δ[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⦌))
          sorry) :
      Δ[n + 1 + 2] _⦋1⦌) :
    Δ[n + 1 + 2] _⦋1⦌)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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)
⊢ 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⦌)
have 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⦌))
                  sorry) :
              Δ[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⦌))
                  sorry) :
              Δ[n + 1 + 2] _⦋1⦌) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
Tactic: ext z : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((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⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑((yonedaEquiv :
                      (a : Δ[n + 1 + 1] ⟶ Λ[n + 1 + 1 + 1, i].toSSet) →
                        (↑(Λ[n + 1 + 1 + 1, i].obj (Opposite.op ⦋n + 1 + 1⦌)) : Type u))
                    (Subfunctor.lift (stdSimplex.δ j) ⋯)) :
                Δ[n + 1 + 2] _⦋n + 1 + 1⦌) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := Opposite.unop (Opposite.op ⦋2⦌)) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)
                (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (mkOfSucc k ≫
              ((stdSimplex.objEquiv :
                    Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)
                ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                  (stdSimplex.δ j))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
Tactic: rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
        Quiver.Hom.unop_op, stdSimplex.map_apply, Quiver.Hom.unop_op]