awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
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
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⦌))
⊢ 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⦌))

Tactic:
rw [← h j hj, NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
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) (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:
rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S X : SSet
t : Limits.IsTerminal X
h : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (t.from S)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h0 : 0 < i
hn : i < Fin.last (n + 2)
this : HasLiftingProperty Λ[n + 2, i].ι (t.from S) := ⋯
⊢ σ₀ = Λ[n + 2, i].ι ≫ CommSq.lift (i := Λ[n + 2, i].ι) (g := t.from Δ[n + 2]) ⋯

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Basic
Goal:
S X : SSet
t : Limits.IsTerminal X
⊢ S.Quasicategory ↔ ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (t.from S)

Tactic:
⟨fun _ ↦ Quasicategory.hasLiftingProperty S t, quasicategory_of_hasLiftingProperty S t⟩

Premises used: SSet.quasicategory_of_hasLiftingProperty, Iff.intro, SSet.Quasicategory.hasLiftingProperty
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
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].ι
succ₁ :
  ∀ (k : ℕ) {i : Fin (k + 1 + 1 + 1)} (h0 : 0 < i) (hn : i < Fin.last (k + 1 + 1)),
    innerHornInclusions Λ[k + 1 + 1, i].ι
⊢ innerHornInclusions Λ[n, i].ι

Tactic:
obtain _ | _ | k := n
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
h0 : 0 < i
hn : i < Fin.last 0
⊢ innerHornInclusions Λ[0, i].ι

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
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:
grind
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
k : ℕ
i : Fin (k + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (k + 1 + 1)
⊢ innerHornInclusions Λ[k + 1 + 1, i].ι

Tactic:
⟨i, h0, hn⟩

Premises used: SSet.innerHornInclusions.intro
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
k : ℕ
i : Fin (k + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (k + 1 + 1)
⊢ innerHornInclusions Λ[k + 1 + 1, i].ι

Tactic:
exact ⟨i, h0, hn⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
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
⊢ 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))].ι

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
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
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
⊢ 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 ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
X Y : SSet
f : X ⟶ Y
h : innerHornInclusions f
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].ι
⊢ (⨆ (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:
obtain @⟨n, i, h0, hn⟩ := h
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 3)
h0 : 0 < i
hn : i < Fin.last (n + 2)
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].ι
⊢ (⨆ (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:
simp only [iSup_iff, ofHoms_iff, Subtype.exists, exists_prop]

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff, Subtype.exists, CategoryTheory.MorphismProperty.iSup_iff, exists_prop
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
X Y : SSet
n : ℕ
i : Fin (n + 3)
h0 : 0 < i
hn : i < Fin.last (n + 2)
w : ℕ
w₁ : Fin (n + 3)
h : (0 < i ∧ i < Fin.last (n + 2)) ∧ Arrow.mk Λ[n + 2, i].ι = Arrow.mk Λ[n + 2, i].ι
⊢ ∃ (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:
use n, i
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
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
⊢ ∃ (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

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff, CategoryTheory.MorphismProperty.iSup_iff
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
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))].ι
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 ⋯) : Fin (n + 3))].ι
⊢ innerHornInclusions f

Tactic:
obtain ⟨n, ⟨i, h0, hn⟩, _, _⟩ := h
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
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 ⋯) : Fin (n + 3))].ι

Tactic:
horn_ι_mem_innerHornInclusions h0 hn

Premises used: SSet.horn_ι_mem_innerHornInclusions
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
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 ⋯) : Fin (n + 3))].ι

Tactic:
exact horn_ι_mem_innerHornInclusions h0 hn

Premises used: SSet.horn_ι_mem_innerHornInclusions
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
⊢ innerHornInclusions ≤ modelCategoryQuillen.J

Tactic:
fun _ _ _ ⟨_, _, _⟩ ↦ modelCategoryQuillen.horn_ι_mem_J ..

Premises used: SSet.modelCategoryQuillen.J, SSet.modelCategoryQuillen.horn_ι_mem_J, _private.0.SSet.innerHornInclusions_le_J.match_1, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
⊢ innerHornInclusions ≤ monomorphisms SSet

Tactic:
innerHornInclusions_le_J.trans modelCategoryQuillen.J_le_monomorphisms

Premises used: SSet.innerHornInclusions_le_J, SSet.modelCategoryQuillen.J_le_monomorphisms, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
X Y : SSet
q : X ⟶ Y
inst : InnerFibration q
⊢ innerFibrations q

