awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
a :
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ i.succ.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
a : (↑i.castSucc.castSucc : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 0) : ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ i.succ.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
      Fin.zero_eta, OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_zero, Fin.succAboveOrderEmb_apply,
      Fin.castSucc_succAbove_castSucc, Fin.succAbove_succ_self]

Premises used: SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkHom, SimplexCategory.δ, Nat.reduceAdd, SimplexCategory.mkOfSucc_homToOrderHom_zero, Fin.zero_eta, Fin.castSucc_succAbove_castSucc, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe, Function.comp_apply, SimplexCategory.comp_toOrderHom, Fin.succAbove_succ_self, Fin.succAboveOrderEmb_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
⊢ (↑i.castSucc.castSucc : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 0) : ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
a :
  (↑(j.succAbove i.succ) : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)

Tactic:
simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, Fin.mk_one,
      OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
      mkOfSucc_homToOrderHom_one, Fin.succAboveOrderEmb_apply]

Premises used: Fin.mk_one, SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkOfSucc_homToOrderHom_one, SimplexCategory.mkHom, SimplexCategory.δ, Nat.reduceAdd, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe, Function.comp_apply, SimplexCategory.comp_toOrderHom, Fin.succAboveOrderEmb_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
a :
  (↑(i.succ.castSucc.succAbove i.succ) : ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
⊢ (↑(j.succAbove i.succ) : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
a : (↑i.succ.succ : ℕ) = (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)
⊢ (↑(i.succ.castSucc.succAbove i.succ) : ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin 2) → Fin (n + 1 + 1)) 1) : ℕ)

Tactic:
rw [Fin.succAbove_castSucc_self]

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

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ mkOfSucc 1 = δ 0

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ mkOfSucc 0 = δ 2

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
⊢ LE.le (α := Fin 2) 0 1

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
⊢ LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)

Tactic:
have : f.toOrderHom 0 ≤ f.toOrderHom 1 := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
.inl ⟨0, ?_⟩

Premises used: Exists.intro, Or.inl, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
refine : f = δ 0
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨0, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
a :
  ∀ (i : Fin (⦋1⦌.len + 1)),
    Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
      ((Hom.toOrderHom (δ 0) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
⊢ f = δ 0

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom (δ 0) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)

Tactic:
e0

Premises used: Fin.succAbove, Fin.succ, Fin.ofNat, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom (δ 0) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)

Tactic:
exact e0
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
    ((Hom.toOrderHom (δ 0) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)

Tactic:
e1

Premises used: Fin.succAbove, Fin.succ, Fin.ofNat, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
    ((Hom.toOrderHom (δ 0) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)

Tactic:
exact e1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (δ 0) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))

Tactic:
match i with
    | 0 => exact e0
    | 1 => exact e1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
.inl ⟨1, ?_⟩

Premises used: Exists.intro, Or.inl, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
refine : f = δ 1
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨1, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
a :
  ∀ (i : Fin (⦋1⦌.len + 1)),
    Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
      ((Hom.toOrderHom (δ 1) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
⊢ f = δ 1

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom (δ 1) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)

Tactic:
e0

Premises used: Fin.succAbove, Fin.ofNat, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom (δ 1) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)

Tactic:
exact e0
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
    ((Hom.toOrderHom (δ 1) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)

Tactic:
e1

Premises used: Fin.succAbove, Fin.succ, Fin.ofNat, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
    ((Hom.toOrderHom (δ 1) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)

Tactic:
exact e1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (δ 1) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))

Tactic:
match i with
    | 0 => exact e0
    | 1 => exact e1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
.inl ⟨2, ?_⟩

Premises used: Exists.intro, Or.inl, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
refine : f = δ 2
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨2, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
a :
  ∀ (i : Fin (⦋1⦌.len + 1)),
    Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
      ((Hom.toOrderHom (δ 2) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
⊢ f = δ 2

Tactic:
ext i : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom (δ 2) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)

Tactic:
e0

Premises used: Fin.succAbove, Fin.ofNat, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom (δ 2) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)

Tactic:
exact e0
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
    ((Hom.toOrderHom (δ 2) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)

Tactic:
e1

Premises used: Fin.succAbove, Fin.ofNat, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
    ((Hom.toOrderHom (δ 2) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)

Tactic:
exact e1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
    ((Hom.toOrderHom (δ 2) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))

Tactic:
match i with
    | 0 => exact e0
    | 1 => exact e1
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
.inr ⟨f.toOrderHom 0, ?_⟩

Premises used: Exists.intro, SimplexCategory.Hom.toOrderHom, OfNat.ofNat, DFunLike.coe, Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
refine : f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inr ⟨f.toOrderHom 0, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this :
  LE.le (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1)
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 0
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
a :
  ∀ (i : Fin (⦋1⦌.len + 1)),
    Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) i : Fin (⦋2⦌.len + 1))
      ((Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)) :
            (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1))
          i :
        Fin (⦋2⦌.len + 1))
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)

Tactic:
ext i : 3