awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
inst : X.IsStrictSegal
d : ℕ
hd : ⦋d + 1⦌.len ≤ n + 1
x y : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋d + 1⦌ hd))
h :
  ∀ (i : Fin (d + 1)),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hd))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋d + 1⦌, property := hd }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hd))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋d + 1⦌, property := hd }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
          y :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
h₁ : ∀ (i : Fin (d + 1)), (X.spine (d + 1) hd x).arrow i = (X.spine (d + 1) hd y).arrow i
⊢ X.spine (d + 1) hd x = X.spine (d + 1) hd y

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
inst : X.IsStrictSegal
d : ℕ
hd : ⦋d + 1⦌.len ≤ n + 1
x y : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋d + 1⦌ hd))
h :
  ∀ (i : Fin (d + 1)),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hd))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋d + 1⦌, property := hd }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hd))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋d + 1⦌, property := hd }))) →
              (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
          y :
        (fun (X : Type u) ↦ X)
          (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
i : Fin (d + 1)
⊢ (X.spine (d + 1) hd x).arrow i = (X.spine (d + 1) hd y).arrow i

Tactic:
apply h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
w :
  ∀ (m : SimplexCategory) (hm : m.len ≤ n + 1)
    (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
        x
⊢ f = g

Tactic:
ext ⟨⟨m, hm⟩⟩ x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
m : SimplexCategory
hm : m.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))
w :
  ∀ (m : ℕ) (hm : ⦋m⦌.len ≤ n + 1)
    (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
        x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) m hm))))
      x

Tactic:
induction m using SimplexCategory.rec with | _ m
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
m : ℕ
hm : ⦋m⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))
w :
  ∀ (hm : ⦋0⦌.len ≤ n + 1)
    (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
        x
w₁ :
  ∀ (m : ℕ) (hm : ⦋m + 1⦌.len ≤ n + 1)
    (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
        x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ hm))))
      x

Tactic:
obtain _ | m := m
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
hm : ⦋0⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))
⊢ SimplexCategory.δ (Fin.castSucc 0) ≫ SimplexCategory.σ 0 = 𝟙 ⦋0⦌

Tactic:
have fac := δ_comp_σ_self (i := (0 : Fin 1))
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
hm : ⦋0⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))
fac : SimplexCategory.δ 0 ≫ SimplexCategory.σ 0 = 𝟙 ⦋0⦌
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ hm))))
      x

Tactic:
simpa [← NatTrans.naturality_apply,
      ← Functor.map_comp_apply, ← op_comp,
      ← SimplexCategory.Truncated.Hom.tr_comp, fac] using
      congr_arg (Y.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0)).op)
        (h (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.σ 0)).op x))

Premises used: CategoryTheory.op_comp, CategoryTheory.NatTrans.naturality_apply, SimplexCategory.Truncated.Hom.tr_comp, SimplexCategory.Truncated.Hom.tr, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, SimplexCategory.δ, SimplexCategory.σ, CategoryTheory.Functor.map_comp_apply, CategoryTheory.Functor.map, congr_arg, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))
i : Fin (m + 1)
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hm))) :
          (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋m + 1⦌, property := hm }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
          x) :
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ hm))) :
          (a : (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋m + 1⦌, property := hm }))) →
            (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (g.app
              (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
          x) :
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))

Tactic:
simp [← NatTrans.naturality_apply, h]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X Y : Truncated (n + 1)
inst : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ }))) →
              (fun (X : Type u) ↦ X) (Y.obj (op { obj := ⦋1⦌, property := ⋯ })))
          x :
        (fun (X : Type u) ↦ X)
          (Y.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋1⦌ ⋯))))
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (g.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m + 1⦌ hm))))
      x

Tactic:
exact IsStrictSegal.ext (fun i ↦ by simp [← NatTrans.naturality_apply, h])

Premises used: SSet.Truncated.IsStrictSegal.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
⊢ X.spine m h (sx.spineToSimplex m h f) = f

Tactic:
congr_fun (sx.spine_spineToSimplex m h) f

Premises used: SSet.Truncated.StrictSegal.spine_spineToSimplex, SSet.Truncated.spine, congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ h))
⊢ sx.spineToSimplex m h (X.spine m h Δ) = Δ

Tactic:
congr_fun (sx.spineToSimplex_spine m h) Δ

Premises used: SSet.Truncated.StrictSegal.spineToSimplex_spine, congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
⊢ Function.Injective (α :=
    X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋m⦌ h))) (β :=
    X.Path m) (⇑(sx.spineEquiv m h) : (a : X.obj (op { obj := ⦋m⦌, property := h })) → X.Path m)

Tactic:
Equiv.injective _

Premises used: Equiv.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
rw : (X.spine m h (sx.spineToSimplex m h f)).vertex i = f.vertex i
rw₁ rw₂ : f.vertex i = f.vertex i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (⦋0⦌.const ⦋m⦌ i) ⋯ h))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
      (sx.spineToSimplex m h f) =
    f.vertex i

Tactic:
rw [← spine_vertex, spine_spineToSimplex_apply]

Premises used: SSet.Truncated.spine_vertex, SSet.Truncated.StrictSegal.spine_spineToSimplex_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
rw : (X.spine m h (sx.spineToSimplex m h f)).arrow i = f.arrow i
rw₁ rw₂ : f.arrow i = f.arrow i
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (mkOfSucc i) ⋯ h))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋1⦌, property := ⋯ })))
      (sx.spineToSimplex m h f) =
    f.arrow i

Tactic:
rw [← spine_arrow, spine_spineToSimplex_apply]

Premises used: SSet.Truncated.spine_arrow, SSet.Truncated.StrictSegal.spine_spineToSimplex_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
Goal:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
a :
  Eq (α := X.Path l)
    ((sx.spineEquiv l ⋯ : (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.Path l)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) ⋯ h).op) :
              (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
                (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋l⦌, property := ⋯ })))
            (sx.spineToSimplex m h f) :
          (fun (X : Type u) ↦ X)
            (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋l⦌ ⋯)))) :
      X.Path l)
    ((sx.spineEquiv l ⋯ : (a : X.obj (op { obj := ⦋l⦌, property := ⋯ })) → X.Path l)
        (sx.spineToSimplex l ⋯ (f.interval j l hjl)) :
      X.Path l)
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋l⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (tr (subinterval j l hjl) ⋯ h).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋m⦌, property := h }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋l⦌, property := ⋯ })))
        (sx.spineToSimplex m h f) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋l⦌ ⋯))))
    (sx.spineToSimplex l ⋯ (f.interval j l hjl) :
      X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋l⦌ ⋯)))

Tactic:
apply sx.spineInjective l

Premises used: SSet.Truncated.StrictSegal.spineInjective