awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ) ⋯
hi :
  ((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)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := Opposite.unop (Opposite.op ⦋2⦌)) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)
                  ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (stdSimplex.δ j))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (Quiver.Hom.op (diag 2))) :
                (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑triangle : Δ[n + 1 + 2] _⦋2⦌) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc k).op) :
                (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (↑((yonedaEquiv :
                      (a : Δ[n + 1 + 1] ⟶ Λ[n + 1 + 1 + 1, i].toSSet) →
                        (↑(Λ[n + 1 + 1 + 1, i].obj (Opposite.op ⦋n + 1 + 1⦌)) : Type u))
                    (Subfunctor.lift (stdSimplex.δ j) ⋯)) :
                Δ[n + 1 + 2] _⦋n + 1 + 1⦌) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))

Tactic:
rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
        Quiver.Hom.unop_op, stdSimplex.map_apply, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, SSet.Subcomplex.yonedaEquiv_coe, SSet.stdSimplex.map_apply, CategoryTheory.Subfunctor.lift_ι
-- 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 : ℕ) ⋯
hi :
  ((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)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                  ((Equiv.symm stdSimplex.objEquiv :
                      (a : Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 1 + 1⦌) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (SimplexCategory.δ j))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                  ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (stdSimplex.map (SimplexCategory.δ j)))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))

Tactic:
rw [SSet.yonedaEquiv_map]

Premises used: SSet.yonedaEquiv_map
-- 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 : ℕ) ⋯
hi :
  ((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)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫ SimplexCategory.δ j) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                  ((Equiv.symm stdSimplex.objEquiv :
                      (a : Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 1 + 1⦌) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (SimplexCategory.δ j))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))

Tactic:
simp only [Equiv.apply_symm_apply, triangle]

Premises used: Equiv.apply_symm_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 : ℕ) ⋯
hi :
  ((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)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫ SimplexCategory.δ j) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))

Tactic:
rw [mkOfSucc_δ_eq heq]

Premises used: SimplexCategory.mkOfSucc_δ_eq
-- 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 : ℕ) ⋯
hi :
  ((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)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
h₁ :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))

Tactic:
fin_cases z
-- 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 : ℕ) ⋯
hi :
  ((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)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl
-- 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 : ℕ) ⋯
hi :
  ((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)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
inst : X.IsStrictSegal
⊢ X.Quasicategory

Tactic:
quasicategory <| ofIsStrictSegal X

Premises used: SSet.StrictSegal.quasicategory, SSet.StrictSegal.ofIsStrictSegal
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
⟨_, _, _, _, _, ?_, c.isPushout⟩

Premises used: CategoryTheory.MorphismProperty.pushouts, Exists.intro, HomotopicalAlgebra.AttachCells.isPushout
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
refine : coproducts.{w, v, u} (ofHoms g) c.m
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
refine ⟨_, _, _, _, _, ?_, c.isPushout⟩
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
x : Discrete c.ι
i : c.ι
⊢ Quiver.Hom.{v, u} (V := C)
    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) { as := i : Discrete c.ι })
    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) { as := i : Discrete c.ι })

Tactic:
exact g (c.π i)

Premises used: HomotopicalAlgebra.AttachCells.π
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
x : Discrete c.ι
i : c.ι
rw :
  Eq (α :=
    Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) { as := i : Discrete c.ι } ⟶ c.cofan₂.pt)
    (c.cofan₁.ι.app { as := i } ≫ c.m)
    (NatTrans.app
      (Cocone.ι
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun (x : Discrete c.ι) ↦
                match (motive :=
                  (x : Discrete c.ι) →
                    Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                      (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                  x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι })
      { as := i })
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) { as := i : Discrete c.ι } ⟶ c.cofan₂.pt)
    (c.cofan₁.ι.app { as := i } ≫ c.m)
    (c.cofan₁.ι.app { as := i : Discrete c.ι } ≫
      c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun (x : Discrete c.ι) ↦
                match (motive :=
                  (x : Discrete c.ι) →
                    Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                      (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                  x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι })

Tactic:
rw [IsColimit.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
x : Discrete c.ι
i : c.ι
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) { as := i : Discrete c.ι } ⟶ c.cofan₂.pt)
    (c.cofan₁.ι.app { as := i } ≫ c.m)
    (NatTrans.app
      (Cocone.ι
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun (x : Discrete c.ι) ↦
                match (motive :=
                  (x : Discrete c.ι) →
                    Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                      (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                  x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι })
      { as := i })

Tactic:
c.hm i

Premises used: CategoryTheory.Limits.Cofan.inj, HomotopicalAlgebra.AttachCells.hm
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
x : Discrete c.ι
i : c.ι
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) { as := i : Discrete c.ι } ⟶ c.cofan₂.pt)
    (c.cofan₁.ι.app { as := i } ≫ c.m)
    (NatTrans.app
      (Cocone.ι
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun (x : Discrete c.ι) ↦
                match (motive :=
                  (x : Discrete c.ι) →
                    Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                      (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                  x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι })
      { as := i })

Tactic:
exact c.hm i

Premises used: HomotopicalAlgebra.AttachCells.hm
-- Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
⊢ c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun (x : Discrete c.ι) ↦
              match (motive :=
                (x : Discrete c.ι) →
                  Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }

Tactic:
have : c.m = c.isColimit₁.desc
      (Cocone.mk _ (Discrete.natTrans (fun ⟨i⟩ ↦ by exact g (c.π i)) ≫ c.cofan₂.ι)) :=
    c.isColimit₁.hom_ext (fun ⟨i⟩ ↦ by rw [IsColimit.fac]; exact c.hm i)