awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Splitting (goal)
Goal:
X : SSet
x : SimplexCategoryᵒᵖ
n : ℕ
⊢ Functor.CoconeTypes.IsColimit (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
    Discrete.functor
      (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
    (Cofan.cofanTypes (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
        (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
have refine_1 : ∀
  (x :
    Functor.CoconeTypes.pt (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
      Discrete.functor
        (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
      (Cofan.cofanTypes (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
          (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))),
  ∃ (i : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)) (y :
    SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌) i),
    CofanTypes.inj (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (Cofan.cofanTypes (F :=
          SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
          (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
            (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
        i y =
      x
Tactic: refine CofanTypes.isColimit_mk _ (fun x ↦ ?_) (fun ⟨⟨⟨m⟩⟩, f, _⟩ x y h ↦ ?_)
      (fun ⟨⟨⟨m⟩⟩, f, _⟩ ⟨⟨⟨p⟩⟩, g, _⟩ x y h ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Splitting (goal)
Goal:
X : SSet
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x :
  Functor.CoconeTypes.pt (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
    Discrete.functor
      (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
    (Cofan.cofanTypes (F :=
      SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
      (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
        (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
⊢ ∃ (i : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)) (y :
    SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌) i),
    CofanTypes.inj (F :=
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
        (Cofan.cofanTypes (F :=
          SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
          (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
            (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
        i y =
      x
have refine_1 : ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌),
  Epi f →
    ∀ (y : (↑(X.nonDegenerate m) : Type u)),
      ∃ (i : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)) (y_1 :
        SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌) i),
        Eq (α :=
          Functor.CoconeTypes.pt (J := Discrete (SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌))) (F :=
            Discrete.functor
              (SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌)))
            (Cofan.cofanTypes (F :=
              SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
              (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
                (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌))))
          (CofanTypes.inj (F :=
            SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
            (Cofan.cofanTypes (F :=
              SimplicialObject.Splitting.summand (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) (Opposite.op ⦋n⦌))
              (SimplicialObject.Splitting.cofan' (fun (n : ℕ) ↦ (↑(X.nonDegenerate n) : Type u)) X
                (fun (n : ℕ) ↦ ↾Subtype.val (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)) (Opposite.op ⦋n⦌)))
            i y_1)
          ((ConcreteCategory.hom (FC := Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            (↑y : X _⦋m⦌))
Tactic: obtain ⟨m, f, _, y, rfl⟩ := X.exists_nonDegenerate x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n i : ℕ
x x_1 : Δ[n] _⦋i⦌
h :
  Eq (α := (a : Fin (i + 1)) → Fin (n + 1))
    ((fun (x : Δ[n] _⦋i⦌) (j : Fin (i + 1)) ↦
        ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
              (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
            j :
          Fin (⦋n⦌.len + 1)))
      x)
    ((fun (x : Δ[n] _⦋i⦌) (j : Fin (i + 1)) ↦
        ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
              (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
            j :
          Fin (⦋n⦌.len + 1)))
      x_1)
⊢ Eq (α := unop (op ⦋i⦌) ⟶ ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x : unop (op ⦋i⦌) ⟶ ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x_1 : unop (op ⦋i⦌) ⟶ ⦋n⦌)
have a : ∀ (x_2 : Fin ((unop (op ⦋i⦌)).len + 1)),
  Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x) :
          (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        x_2 :
      Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x_1) :
          (a : Fin ((unop (op ⦋i⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
        x_2 :
      Fin (⦋n⦌.len + 1))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
X : SSet
x : X _⦋0⦌
⊢ Eq (α := Δ[0] ⟶ X) ((Equiv.symm yonedaEquiv : (a : X _⦋0⦌) → Δ[0] ⟶ X) x : Δ[0] ⟶ X) (const x : Δ[0] ⟶ X)
have a : Eq (α := X _⦋0⦌)
  ((yonedaEquiv : (a : Δ[0] ⟶ X) → X _⦋0⦌) ((Equiv.symm yonedaEquiv : (a : X _⦋0⦌) → Δ[0] ⟶ X) x : Δ[0] ⟶ X) : X _⦋0⦌)
  ((yonedaEquiv : (a : Δ[0] ⟶ X) → X _⦋0⦌) (const x) : X _⦋0⦌)
Tactic: apply yonedaEquiv.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x : Δ[n] _⦋0⦌
⊢ (fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
      ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) =
    x
have h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
  Eq (α := Fin (n + 1))
    (((fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
            ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) :
          (a : Fin (0 + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    ((x : (a : Fin (0 + 1)) → Fin (n + 1)) i : Fin (n + 1))
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x : Δ[n] _⦋0⦌
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq (α := Fin (n + 1))
    (((fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
            ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) :
          (a : Fin (0 + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    ((x : (a : Fin (0 + 1)) → Fin (n + 1)) i : Fin (n + 1))
have h : Eq (α := Fin (n + 1))
  (((fun (i : Fin (n + 1)) ↦ (const n i (op ⦋0⦌) : Δ[n] _⦋0⦌))
        ((fun (x : Δ[n] _⦋0⦌) ↦ ((x : (a : Fin (0 + 1)) → Fin (n + 1)) 0 : Fin (n + 1))) x) :
      (a : Fin (0 + 1)) → Fin (n + 1))
    ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
  ((x : (a : Fin (0 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ Δ[n] _⦋1⦌
have refine : Monotone ![a, b]
Tactic: refine objMk ⟨![a, b], ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ Monotone ![a, b]
have rw : ∀ (i : Fin (unop (op ⦋1⦌)).len), ![a, b] i.castSucc ≤ ![a, b] i.succ
Tactic: rw [Fin.monotone_iff_le_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ ∀ (i : Fin (unop (op ⦋1⦌)).len), ![a, b] i.castSucc ≤ ![a, b] i.succ
have simp : ![a, b] (Fin.castSucc 0) ≤ ![a, b] (Fin.succ 0)
Tactic: simp only [unop_op, len_mk, Fin.forall_fin_one]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ Δ[n] _⦋2⦌
have refine : Monotone ![a, b, c]
Tactic: refine objMk ⟨![a, b, c], ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ Monotone ![a, b, c]
have rw : ∀ (i : Fin (unop (op ⦋2⦌)).len), ![a, b, c] i.castSucc ≤ ![a, b, c] i.succ
Tactic: rw [Fin.monotone_iff_le_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ ∀ (i : Fin (unop (op ⦋2⦌)).len), ![a, b, c] i.castSucc ≤ ![a, b, c] i.succ
have simp : ![a, b, c] (Fin.castSucc 0) ≤ ![a, b, c] (Fin.succ 0) ∧ ![a, b, c] (Fin.castSucc 1) ≤ ![a, b, c] (Fin.succ 1)
Tactic: simp only [unop_op, len_mk, Fin.forall_fin_two]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ ![a, b, c] (Fin.castSucc 0) ≤ ![a, b, c] (Fin.succ 0) ∧ ![a, b, c] (Fin.castSucc 1) ≤ ![a, b, c] (Fin.succ 1)
have dsimp : a ≤ b ∧ b ≤ c
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
⊢ Eq.{u + 1} (α := Δ[n].Subcomplex) (face ∅) ⊥
have obj : ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Δ[n].obj x),
  Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face ∅) x) x_1 ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊥ x) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
⊢ Eq.{u + 1} (α := Δ[n].Subcomplex) (face univ) ⊤
have obj : ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Δ[n].obj x),
  Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face univ) x) x_1 ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
⊢ Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face univ) x) x_1 ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x) x_1
have obj : Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (face univ) x) x_1
Tactic: simp only [Subfunctor.top_obj, Set.top_eq_univ, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ≤ face S₂ ↔ S₁ ≤ S₂
have refine : ∀ (h : face S₁ ≤ face S₂) (i : Fin (n + 1)) (hi : i ∈ S₁), i ∈ S₂
Tactic: refine ⟨fun h i hi ↦ ?_, fun h d a ha ↦ ha.trans h⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
h : face S₁ ≤ face S₂
i : Fin (n + 1)
hi : i ∈ S₁
⊢ i ∈ S₂
have simp : ∀
  (hi :
    Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₁).obj (op ⦋0⦌))
      ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)),
  Membership.mem (α := Δ[n] _⦋0⦌) (γ := Set (Δ[n] _⦋0⦌)) ((face S₂).obj (op ⦋0⦌))
    ((Equiv.symm obj₀Equiv : (a : Fin (n + 1)) → Δ[n] _⦋0⦌) i : Δ[n] _⦋0⦌)
Tactic: simp only [← obj₀Equiv_symm_mem_face_iff.{u}] at hi ⊢
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ face S =
    Subcomplex.ofSimplex
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))
have a : face S ≤
  Subcomplex.ofSimplex
    (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
a :
  face S ≤
    Subcomplex.ofSimplex
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))
⊢ face S =
    Subcomplex.ofSimplex
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))
have a₁ : Subcomplex.ofSimplex
    (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) ≤
  face S
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : SimplexCategory
x : Δ[n].obj (op k)
hx : Membership.mem (γ := Set (Δ[n].obj (op k))) ((face S).obj (op k)) x
⊢ Membership.mem (γ := Set (Δ[n].obj (op k)))
    ((Subcomplex.ofSimplex
          (objMk
            (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
      (op k))
    x
have a : ∀ (k : ℕ) ⦃x : Δ[n] _⦋k⦌⦄ (hx : Membership.mem (γ := Set (Δ[n] _⦋k⦌)) ((face S).obj (op ⦋k⦌)) x),
  Membership.mem (γ := Set (Δ[n] _⦋k⦌))
    ((Subcomplex.ofSimplex
          (objMk
            (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌))
    x
Tactic: induction k using SimplexCategory.rec with | _ k
Cleared hypotheses: k, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (hypothesis)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋k⦌)) ((face S).obj (op ⦋k⦌)) x
⊢ Membership.mem (γ := Set (Δ[n] _⦋k⦌))
    ((Subcomplex.ofSimplex
          (objMk
            (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌))
    x
have hx₁ : ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))
Tactic: rw [mem_face_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))
φ : Fin (k + 1) →o ↥S :=
  {
    toFun := fun (i : Fin (k + 1)) ↦
      Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (k + 1)) → Fin (n + 1)) i) ⋯,
    monotone' := ⋯ }
⊢ Membership.mem (γ := Set (Δ[n] _⦋k⦌))
    ((Subcomplex.ofSimplex
          (objMk
            (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌))
    x
have a : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))) :
      (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌))
    (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) =
  x
Tactic: refine ⟨Quiver.Hom.op
      (SimplexCategory.Hom.mk ((e.symm.toOrderEmbedding.toOrderHom.comp φ))), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), Membership.mem (α := Fin (n + 1)) S ((x : (a : Fin (k + 1)) → Fin (n + 1)) i : Fin (n + 1))
φ : Fin (k + 1) →o ↥S :=
  {
    toFun := fun (i : Fin (k + 1)) ↦
      Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (k + 1)) → Fin (n + 1)) i) ⋯,
    monotone' := ⋯ }
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))) :
        (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌))
      (objMk (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) =
    x
have a : ∀ (j : Fin (k + 1)),
  Eq (α := Fin (n + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Δ[n].map (Quiver.Hom.op (Hom.mk (e.symm.toOrderEmbedding.toOrderHom.comp φ)))) :
                (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌))
              (objMk
                (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S) e.toOrderEmbedding.toOrderHom)) :
            (fun (X : Type u) ↦ X) (Δ[n] _⦋k⦌)) :
          (a : Fin (k + 1)) → Fin (n + 1))
        j :
      Fin (n + 1))
    ((x : (a : Fin (k + 1)) → Fin (n + 1)) j : Fin (n + 1))
Tactic: ext j : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x_1 : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : Membership.mem (γ := Set (Δ[n].obj (op j))) ((face S).obj (op j)) x
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
⊢ LE.le (α := ↥S)
    (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S)
        ((Hom.toOrderHom
              (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → unop (op j) ⟶ ⦋n⦌) x) :
            (a : Fin ((unop (op j)).len + 1)) → Fin (⦋n⦌.len + 1))
          i₁)
        ⋯ :
      ↥S)
    (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S)
        ((Hom.toOrderHom
              (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → unop (op j) ⟶ ⦋n⦌) x) :
            (a : Fin ((unop (op j)).len + 1)) → Fin (⦋n⦌.len + 1))
          i₂)
        ⋯ :
      ↥S)
have simp : LE.le (α := Fin (n + 1))
  ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
        (a : Fin (j.len + 1)) → Fin (n + 1))
      i₁ :
    Fin (n + 1))
  ((Hom.toOrderHom (((objEquiv : Δ[n].obj (op j) ≃ (unop (op j) ⟶ ⦋n⦌)) : (a : Δ[n].obj (op j)) → j ⟶ ⦋n⦌) x) :
        (a : Fin (j.len + 1)) → Fin (n + 1))
      i₂ :
    Fin (n + 1))
Tactic: simp only [Subtype.mk_le_mk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x_1 : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x
⊢ (fun (f : ⦋j⦌ ⟶ ⦋m⦌) ↦
        (Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
            (objMk
              (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))
            ⋯ :
          { x : Δ[n] _⦋j⦌ // Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x }))
      ((fun (x : (face S).toSSet _⦋j⦌) ↦
          (match (motive := (face S).toSSet _⦋j⦌ → (⦋j⦌ ⟶ ⦋m⦌)) x with
            | ⟨x, hx⟩ =>
              Hom.mk
                {
                  toFun := fun (i : Fin (⦋j⦌.len + 1)) ↦
                    (e.symm : (a : ↥S) → Fin (m + 1))
                      (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S)
                        ((Hom.toOrderHom
                              (((objEquiv : Δ[n] _⦋j⦌ ≃ (unop (op ⦋j⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋j⦌) → unop (op ⦋j⦌) ⟶ ⦋n⦌)
                                x) :
                            (a : Fin ((unop (op ⦋j⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
                          i)
                        ⋯),
                  monotone' := ⋯ } :
            ⦋j⦌ ⟶ ⦋m⦌))
        (Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x
          hx)) =
    Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx
have mk : Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
    (objMk
      (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
        (e.toOrderEmbedding.toOrderHom.comp
          {
            toFun := fun (i : Fin (j + 1)) ↦
              (e.symm : (a : ↥S) → Fin (m + 1))
                (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i) sorry),
            monotone' := sorry : Fin (j + 1) →o Fin (m + 1) })))
    sorry =
  Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex (goal)
Goal:
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : ℕ
x_1 : (face S).toSSet _⦋j⦌
x : Δ[n] _⦋j⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x
⊢ Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
      (objMk
        (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
          (e.toOrderEmbedding.toOrderHom.comp
            {
              toFun := fun (i : Fin (j + 1)) ↦
                (e.symm : (a : ↥S) → Fin (m + 1))
                  (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i) ⋯),
              monotone' := ⋯ : Fin (j + 1) →o Fin (m + 1) })))
      ⋯ =
    Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx
have mk : ∀ (i : Fin (j + 1)),
  Eq (α := Fin (n + 1))
    (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x)
                (objMk
                  (OrderHom.comp (OrderHom.Subtype.val fun (x : Fin (n + 1)) ↦ x ∈ S)
                    (e.toOrderEmbedding.toOrderHom.comp
                      {
                        toFun := fun (i : Fin (j + 1)) ↦
                          (e.symm : (a : ↥S) → Fin (m + 1))
                            (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ x ∈ S) ((x : (a : Fin (j + 1)) → Fin (n + 1)) i)
                              sorry),
                        monotone' := sorry : Fin (j + 1) →o Fin (m + 1) })))
                sorry) :
            Δ[n] _⦋j⦌) :
          (a : Fin (j + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    (((↑(Subtype.mk (p := fun (x : Δ[n] _⦋j⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋j⦌)) ((face S).obj (op ⦋j⦌)) x) x hx) :
            Δ[n] _⦋j⦌) :
          (a : Fin (j + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
Tactic: ext i : 2