awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx_1 : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  Eq (α := nerve T _⦋k⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) (Opposite.op ⦋k⦌)) :
          (a : Δ[n] _⦋k⦌) → nerve T _⦋k⦌)
        i :
      nerve T _⦋k⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) (Opposite.op ⦋k⦌)) :
          (a : Δ[n] _⦋k⦌) → nerve T _⦋k⦌)
        j :
      nerve T _⦋k⦌)
l : Fin (k + 1)
⊢ Eq (α := Fin (n + 1)) ((i : (a : Fin (k + 1)) → Fin (n + 1)) l : Fin (n + 1))
    ((j : (a : Fin (k + 1)) → Fin (n + 1)) l : Fin (n + 1))

Tactic:
exact hx (Functor.congr_obj hij l)

Premises used: CategoryTheory.Functor.congr_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
n : SimplexCategory
⊢ Nonsingular.{u} (stdSimplex.obj n)

Tactic:
Nonsingular.of_iso (stdSimplex.isoNerve _).symm

Premises used: CategoryTheory.Iso.symm, SSet.stdSimplex.isoNerve, SSet.Nonsingular.of_iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
n m : SimplexCategory
⊢ Nonsingular.{u} (tensorObj (𝒞 := Functor.category) (stdSimplex.obj n) (stdSimplex.obj m))

Tactic:
Nonsingular.of_iso (prodStdSimplex.isoNerve _ _).symm

Premises used: SSet.prodStdSimplex.isoNerve, CategoryTheory.Iso.symm, SSet.Nonsingular.of_iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i : Fin (n + 2)
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n + 1]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x)

Tactic:
have := Nonsingular.mono' x hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i : Fin (n + 2)
this :
  Mono.{u, u + 1} (C := SSet) (X := Δ[n + 1]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x) (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[n + 1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
            (SimplexCategory.δ i) :
          Δ[n + 1] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))

Tactic:
have : X.δ i x = (yonedaEquiv.symm x).app _
    (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) := rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i : Fin (n + 2)
this_1 :
  Mono.{u, u + 1} (C := SSet) (X := Δ[n + 1]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x)
this :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x) (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[n + 1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
            (SimplexCategory.δ i) :
          Δ[n + 1] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
rw : Mono (SimplexCategory.δ i)
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (X _⦋n⦌)) (X.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))

Tactic:
rw [this, nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, SSet.nonDegenerate_iff_of_mono, SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i : Fin (n + 2)
this_1 :
  Mono.{u, u + 1} (C := SSet) (X := Δ[n + 1]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x)
this :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x) (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[n + 1] _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
            (SimplexCategory.δ i) :
          Δ[n + 1] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ Mono (SimplexCategory.δ i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i j : Fin (n + 2)
hij :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
a : SimplexCategory.δ i = SimplexCategory.δ j
⊢ i = j

Tactic:
apply SimplexCategory.δ_injective

Premises used: SimplexCategory.δ_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i j : Fin (n + 2)
hij :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
a :
  Eq.{u + 1} (α := Δ[n + 1] _⦋n⦌)
    ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
        (SimplexCategory.δ i) :
      Δ[n + 1] _⦋n⦌)
    ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
        (SimplexCategory.δ j) :
      Δ[n + 1] _⦋n⦌)
⊢ SimplexCategory.δ i = SimplexCategory.δ j

Tactic:
apply stdSimplex.objEquiv.symm.injective

Premises used: Equiv.injective, Equiv.symm, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i j : Fin (n + 2)
hij :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n + 1]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x)

Tactic:
have := mono' x hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i j : Fin (n + 2)
hij :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
this :
  Mono.{u, u + 1} (C := SSet) (X := Δ[n + 1]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x)
⊢ Eq.{u + 1} (α := Δ[n + 1] _⦋n⦌)
    ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
        (SimplexCategory.δ i) :
      Δ[n + 1] _⦋n⦌)
    ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
        (SimplexCategory.δ j) :
      Δ[n + 1] _⦋n⦌)

Tactic:
injective_of_mono ((yonedaEquiv.symm x).app _) hij

Premises used: SSet.yonedaEquiv, Equiv.symm, CategoryTheory.injective_of_mono, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
i j : Fin (n + 2)
hij :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
this :
  Mono.{u, u + 1} (C := SSet) (X := Δ[n + 1]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x)
⊢ Eq.{u + 1} (α := Δ[n + 1] _⦋n⦌)
    ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
        (SimplexCategory.δ i) :
      Δ[n + 1] _⦋n⦌)
    ((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌)
        (SimplexCategory.δ j) :
      Δ[n + 1] _⦋n⦌)

Tactic:
exact injective_of_mono ((yonedaEquiv.symm x).app _) hij

Premises used: SSet.yonedaEquiv, Equiv.symm, CategoryTheory.injective_of_mono, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Op
Goal:
X Y : SSet
f : X ⟶ Y
n : SimplexCategoryᵒᵖ
x : X.op.obj n
⊢ Eq (α := (fun (X : Type u) ↦ X) ((opFunctor.obj Y).obj n))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((opFunctor.map f).app n) :
          (a : (fun (X : Type u) ↦ X) ((opFunctor.obj X).obj n)) → (fun (X : Type u) ↦ X) ((opFunctor.obj Y).obj n))
        x :
      (fun (X : Type u) ↦ X) ((opFunctor.obj Y).obj n))
    ((Equiv.symm opObjEquiv : (a : Y.obj n) → Y.op.obj n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app n) :
              (a : (fun (X : Type u) ↦ X) (X.obj n)) → (fun (X : Type u) ↦ X) (Y.obj n))
            ((opObjEquiv : (a : X.op.obj n) → X.obj n) x : X.obj n) :
          (fun (X : Type u) ↦ X) (Y.obj n)) :
      Y.op.obj n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Op
