awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal (goal)
Goal:
w x y z : AugmentedSimplexCategory
h₁ :
  w.inl x ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
                (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
            z ≫
          (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
            Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
              (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
    w.inl x ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
        (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
                (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
            z ≫
          Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
            Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))
⊢ (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
      Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
        (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
      Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))
have h₂ : w.inr x ≫
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
              (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
          z ≫
        (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
          Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
            (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
  w.inr x ≫
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inl y ≫
      (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
              (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inl
          z ≫
        Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
          Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
a b : SimplexCategory
f g : a ⟶ b
h : f = g
x : Fin (a.len + 1)
⊢ Eq (α := Fin (b.len + 1)) ((Hom.toOrderHom f : (a : Fin (a.len + 1)) → Fin (b.len + 1)) x : Fin (b.len + 1))
    ((Hom.toOrderHom g : (a : Fin (a.len + 1)) → Fin (b.len + 1)) x : Fin (b.len + 1))
have rw : Eq (α := Fin (b.len + 1)) ((Hom.toOrderHom g : (a : Fin (a.len + 1)) → Fin (b.len + 1)) x : Fin (b.len + 1))
  ((Hom.toOrderHom g : (a : Fin (a.len + 1)) → Fin (b.len + 1)) x : Fin (b.len + 1))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
⊢ Monotone (β := Fin (y.len + 1)) fun (x : Fin (x.len + 1)) ↦ i
have tauto : ∀ ⦃a b : Fin (x.len + 1)⦄,
  a ≤ b → LE.le (α := Fin (y.len + 1)) ((fun (x : Fin (x.len + 1)) ↦ i) a) ((fun (x : Fin (x.len + 1)) ↦ i) b)
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = CategoryStruct.comp (Y := ⦋0⦌) (n.const ⦋0⦌ 0) (⦋0⦌.const m i)
have rw : n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i) : (a : Fin (⦋0⦌.len + 1)) → Fin (m.len + 1)) 0)
Tactic: rw [const_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 :
  Eq (α := Fin (n.len + 1)) ((toOrderHom f : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) 0)
    ((toOrderHom g : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) 0)
⊢ f = g
have a : ∀ (i : Fin (⦋0⦌.len + 1)),
  (↑((toOrderHom f : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) i) : ℕ) =
    (↑((toOrderHom g : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) i) : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
⊢ f = ⦋0⦌.const n ((Hom.toOrderHom f : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) 0)
have a : ∀ (x : Fin (⦋0⦌.len + 1)),
  (↑((Hom.toOrderHom f : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const n ((Hom.toOrderHom f : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) 0)) :
            (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1))
          x) :
      ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : SimplexCategory
f : n ⟶ ⦋0⦌
⊢ f = n.const ⦋0⦌ 0
have a : ∀ (x : Fin (n.len + 1)),
  Eq (α := Fin (⦋0⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (n.len + 1)) → Fin (⦋0⦌.len + 1)) x : Fin (⦋0⦌.len + 1))
    ((Hom.toOrderHom (n.const ⦋0⦌ 0) : (a : Fin (n.len + 1)) → Fin (⦋0⦌.len + 1)) x : Fin (⦋0⦌.len + 1))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 :
  Eq (α := Fin (n.len + 1)) ((toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (n.len + 1)) 0)
    ((toOrderHom g : (a : Fin (⦋1⦌.len + 1)) → Fin (n.len + 1)) 0)
h1 :
  Eq (α := Fin (n.len + 1)) ((toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (n.len + 1)) 1)
    ((toOrderHom g : (a : Fin (⦋1⦌.len + 1)) → Fin (n.len + 1)) 1)
⊢ f = g
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  (↑((toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (n.len + 1)) i) : ℕ) =
    (↑((toOrderHom g : (a : Fin (⦋1⦌.len + 1)) → Fin (n.len + 1)) i) : ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 0
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌
have refine : f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
Tactic: refine .inl ⟨f.toOrderHom 0, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 0
⊢ f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)) :
          (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 1
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌
have refine : f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
Tactic: refine .inl ⟨f.toOrderHom 0, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 1
⊢ f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
have a : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom (⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)) :
          (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 1
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌
have h : f = 𝟙 ⦋1⦌
Tactic: right
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 1
⊢ f = 𝟙 ⦋1⦌
have h : ∀ (i : Fin (⦋1⦌.len + 1)),
  Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom (𝟙 ⦋1⦌) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))
Tactic: ext i : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 0
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌
have this : LE.le (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
  ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1)
Tactic: have := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1) 0
this :
  LE.le (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1)
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌
have this₁ : LE.le (α := Fin (⦋1⦌.len + 1)) 1 0
Tactic: rw [e0, e1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ Eq (α := ⦋0⦌ ⟶ ⦋n⦌) (⦋0⦌.const ⦋l⦌ i ≫ subinterval j l hjl) (⦋0⦌.const ⦋n⦌ ⟨j + (↑i : ℕ), ⋯⟩)
have rw : Eq (α := ⦋0⦌ ⟶ ⦋n⦌)
  (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom (subinterval j l hjl) : (a : Fin (⦋l⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i) : ⦋0⦌ ⟶ ⦋n⦌)
  (⦋0⦌.const ⦋n⦌ ⟨j + (↑i : ℕ), sorry⟩ : ⦋0⦌ ⟶ ⦋n⦌)
Tactic: rw [const_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ Eq (α := ⦋0⦌ ⟶ ⦋n⦌)
    (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom (subinterval j l hjl) : (a : Fin (⦋l⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i) : ⦋0⦌ ⟶ ⦋n⦌)
    (⦋0⦌.const ⦋n⦌ ⟨j + (↑i : ℕ), ⋯⟩ : ⦋0⦌ ⟶ ⦋n⦌)
have e_i : Eq (α := Fin (⦋n⦌.len + 1))
  ((Hom.toOrderHom (subinterval j l hjl) : (a : Fin (⦋l⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i : Fin (⦋n⦌.len + 1))
  (⟨j + (↑i : ℕ), sorry⟩ : Fin (⦋n⦌.len + 1))
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (subinterval j l hjl) : (a : Fin (⦋l⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i : Fin (⦋n⦌.len + 1))
    (⟨j + (↑i : ℕ), ⋯⟩ : Fin (⦋n⦌.len + 1))
have e_i : (↑((Hom.toOrderHom (subinterval j l hjl) : (a : Fin (⦋l⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i) : ℕ) =
  (↑(⟨j + (↑i : ℕ), sorry⟩ : Fin (⦋n⦌.len + 1)) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ (↑i : ℕ) + j = j + (↑i : ℕ)
have e_i : j + (↑i : ℕ) = j + (↑i : ℕ)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin l
⊢ mkHom
        {
          toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
            match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (l + 1)) x with
            | 0 => i.castSucc
            | 1 => i.succ,
          monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (l + 1) } ≫
      mkHom { toFun := fun (i : Fin (l + 1)) ↦ ⟨(↑i : ℕ) + j, ⋯⟩, monotone' := ⋯ } =
    mkHom
      {
        toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
          match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (n + 1)) x with
          | 0 => (⟨j + (↑i : ℕ), ⋯⟩ : Fin n).castSucc
          | 1 => (⟨j + (↑i : ℕ), ⋯⟩ : Fin n).succ,
        monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }
have a : ∀ (i_1 : Fin 2),
  (↑((Hom.toOrderHom
              (mkHom
                  {
                    toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                      match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (l + 1)) x with
                      | 0 => i.castSucc
                      | 1 => i.succ,
                    monotone' := sorry : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (l + 1) } ≫
                mkHom
                  { toFun := fun (i : Fin (l + 1)) ↦ (⟨(↑i : ℕ) + j, sorry⟩ : Fin (n + 1)), monotone' := sorry :
                    Fin (l + 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          i_1) :
      ℕ) =
    (↑((Hom.toOrderHom
              (mkHom
                {
                  toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                    match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (n + 1)) x with
                    | 0 => (⟨j + (↑i : ℕ), sorry⟩ : Fin n).castSucc
                    | 1 => (⟨j + (↑i : ℕ), sorry⟩ : Fin n).succ,
                  monotone' := sorry : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          i_1) :
      ℕ)
Tactic: ext (i : Fin 2)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i_1 : Fin l
i : Fin 2
⊢ (↑((Hom.toOrderHom
              (mkHom
                  {
                    toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                      match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (l + 1)) x with
                      | 0 => i_1.castSucc
                      | 1 => i_1.succ,
                    monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (l + 1) } ≫
                mkHom
                  { toFun := fun (i : Fin (l + 1)) ↦ (⟨(↑i : ℕ) + j, ⋯⟩ : Fin (n + 1)), monotone' := ⋯ :
                    Fin (l + 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          0) :
      ℕ) =
    (↑((Hom.toOrderHom
              (mkHom
                {
                  toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                    match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (n + 1)) x with
                    | 0 => (⟨j + (↑i_1 : ℕ), ⋯⟩ : Fin n).castSucc
                    | 1 => (⟨j + (↑i_1 : ℕ), ⋯⟩ : Fin n).succ,
                  monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          0) :
      ℕ)
have simp : (↑i_1 : ℕ) + j = j + (↑i_1 : ℕ)
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i_1 : Fin l
i : Fin 2
⊢ (↑((Hom.toOrderHom
              (mkHom
                  {
                    toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                      match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (l + 1)) x with
                      | 0 => i_1.castSucc
                      | 1 => i_1.succ,
                    monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (l + 1) } ≫
                mkHom
                  { toFun := fun (i : Fin (l + 1)) ↦ (⟨(↑i : ℕ) + j, ⋯⟩ : Fin (n + 1)), monotone' := ⋯ :
                    Fin (l + 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          1) :
      ℕ) =
    (↑((Hom.toOrderHom
              (mkHom
                {
                  toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                    match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (n + 1)) x with
                    | 0 => (⟨j + (↑i_1 : ℕ), ⋯⟩ : Fin n).castSucc
                    | 1 => (⟨j + (↑i_1 : ℕ), ⋯⟩ : Fin n).succ,
                  monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          1) :
      ℕ)
have simp : (↑i_1 : ℕ) + 1 + j = j + (↑i_1 : ℕ) + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
⊢ mkHom
        {
          toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
            match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (l + 1)) x with
            | 0 => 0
            | 1 => Fin.last l,
          monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (l + 1) } ≫
      mkHom { toFun := fun (i : Fin (l + 1)) ↦ ⟨(↑i : ℕ) + j, ⋯⟩, monotone' := ⋯ } =
    mkHom
      {
        toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
          match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (n + 1)) x with
          | 0 => (⟨j, ⋯⟩ : Fin (n + 1))
          | 1 => (⟨j + l, ⋯⟩ : Fin (n + 1)),
        monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }
have a : ∀ (i : Fin 2),
  (↑((Hom.toOrderHom
              (mkHom
                  {
                    toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                      match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (l + 1)) x with
                      | 0 => 0
                      | 1 => Fin.last l,
                    monotone' := sorry : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (l + 1) } ≫
                mkHom
                  { toFun := fun (i : Fin (l + 1)) ↦ (⟨(↑i : ℕ) + j, sorry⟩ : Fin (n + 1)), monotone' := sorry :
                    Fin (l + 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          i) :
      ℕ) =
    (↑((Hom.toOrderHom
              (mkHom
                {
                  toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                    match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (n + 1)) x with
                    | 0 => (⟨j, sorry⟩ : Fin (n + 1))
                    | 1 => (⟨j + l, sorry⟩ : Fin (n + 1)),
                  monotone' := sorry : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          i) :
      ℕ)
Tactic: ext (i : Fin 2)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ (↑((Hom.toOrderHom
              (mkHom
                  {
                    toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                      match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (l + 1)) x with
                      | 0 => 0
                      | 1 => Fin.last l,
                    monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (l + 1) } ≫
                mkHom
                  { toFun := fun (i : Fin (l + 1)) ↦ (⟨(↑i : ℕ) + j, ⋯⟩ : Fin (n + 1)), monotone' := ⋯ :
                    Fin (l + 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          1) :
      ℕ) =
    (↑((Hom.toOrderHom
              (mkHom
                {
                  toFun := fun (x : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                    match (motive := Fin (HAdd.hAdd (α := ℕ) 1 1) → Fin (n + 1)) x with
                    | 0 => (⟨j, ⋯⟩ : Fin (n + 1))
                    | 1 => (⟨j + l, ⋯⟩ : Fin (n + 1)),
                  monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          1) :
      ℕ)
have simp : l + j = j + l
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
Δ : SimplexCategory
f g : Δ ⟶ ⦋0⦌
⊢ f = g
have a : ∀ (x : Fin (Δ.len + 1)),
  Eq (α := Fin (⦋0⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (Δ.len + 1)) → Fin (⦋0⦌.len + 1)) x : Fin (⦋0⦌.len + 1))
    ((Hom.toOrderHom g : (a : Fin (Δ.len + 1)) → Fin (⦋0⦌.len + 1)) x : Fin (⦋0⦌.len + 1))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
x y : SimplexCategory
h : x = y
⊢ Hom.toOrderHom (eqToHom h) = OrderEmbedding.toOrderHom (OrderIso.toOrderEmbedding (Fin.castOrderIso ⋯))
have subst : Hom.toOrderHom (eqToHom sorry) = OrderEmbedding.toOrderHom (OrderIso.toOrderEmbedding (Fin.castOrderIso sorry))
Tactic: subst h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc
have a : ∀ (k : Fin (⦋n⦌.len + 1)),
  (↑((Hom.toOrderHom (δ i ≫ δ j.succ) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1 + 1⦌.len + 1)) k) : ℕ) =
    (↑((Hom.toOrderHom (δ j ≫ δ i.castSucc) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1 + 1⦌.len + 1)) k) : ℕ)
Tactic: ext k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (↑((Hom.toOrderHom (δ i ≫ δ j.succ) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1 + 1⦌.len + 1)) k) : ℕ) =
    (↑((Hom.toOrderHom (δ j ≫ δ i.castSucc) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1 + 1⦌.len + 1)) k) : ℕ)
have a : (↑(if (if k.castSucc < i then k.castSucc else k.succ).castSucc < j.succ then
        (if k.castSucc < i then k.castSucc else k.succ).castSucc
      else (if k.castSucc < i then k.castSucc else k.succ).succ) :
    ℕ) =
  (↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < i.castSucc then
        (if k.castSucc < j then k.castSucc else k.succ).castSucc
      else (if k.castSucc < j then k.castSucc else k.succ).succ) :
    ℕ)
Tactic: dsimp [δ, Fin.succAbove]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (↑(if (if k.castSucc < i then k.castSucc else k.succ).castSucc < j.succ then
          (if k.castSucc < i then k.castSucc else k.succ).castSucc
        else (if k.castSucc < i then k.castSucc else k.succ).succ) :
      ℕ) =
    (↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < i.castSucc then
          (if k.castSucc < j then k.castSucc else k.succ).castSucc
        else (if k.castSucc < j then k.castSucc else k.succ).succ) :
      ℕ)
have a : ∀ (i : ℕ) (isLt : i < n + 2) (H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ j),
  (↑(if (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc < j.succ then
          (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc
        else (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).succ) :
      ℕ) =
    (↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if k.castSucc < j then k.castSucc else k.succ).castSucc
        else (if k.castSucc < j then k.castSucc else k.succ).succ) :
      ℕ)
Tactic: rcases i with ⟨i, _⟩
Cleared hypotheses: i, H