Tactic:
InnerFibration.mem

Premises used: SSet.InnerFibration.mem
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
S X : SSet
t : Limits.IsTerminal X
h : innerFibrations (t.from S)
⊢ S.Quasicategory

Tactic:
quasicategory_of_hasLiftingProperty S t (fun h0 hn ↦ h _ (horn_ι_mem_innerHornInclusions h0 hn))

Premises used: SSet.quasicategory_of_hasLiftingProperty, SSet.horn_ι_mem_innerHornInclusions, SSet.Subcomplex.ι, SSet.horn
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
S : SSet
inst : S.Quasicategory
X : SSet
t : Limits.IsTerminal X
⊢ innerFibrations (t.from S)

Tactic:
fun _ _ _ ⟨_, h0, hn⟩ ↦ hasLiftingProperty S t h0 hn

Premises used: CategoryTheory.HasLiftingProperty, CategoryTheory.Limits.IsTerminal.from, _private.0.SSet.innerHornInclusions_le_J.match_1, CategoryTheory.MorphismProperty.rlp, SSet.innerFibrations, SSet.Quasicategory.hasLiftingProperty
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
S X : SSet
t : Limits.IsTerminal X
⊢ S.Quasicategory ↔ InnerFibration (t.from S)

Tactic:
⟨fun _ ↦ ⟨Quasicategory.from_innerFibrations S t⟩,
    fun ⟨h⟩ ↦ quasicategory_of_from_innerFibrations S t h⟩

Premises used: SSet.Quasicategory, SSet.quasicategory_of_from_innerFibrations, Iff.intro, SSet.InnerFibration.mk, _private.0.SSet.quasicategory_iff_from_innerFibration.match_1, SSet.Quasicategory.from_innerFibrations
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
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
t : Limits.IsTerminal (⊤_ SSet)
⊢ X.Quasicategory

Tactic:
rw [quasicategory_iff_from_innerFibration]

Premises used: SSet.quasicategory_iff_from_innerFibration
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
X Y : SSet
q : X ⟶ Y
inst : Y.Quasicategory
inst_1 : InnerFibration q
mem : innerFibrations (Y := ⊤_ SSet) (Limits.IsTerminal.from Limits.terminalIsTerminal X)
⊢ InnerFibration (Y := ⊤_ SSet) (Limits.IsTerminal.from Limits.terminalIsTerminal X)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
X Y : SSet
q : X ⟶ Y
inst : Y.Quasicategory
inst_1 : InnerFibration q
⊢ innerFibrations (Y := ⊤_ SSet) (q ≫ Limits.IsTerminal.from Limits.terminalIsTerminal Y)

Tactic:
comp_mem _ _ _ (mem_innerFibrations q) (Quasicategory.from_innerFibrations Y _)

Premises used: CategoryTheory.MorphismProperty.comp_mem, SSet.mem_innerFibrations, SSet.Quasicategory.from_innerFibrations
-- Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
Goal:
X Y : SSet
q : X ⟶ Y
inst : Y.Quasicategory
inst_1 : InnerFibration q
⊢ innerFibrations (Y := ⊤_ SSet) (q ≫ Limits.IsTerminal.from Limits.terminalIsTerminal Y)

Tactic:
exact comp_mem _ _ _ (mem_innerFibrations q) (Quasicategory.from_innerFibrations Y _)

Premises used: CategoryTheory.MorphismProperty.comp_mem, SSet.mem_innerFibrations, SSet.Quasicategory.from_innerFibrations
-- Module: Mathlib.AlgebraicTopology.Quasicategory.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
⊢ (nerve.{v, u} C).Quasicategory

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
Goal:
⊢ Bicategory.Strict QCat

Tactic:
CatEnrichedOrdinary.instStrict

Premises used: CategoryTheory.CatEnrichedOrdinary, CategoryTheory.CatEnrichedOrdinary.instStrict
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
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⦌))
⊢ X.Quasicategory

Tactic:
apply quasicategory_of_filler X

Premises used: SSet.quasicategory_of_filler
-- 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)
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⦌))
⊢ ∃ (σ : 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:
use sx.spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀

Premises used: SSet.Path.map, SSet.StrictSegal.spineToSimplex, SSet.horn.spineId
-- 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
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))
⊢ 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⦌))

Tactic:
apply sx.spineInjective

Premises used: SSet.StrictSegal.spineInjective