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
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ 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:
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
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⦌))
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⦌))
⊢ 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 _ | n := n
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
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
⊢ k = 0

Tactic:
omega
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
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
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⦌))
⊢ 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 rfl : k = 0 := by omega

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
j : Fin (HAdd.hAdd (α := ℕ) 0 3)
ksucc : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1 + 1) := Fin.castSucc (Fin.succ 0)
heq : j = ksucc
σ₀ :
  Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
      Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))] ⟶
    X
h₀ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) 0 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)
hₙ :
  LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)
    (Fin.last (HAdd.hAdd (α := ℕ) 0 2))
hj : j ≠ (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩
⊢ 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, ⋯⟩ : 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, ⋯⟩ : 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, ⋯⟩].toSSet _⦋0 + 1⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))

Tactic:
contradiction
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
j : Fin (HAdd.hAdd (α := ℕ) 0 3)
ksucc : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1 + 1) := Fin.castSucc (Fin.succ 0)
heq : j = ksucc
σ₀ :
  Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
      Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))] ⟶
    X
h₀ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) 0 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)
hₙ :
  LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)
    (Fin.last (HAdd.hAdd (α := ℕ) 0 2))
hj : j ≠ (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩
⊢ 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) (⟨1, ⋯⟩ : 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) (⟨1, ⋯⟩ : 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) ⟨1, ⋯⟩].toSSet _⦋0 + 1⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))

Tactic:
contradiction
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
j : Fin (HAdd.hAdd (α := ℕ) 0 3)
ksucc : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1 + 1) := Fin.castSucc (Fin.succ 0)
heq : j = ksucc
σ₀ :
  Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
      Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))] ⟶
    X
h₀ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) 0 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, ⋯⟩)
hₙ :
  LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, ⋯⟩)
    (Fin.last (HAdd.hAdd (α := ℕ) 0 2))
hj : j ≠ (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, ⋯⟩
⊢ 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) (⟨2, ⋯⟩ : 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) (⟨2, ⋯⟩ : 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) ⟨2, ⋯⟩].toSSet _⦋0 + 1⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, ⋯⟩ : Fin (⦋2⦌.len + 1))) j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))

Tactic:
contradiction
-- 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
⊢ (↑k : ℕ) < n + 2

Tactic:
grind
-- 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 : ℕ) ⋯
⊢ (↑k : ℕ) + 2 ≤ n + 1 + 2

Tactic:
grind
-- 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 : ℕ) ⋯
h :
  ∀ (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
⊢ ((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:
ext m
-- 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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
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 ⋯).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⦌)
⊢ (((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

Tactic:
dsimp [spine_arrow, Path.map_interval, Path.map_arrow]

Premises used: SSet.Path.map_interval, SSet.spine_arrow, SSet.Path.map_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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
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 ⋯).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⦌)
⊢ 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⦌)

Tactic:
rw [← dsimp% σ₀.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  ((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⦌))
      ⋯
⊢ 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⦌)

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  (↑(((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⦌)
⊢ ((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⦌))
      ⋯

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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  ∀ (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))
⊢ (↑(((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⦌)

Tactic:
ext a : 1
-- 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 : ℕ) ⋯
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, ⋯⟩))
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) ⟨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, ⋯⟩))
⊢ 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))

Tactic:
fin_cases a