awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
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:
match i with
    | 0 => exact e0
    | 1 => exact e1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
⊢ LE.le (α := Fin 2) 0 1

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
⊢ 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)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
⊢ LE.le (α := Fin (⦋1⦌.len + 1)) 1 0

Tactic:
rw [e0, e1] at this
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)) 1 0
⊢ ¬LE.le (α := Fin (⦋1⦌.len + 1)) 1 0

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)) 1 0
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
exact Not.elim (by decide) this

Premises used: Not.elim
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋1⦌
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
match e0 : f.toOrderHom 0, e1 : f.toOrderHom 1 with
  | 0, 0 | 1, 1 =>
    refine .inl ⟨f.toOrderHom 0, ?_⟩
    ext i : 3
    match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
  | 0, 1 =>
    right
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1
  | 1, 0 =>
    have := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)
    rw [e0, e1] at this
    exact Not.elim (by decide) this
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
j : Fin (n + 1)
⊢ j ≤ j

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
j : Fin (n + 1)
⊢ mkOfLe j j ⋯ = ⦋1⦌.const ⦋n⦌ j

Tactic:
Hom.ext_one_left _ _

Premises used: SimplexCategory.Hom.ext_one_left
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
⊢ j < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
⊢ j + l < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
⊢ (Hom.toOrderHom (mkOfSucc i) : (a : Fin 2) → Fin (n + 1)) 0 = i.castSucc

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
⊢ (Hom.toOrderHom (mkOfSucc i) : (a : Fin 2) → Fin (n + 1)) 1 = i.succ

Tactic:
rfl

Premises used: Fin.succ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ mkOfSucc 0 = 𝟙 ⦋1⦌

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ (↑i : ℕ) + j < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i i' : Fin (l + 1)
hii' : i ≤ i'
⊢ LE.le (α := Fin (n + 1)) ((fun (i : Fin (l + 1)) ↦ (⟨(↑i : ℕ) + j, ⋯⟩ : Fin (n + 1))) i)
    ((fun (i : Fin (l + 1)) ↦ (⟨(↑i : ℕ) + j, ⋯⟩ : Fin (n + 1))) i')

Tactic:
simpa only [Fin.mk_le_mk, add_le_add_iff_right] using hii'

Premises used: Fin.mk_le_mk, add_le_add_iff_right
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
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 : ℕ), ⋯⟩ : ⦋0⦌ ⟶ ⦋n⦌)
⊢ Eq (α := ⦋0⦌ ⟶ ⦋n⦌) (⦋0⦌.const ⦋l⦌ i ≫ subinterval j l hjl) (⦋0⦌.const ⦋n⦌ ⟨j + (↑i : ℕ), ⋯⟩)

Tactic:
rw [const_comp]

Premises used: SimplexCategory.const_comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
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 : ℕ), ⋯⟩ : Fin (⦋n⦌.len + 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⦌)

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
e_i :
  (↑((Hom.toOrderHom (subinterval j l hjl) : (a : Fin (⦋l⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i) : ℕ) =
    (↑(⟨j + (↑i : ℕ), ⋯⟩ : Fin (⦋n⦌.len + 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))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
e_i e_i₁ : j + (↑i : ℕ) = j + (↑i : ℕ)
⊢ (↑i : ℕ) + j = j + (↑i : ℕ)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin l
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' := ⋯ : 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))
            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 : ℕ), ⋯⟩ : Fin n).castSucc
                      | 1 => (⟨j + (↑i : ℕ), ⋯⟩ : Fin n).succ,
                    monotone' := ⋯ : Fin (HAdd.hAdd (α := ℕ) 1 1) →o Fin (n + 1) }) :
              (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
            i_1) :
        ℕ)
⊢ 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) }

Tactic:
ext (i : Fin 2)

Premises used: OfNat.ofNat, Fin
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i_1 : Fin l
i : Fin 2
simp : (↑i_1 : ℕ) + j = j + (↑i_1 : ℕ)
⊢ (↑((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) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i_1 : Fin l
i : Fin 2
⊢ (↑i_1 : ℕ) + j = j + (↑i_1 : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i_1 : Fin l
i : Fin 2
simp : (↑i_1 : ℕ) + 1 + j = j + (↑i_1 : ℕ) + 1
⊢ (↑((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) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i_1 : Fin l
i : Fin 2
⊢ (↑i_1 : ℕ) + 1 + j = j + (↑i_1 : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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))
          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 + (↑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))
          i) :
      ℕ)

Tactic:
match i with | 0 | 1 => simp; lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
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' := ⋯ : 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))
            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, ⋯⟩ : 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))
            i) :
        ℕ)
⊢ 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) }

Tactic:
ext (i : Fin 2)

Premises used: OfNat.ofNat, Fin
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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))
          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, ⋯⟩ : 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))
          0) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
simp : l + j = j + l
⊢ (↑((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) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ l + j = j + l

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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))
          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, ⋯⟩ : 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))
          i) :
      ℕ)

Tactic:
match i with | 0 | 1 => simp <;> lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ : SimplexCategory
f g : Δ ⟶ ⦋0⦌
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))
⊢ f = g

Tactic:
ext : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ : SimplexCategory
f g : Δ ⟶ ⦋0⦌
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:
apply Subsingleton.elim (α := Fin 1)

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋0⦌ ⟶ ⦋0⦌
⊢ f = 𝟙 ⦋0⦌

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
h : x = y
subst : Hom.toOrderHom (eqToHom ⋯) = OrderEmbedding.toOrderHom (OrderIso.toOrderEmbedding (Fin.castOrderIso ⋯))
⊢ Hom.toOrderHom (eqToHom h) = OrderEmbedding.toOrderHom (OrderIso.toOrderEmbedding (Fin.castOrderIso ⋯))

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
⊢ Hom.toOrderHom (eqToHom ⋯) = OrderEmbedding.toOrderHom (OrderIso.toOrderEmbedding (Fin.castOrderIso ⋯))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
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) : ℕ)
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
ext k
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
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) :
      ℕ)
⊢ (↑((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:
dsimp [δ, Fin.succAbove]

Premises used: Fin.succAbove, SimplexCategory.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (⦋n⦌.len + 1)
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) :
        ℕ)
⊢ (↑(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:
rcases i with ⟨i, _⟩