awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.Basic (goal)
Goal:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
    ∃ (σ : S _⦋n + 2⦌),
      ∀ (j : Fin (n + 3)) (h : j ≠ i),
        Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
                (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              σ :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
                (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
              (horn.face i j h) :
            (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
            (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          σ :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Λ[n + 2, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
          (horn.face i j h) :
        (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Λ[n + 1 + 1, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        (horn.face i j hj) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Λ[n + 2, i].ι ≫ (Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ)
              (Opposite.op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Λ[n + 1 + 1, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
        (horn.face i j hj) :
      (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
have h₁ : Eq (α := (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S j) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1 + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      σ :
    (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Λ[n + 2, i].ι.app (Opposite.op ⦋n + 1⦌) ≫
            NatTrans.app ((Equiv.symm yonedaEquiv : (a : S _⦋n + 2⦌) → Δ[n + 2] ⟶ S) σ) (Opposite.op ⦋n + 1⦌)) :
        (a : (fun (X : Type u_1) ↦ X) (Λ[n + 1 + 1, i].toSSet _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
      (horn.face i j hj) :
    (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
Tactic: rw [← h j hj, NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions Λ[n, i].ι
have zero : ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h0 : 0 < i) (hn : i < Fin.last 0), innerHornInclusions Λ[0, i].ι
Tactic: obtain _ | _ | k := n
Cleared hypotheses: n, i, h0, hn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
zero : ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h0 : 0 < i) (hn : i < Fin.last 0), innerHornInclusions Λ[0, i].ι
⊢ innerHornInclusions Λ[n, i].ι
have succ : ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1)} (h0 : 0 < i) (hn : i < Fin.last (HAdd.hAdd (α := ℕ) 0 1)),
  innerHornInclusions Λ[HAdd.hAdd (α := ℕ) 0 1, i].ι
Tactic: obtain _ | _ | k := n
Cleared hypotheses: n, i, h0, hn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
zero : ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 1)} (h0 : 0 < i) (hn : i < Fin.last 0), innerHornInclusions Λ[0, i].ι
succ :
  ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1)} (h0 : 0 < i) (hn : i < Fin.last (HAdd.hAdd (α := ℕ) 0 1)),
    innerHornInclusions Λ[HAdd.hAdd (α := ℕ) 0 1, i].ι
⊢ innerHornInclusions Λ[n, i].ι
have succ₁ : ∀ (k : ℕ) {i : Fin (k + 1 + 1 + 1)} (h0 : 0 < i) (hn : i < Fin.last (k + 1 + 1)), innerHornInclusions Λ[k + 1 + 1, i].ι
Tactic: obtain _ | _ | k := n
Cleared hypotheses: n, i, h0, hn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
⊢ innerHornInclusions =
    ⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι
have h : ∀ ⦃X Y : SSet.{u}⦄ (f : X ⟶ Y),
  innerHornInclusions f ↔
    (⨆ (n : ℕ),
        ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Λ[n + 2, (↑p : Fin (n + 3))].toSSet) (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Δ[n + 2]) fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
      f
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
f : X ⟶ Y
⊢ innerHornInclusions f ↔
    (⨆ (n : ℕ),
        ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Λ[n + 2, (↑p : Fin (n + 3))].toSSet) (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Δ[n + 2]) fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
      f
have h : ∀ (h : innerHornInclusions f),
  (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
    f
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h :
  ∀ (h : innerHornInclusions f),
    (⨆ (n : ℕ),
        ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Λ[n + 2, (↑p : Fin (n + 3))].toSSet) (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Δ[n + 2]) fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
      f
⊢ innerHornInclusions f ↔
    (⨆ (n : ℕ),
        ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Λ[n + 2, (↑p : Fin (n + 3))].toSSet) (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Δ[n + 2]) fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
      f
have h₁ : ∀
  (h :
    (⨆ (n : ℕ),
        ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Λ[n + 2, (↑p : Fin (n + 3))].toSSet) (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦
          Δ[n + 2]) fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
      f),
  innerHornInclusions f
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h : innerHornInclusions f
⊢ (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
    f
have h₁ : ∀ ⦃X Y : SSet.{u}⦄ {n : ℕ} (i : Fin (n + 3)) (h0 : 0 < i) (hn : i < Fin.last (n + 2)),
  (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
    Λ[n + 2, i].ι
Tactic: obtain @⟨n, i, h0, hn⟩ := h
Cleared hypotheses: X, Y, f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 3)
h0 : 0 < i
hn : i < Fin.last (n + 2)
⊢ (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
    Λ[n + 2, i].ι
have h : ∃ (i_1 : ℕ) (a : Fin (i_1 + 3)), (0 < a ∧ a < Fin.last (i_1 + 2)) ∧ Arrow.mk Λ[n + 2, i].ι = Arrow.mk Λ[i_1 + 2, a].ι
Tactic: simp only [iSup_iff, ofHoms_iff, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 3)
h0 : 0 < i
hn : i < Fin.last (n + 2)
w : ℕ
w₁ : Fin (n + 3)
⊢ ∃ (i_1 : ℕ) (a : Fin (i_1 + 3)), (0 < a ∧ a < Fin.last (i_1 + 2)) ∧ Arrow.mk Λ[n + 2, i].ι = Arrow.mk Λ[i_1 + 2, a].ι
have h : (0 < i ∧ i < Fin.last (n + 2)) ∧ Arrow.mk Λ[n + 2, i].ι = Arrow.mk Λ[n + 2, i].ι
Tactic: use n, i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (hypothesis)
Goal:
X Y : SSet
f : X ⟶ Y
h :
  (⨆ (n : ℕ),
      ofHoms (X := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].toSSet)
        (Y := fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Δ[n + 2])
        fun (p : { p : Fin (n + 3) // 0 < p ∧ p < Fin.last (n + 2) }) ↦ Λ[n + 2, (↑p : Fin (n + 3))].ι)
    f
⊢ innerHornInclusions f
have h₁ : ∃ (i : ℕ) (i_1 : { p : Fin (i + 3) // 0 < p ∧ p < Fin.last (i + 2) }),
  Arrow.mk f = Arrow.mk Λ[i + 2, (↑i_1 : Fin (i + 3))].ι
Tactic: simp only [iSup_iff, ofHoms_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h :
  ∃ (i : ℕ) (i_1 : { p : Fin (i + 3) // 0 < p ∧ p < Fin.last (i + 2) }),
    Arrow.mk f = Arrow.mk Λ[i + 2, (↑i_1 : Fin (i + 3))].ι
⊢ innerHornInclusions f
have h₁ : ∀ (n : ℕ) (i : Fin (n + 3)) (h0 : 0 < i) (hn : i < Fin.last (n + 2)),
  innerHornInclusions
    Λ[n + 2, (↑(Subtype.mk (p := fun (p : Fin (n + 3)) ↦ 0 < p ∧ p < Fin.last (n + 2)) i sorry) : Fin (n + 3))].ι
Tactic: obtain ⟨n, ⟨i, h0, hn⟩, _, _⟩ := h
Cleared hypotheses: X, Y, f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
q : X ⟶ Y
inst : Y.Quasicategory
inst_1 : InnerFibration q
⊢ X.Quasicategory
have rw : InnerFibration (Y := ⊤_ SSet) (Limits.IsTerminal.from Limits.terminalIsTerminal X)
Tactic: rw [quasicategory_iff_from_innerFibration]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
q : X ⟶ Y
inst : Y.Quasicategory
inst_1 : InnerFibration q
rw : InnerFibration (Y := ⊤_ SSet) (Limits.IsTerminal.from Limits.terminalIsTerminal X)
X₁ : SSet
⊢ X.Quasicategory
have t : Limits.IsTerminal (⊤_ SSet)
Tactic: rw [quasicategory_iff_from_innerFibration]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.InnerFibration (goal)
Goal:
X Y : SSet
q : X ⟶ Y
inst : Y.Quasicategory
inst_1 : InnerFibration q
⊢ InnerFibration (Y := ⊤_ SSet) (Limits.IsTerminal.from Limits.terminalIsTerminal X)
have mem : innerFibrations (Y := ⊤_ SSet) (Limits.IsTerminal.from Limits.terminalIsTerminal X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
⊢ X.Quasicategory
have apply : ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ X) (_h0 : 0 < i) (_hn : i < Fin.last (n + 2)),
  ∃ (σ : X _⦋n + 2⦌),
    ∀ (j : Fin (n + 3)) (h : j ≠ i),
      Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
            σ :
          (fun (X : Type u) ↦ X) (X _⦋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 h) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
Tactic: apply quasicategory_of_filler X
-- 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)
⊢ ∃ (σ : X _⦋n + 2⦌),
    ∀ (j : Fin (n + 3)) (h : j ≠ i),
      Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
            σ :
          (fun (X : Type u) ↦ X) (X _⦋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 h) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
have h : ∀ (j : Fin (n + 3)) (h : j ≠ i),
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
    ((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 h) :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
Tactic: use sx.spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀
-- 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
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋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⦌))
    ((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⦌))
have h : 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: apply sx.spineInjective
-- 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
⊢ 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))
have 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)
Tactic: ext k
-- 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)
⊢ 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)
have 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⦌)
Tactic: dsimp only [spineEquiv, spine_arrow, Function.comp_apply, Equiv.coe_fn_mk]
-- 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)
⊢ 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⦌)
have 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⦌))
Tactic: rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
-- 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
⊢ 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 : ∀ (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⦌))
Tactic: obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by lia