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 + 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⦌))
⊢ 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⦌))
have 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⦌))
Tactic: obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by lia
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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⦌))
⊢ 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⦌))
have 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⦌))
Tactic: obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by lia
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
⊢ 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⦌))
have 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)
Tactic: rw [← spine_arrow, spine_δ_arrow_lt sx _ hlt]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
⊢ ((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)
have 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⦌)
Tactic: dsimp only [Path.map_arrow, spine_arrow, Fin.coe_eq_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
⊢ 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⦌)
have 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⦌))
          sorry :
        { x : Δ[n + 2] _⦋1⦌ // Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 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 + 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
⊢ 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⦌)
have 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⦌))
    sorry
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
⊢ (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⦌))
      ⋯
have 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⦌))
        sorry) :
    Δ[n + 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 + 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 =
    (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⦌)
have 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)
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
⊢ 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⦌))
have 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)
Tactic: rw [← spine_arrow, spine_δ_arrow_gt sx _ hgt]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
⊢ ((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)
have 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⦌))
          sorry :
        { x : Δ[n + 2] _⦋1⦌ // Membership.mem (γ := Set (Δ[n + 2] _⦋1⦌)) (Λ[n + 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 + 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
⊢ 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⦌)
have 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⦌))
    sorry
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
⊢ (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⦌))
      ⋯
have 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⦌))
        sorry) :
    Δ[n + 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 + 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
⊢ 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⦌)
have 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)
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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
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⦌))
have h : ∀ ⦃i : Fin (HAdd.hAdd (α := ℕ) 0 3)⦄ (σ₀ : Λ[HAdd.hAdd (α := ℕ) 0 2, i].toSSet ⟶ X) (h₀ : 0 < i)
  (hₙ : i < Fin.last (HAdd.hAdd (α := ℕ) 0 2)) (j : Fin (HAdd.hAdd (α := ℕ) 0 3)) (hj : j ≠ i)
  (k : Fin (HAdd.hAdd (α := ℕ) 0 1)),
  let ksucc := k.succ.castSucc;
  ∀ (heq : j = ksucc),
    Eq (α := X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc k).op) : (a : X _⦋0 + 1⦌) → X _⦋1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋0 + 1 + 1⦌) → X _⦋0 + 1⦌)
              (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
            X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) :
        X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Λ[HAdd.hAdd (α := ℕ) 0 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[0 + 2, i].toSSet _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (horn.face i j hj) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
Tactic: obtain _ | n := n
Cleared hypotheses: n, i, σ₀, h₀, hₙ, j, hj, k, ksucc, heq