Goal:
X : SSet
n m : SimplexCategoryᵒᵖ
f : n ⟶ m
x : X.op.obj n
⊢ Eq (α := (fun (X : Type u) ↦ X) (X.op.obj m))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f) :
          (a : (fun (X : Type u) ↦ X) (X.op.obj n)) → (fun (X : Type u) ↦ X) (X.op.obj m))
        x :
      (fun (X : Type u) ↦ X) (X.op.obj m))
    ((Equiv.symm opObjEquiv :
          (a : X.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop m)))) →
            X.op.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop m))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.rev.map f.unop).op) :
              (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop n))))) →
                (fun (X : Type u) ↦ X) (X.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop m)))))
            ((opObjEquiv :
                  (a : X.op.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop n)))) →
                    X.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop n))))
                x :
              X.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop n)))) :
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop m))))) :
      X.op.obj (Opposite.op (SimplexCategory.rev.obj (Opposite.unop m))))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Op
Goal:
X : SSet
n : ℕ
i : Fin (n + 2)
x : X _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u) ↦ X) (X.op _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) :
          (a : (fun (X : Type u) ↦ X) (X.op _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X.op _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (X.op _⦋n⦌))
    ((Equiv.symm opObjEquiv : (a : X _⦋n⦌) → X.op _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i.rev) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            ((opObjEquiv : (a : X.op _⦋n + 1⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) :
          (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
      X.op _⦋n⦌)

Tactic:
simp [SimplicialObject.δ, op_map]

Premises used: SSet.op_map, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Op
Goal:
X : SSet
n : ℕ
i : Fin (n + 1)
x : X _⦋n⦌
⊢ Eq (α := (fun (X : Type u) ↦ X) (X.op _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X.op i) :
          (a : (fun (X : Type u) ↦ X) (X.op _⦋n⦌)) → (fun (X : Type u) ↦ X) (X.op _⦋n + 1⦌))
        x :
      (fun (X : Type u) ↦ X) (X.op _⦋n + 1⦌))
    ((Equiv.symm opObjEquiv : (a : X _⦋n + 1⦌) → X.op _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i.rev) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
            ((opObjEquiv : (a : X.op _⦋n⦌) → X _⦋n⦌) x : X _⦋n⦌) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) :
      X.op _⦋n + 1⦌)

Tactic:
simp [SimplicialObject.σ, op_map]

Premises used: SSet.op_map, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f : X.Path m
i : Fin m
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
      (f.arrow i) =
    f.vertex i.castSucc

Tactic:
Path₁.arrow_src f i

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, CategoryTheory.ObjectProperty.homMk, OrderEmbedding.toOrderHom, SSet.Truncated.Path₁.arrow_src, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path m
hᵥ : f.vertex = g.vertex
hₐ : f.arrow = g.arrow
⊢ f = g

Tactic:
Path₁.ext hᵥ hₐ

Premises used: SSet.Truncated.Path₁.ext, SSet.Truncated.Path
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
hᵥ : ∀ (j : Fin (m + 1 + 1)), f.vertex j = g.vertex j
hₐ : ∀ (j : Fin (m + 1)), f.arrow j = g.arrow j
⊢ f = g

Tactic:
ext j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hᵥ : ∀ (k : Fin (m + 1)) (hk : j = k.castSucc), f.vertex j = g.vertex j
hᵥ₁ : ∀ (hl : j = Fin.last (m + 1)), f.vertex j = g.vertex j
⊢ f.vertex j = g.vertex j

Tactic:
rcases Fin.eq_castSucc_or_eq_last j with ⟨k, hk⟩ | hl

Premises used: Fin.eq_castSucc_or_eq_last
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
hᵥ : f.vertex k.castSucc = g.vertex k.castSucc
hᵥ₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
      (f.arrow k) =
    g.vertex k.castSucc
hᵥ₂ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (f.arrow k) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (g.arrow k) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
hᵥ₃ hᵥ₄ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (g.arrow k) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (g.arrow k) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
⊢ f.vertex j = g.vertex j

Tactic:
rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]

Premises used: SSet.Truncated.Path.arrow_src
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
hᵥ : f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ
⊢ f.vertex j = g.vertex j

Tactic:
simp only [hl, ← Fin.succ_last]

Premises used: Fin.succ_last
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
hᵥ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
      (f.arrow (Fin.last m)) =
    g.vertex (Fin.last m).succ
hᵥ₁ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (f.arrow (Fin.last m)) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (g.arrow (Fin.last m)) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
hᵥ₂ hᵥ₃ :
  Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (g.arrow (Fin.last m)) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) ⋯ ⋯))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := ⋯ })))
        (g.arrow (Fin.last m)) :
      (fun (X : Type u) ↦ X)
        (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ ⋯))))
⊢ f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ

Tactic:
rw [← f.arrow_tgt (Fin.last m), ← g.arrow_tgt (Fin.last m), h]

Premises used: Fin.last, SSet.Truncated.Path.arrow_tgt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1)
⊢ f.arrow j = g.arrow j

Tactic:
h j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Path
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1)
⊢ f.arrow j = g.arrow j

Tactic:
exact h j