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
heq : j = ksucc
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⦌))
⊢ 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₁ : ∀ (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)),
  let ksucc := k.succ.castSucc;
  ∀ (heq : j = ksucc),
    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: obtain _ | n := n
Cleared hypotheses: n, i, σ₀, h₀, hₙ, j, hj, k, ksucc, heq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
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)
ksucc : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1 + 1) := 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⦌))
have h : let ksucc : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1 + 1) := Fin.castSucc (Fin.succ 0);
∀ (heq : j = ksucc),
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (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 (Quiver.Hom.op (mkOfSucc 0)) ≫ σ₀.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 rfl : k = 0 := by omega
Cleared hypotheses: k, ksucc, heq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
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
ksucc : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1 + 1) := Fin.castSucc (Fin.succ 0)
heq : j = ksucc
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (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 (Quiver.Hom.op (mkOfSucc 0)) ≫ σ₀.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⦌))
have h : ∀
  (σ₀ :
    Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
        Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋2⦌.len + 1))] ⟶
      X)
  (h₀ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) 0 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
  (hₙ :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, sorry⟩)
      (Fin.last (HAdd.hAdd (α := ℕ) 0 2)))
  (hj : j ≠ (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, sorry⟩),
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (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 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋2⦌.len + 1))) h₀ hₙ).map σ₀)) :
          X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
                    Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋2⦌.len + 1))]).map
                (Quiver.Hom.op (mkOfSucc 0)) ≫
              σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[0 + 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, sorry⟩].toSSet _⦋0 + 1⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋2⦌.len + 1))) j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))
Tactic: fin_cases i
Cleared hypotheses: i, σ₀, h₀, hₙ, hj
-- 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 : ℕ) ⋯
⊢ ((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)
have h : ∀ (m : Fin (HAdd.hAdd (α := ℕ) 1 1)),
  (((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 sorry).arrow m =
    Path.arrow
      (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))
      m
Tactic: ext m
-- 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)
⊢ (((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯).arrow m =
    Path.arrow
      (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))
      m
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⦌)
      (((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow m) :
    X _⦋1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc m).op) : (a : X _⦋2⦌) → X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
            (a : (↑(Λ[n + 1 + 2, i].obj (Opposite.op ⦋2⦌)) : Type u)) → X _⦋2⦌)
          triangle :
        X _⦋2⦌) :
    X _⦋1⦌)
Tactic: dsimp [spine_arrow, Path.map_interval, Path.map_arrow]
-- 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 (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (↑(Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) : Type u)) → X _⦋1⦌)
        (((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow m) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (mkOfSucc m).op) : (a : X _⦋2⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
              (a : (↑(Λ[n + 1 + 2, i].obj (Opposite.op ⦋2⦌)) : Type u)) → X _⦋2⦌)
            triangle :
          X _⦋2⦌) :
      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⦌)
      (((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow m) :
    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 m).op) :
              (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⦌)
Tactic: rw [← dsimp% σ₀.naturality_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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ 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⦌)
        (((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow m) :
      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 m).op) :
                (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⦌)
have h : ((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow m =
  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⦌))
    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 + 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)
⊢ ((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow m =
    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⦌))
      ⋯
have h : (↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow m) : Δ[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 m).op) :
            (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
          (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
        sorry) :
    Δ[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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ (↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow m) : Δ[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 m).op) :
              (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
          ⋯) :
      Δ[n + 1 + 2] _⦋1⦌)
have h : ∀ (a : Fin (HAdd.hAdd (α := ℕ) 1 1)),
  Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow m) : Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
        a :
      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 m).op) :
                      (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))
        a :
      Fin (n + 1 + 2 + 1))
Tactic: ext a : 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 : ℕ) ⋯
m a : 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))
        a :
      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 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))
        a :
      Fin (n + 1 + 2 + 1))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow m) : Δ[n + 1 + 2] _⦋1⦌) :
      (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, 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 (mkOfSucc m).op) :
                  (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) ⟨0, sorry⟩))
Tactic: fin_cases a
Cleared hypotheses: a
-- 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 a : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  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) ⟨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 (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) ⟨0, ⋯⟩))
⊢ 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))
        a :
      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 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))
        a :
      Fin (n + 1 + 2 + 1))
have h₁ : Eq (α := Fin (n + 1 + 2 + 1))
  (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow m) : Δ[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 (mkOfSucc m).op) :
                  (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 a
Cleared hypotheses: a
-- 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) ⟨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 (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) ⟨0, ⋯⟩))
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) ⟨0, 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) ⟨0, sorry⟩))
Tactic: fin_cases m
Cleared hypotheses: m