awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (goal)
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
⊢ ∀ (x : (↑((nerve T).nonDegenerate n) : Type u_1)),
    Mono.{u_1, u_1 + 1} (C := SSet) (X := Δ[n]) (Y := nerve T)
      ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) (↑x : nerve T _⦋n⦌))
have this : ∀ (x : nerve T _⦋n⦌) (hx : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x),
  Mono.{u_1, u_1 + 1} (C := SSet) (X := Δ[n]) (Y := nerve T)
    ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T)
      (↑(Subtype.mk (p := fun (x : nerve T _⦋n⦌) ↦
            Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x) x hx) :
        nerve T _⦋n⦌))
Tactic: ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (hypothesis)
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x
⊢ Mono.{u_1, u_1 + 1} (C := SSet) (X := Δ[n]) (Y := nerve T)
    ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T)
      (↑(Subtype.mk (p := fun (x : nerve T _⦋n⦌) ↦
            Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x) x hx) :
        nerve T _⦋n⦌))
have hx₁ : Function.Injective x.obj
Tactic: rw [PartialOrder.mem_nerve_nonDegenerate_iff_injective] at hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (goal)
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
⊢ Mono.{u_1, u_1 + 1} (C := SSet) (X := Δ[n]) (Y := nerve T)
    ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T)
      (↑(Subtype.mk (p := fun (x : nerve T _⦋n⦌) ↦
            Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x) x hx_1) :
        nerve T _⦋n⦌))
have simp : ∀ (k : SimplexCategoryᵒᵖ),
  Function.Injective (α := Δ[n].obj k) (β := (nerve T).obj k)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) k)) :
      (a : Δ[n].obj k) → (nerve T).obj k)
Tactic: simp only [NatTrans.mono_iff_mono_app, mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (goal)
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⦌)
⊢ i = j
have h : ∀ (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: ext l : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (hypothesis)
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)
⊢ 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⦌))
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (hypothesis)
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)
⊢ 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⦌))
have 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⦌))
Tactic: have : X.δ i x = (yonedaEquiv.symm x).app _
    (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) := rfl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (goal)
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⦌))
⊢ 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⦌))
have rw : Mono (SimplexCategory.δ i)
Tactic: rw [this, nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (goal)
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⦌))
⊢ i = j
have a : SimplexCategory.δ i = SimplexCategory.δ j
Tactic: apply SimplexCategory.δ_injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (goal)
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⦌))
⊢ SimplexCategory.δ i = SimplexCategory.δ j
have 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⦌)
Tactic: apply stdSimplex.objEquiv.symm.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular (hypothesis)
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⦌))
⊢ 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⦌)
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
⊢ f = g
have hᵥ : ∀ (j : Fin (m + 1 + 1)), f.vertex j = g.vertex j
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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)
⊢ f.vertex j = g.vertex j
have hᵥ : ∀ (k : Fin (m + 1)) (hk : j = k.castSucc), f.vertex j = g.vertex j
Tactic: rcases Fin.eq_castSucc_or_eq_last j with ⟨k, hk⟩ | hl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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
⊢ f.vertex j = g.vertex j
have hᵥ₁ : ∀ (hl : j = Fin.last (m + 1)), f.vertex j = g.vertex j
Tactic: rcases Fin.eq_castSucc_or_eq_last j with ⟨k, hk⟩ | hl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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
⊢ f.vertex j = g.vertex j
have hᵥ : f.vertex k.castSucc = g.vertex k.castSucc
Tactic: rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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
⊢ f.vertex j = g.vertex j
have hᵥ₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) sorry sorry))) :
      (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
        (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
    (f.arrow k) =
  g.vertex k.castSucc
Tactic: rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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
⊢ f.vertex j = g.vertex j
have hᵥ₂ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (f.arrow k) :
    (fun (X : Type u) ↦ X)
      (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (g.arrow k) :
    (fun (X : Type u) ↦ X)
      (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry))))
Tactic: rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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⦌ ⋯))))
⊢ f.vertex j = g.vertex j
have hᵥ₃ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (g.arrow k) :
    (fun (X : Type u) ↦ X)
      (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 1) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (g.arrow k) :
    (fun (X : Type u) ↦ X)
      (X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry))))
Tactic: rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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)
⊢ f.vertex j = g.vertex j
have hᵥ : f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ
Tactic: simp only [hl, ← Fin.succ_last]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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)
⊢ f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ
have hᵥ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) sorry sorry))) :
      (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
        (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
    (f.arrow (Fin.last m)) =
  g.vertex (Fin.last m).succ
Tactic: rw [← f.arrow_tgt (Fin.last m), ← g.arrow_tgt (Fin.last m), h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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
⊢ f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ
have hᵥ₁ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (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⦌ sorry))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (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⦌ sorry))))
Tactic: rw [← f.arrow_tgt (Fin.last m), ← g.arrow_tgt (Fin.last m), h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
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⦌ ⋯))))
⊢ f.vertex (Fin.last m).succ = g.vertex (Fin.last m).succ
have hᵥ₂ : Eq (α := X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n + 1) ⦋0⦌ sorry)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (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⦌ sorry))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (tr (SimplexCategory.δ 0) sorry sorry))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0 + 1⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (op { obj := ⦋0⦌, property := sorry })))
      (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⦌ sorry))))
Tactic: rw [← f.arrow_tgt (Fin.last m), ← g.arrow_tgt (Fin.last m), h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Path (goal)
Goal:
n_1 : ℕ
X_1 : Truncated (n_1 + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Functor.obj (trunc (n + 1) 1 ⋯) X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
        (a :
            (fun (X : Type u) ↦ X)
              (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
          (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 ⋯).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.castSucc
have 0 : (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((Functor.obj (trunc (n + 1) 1 sorry) X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op) :
      (a :
          (fun (X : Type u) ↦ X)
            (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0 + 1⦌, property := Path₁._proof_5 }))) →
        (fun (X : Type u) ↦ X) (((trunc (n + 1) 1 sorry).obj X).obj (op { obj := ⦋0⦌, property := Path₁._proof_1 })))
    (![p.arrow 0, q.arrow 0] ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1)))) =
  ![p.vertex 0, p.vertex 1, q.vertex 1] (Fin.castSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1))))
Tactic: fin_cases i
Cleared hypotheses: i