awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
w x y z : AugmentedSimplexCategory
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inr 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)) =
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x).inr 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:
simp [-id_tensorHom, -tensorHom_id]

Premises used: AugmentedSimplexCategory.tensorHom_id, AugmentedSimplexCategory.id_tensorHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Goal:
w x y z : AugmentedSimplexCategory
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
            (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inr
        z ≫
      (Iso.hom (α_ w x y) ⊗ₘ 𝟙 z) ≫
        Iso.hom (α_ w (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) x y) z) ≫
          (𝟙 w ⊗ₘ Iso.hom (α_ x y z)) =
    (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory)
            (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y).inr
        z ≫
      Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) w x) y z) ≫
        Iso.hom (α_ w x (MonoidalCategoryStruct.tensorObj (𝒞 := WithInitial.instCategory) y z))

Tactic:
simp [-id_tensorHom, -tensorHom_id]

Premises used: AugmentedSimplexCategory.tensorHom_id, AugmentedSimplexCategory.id_tensorHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
a b : SimplexCategory
x x_1 : a ⟶ b
h :
  Eq (α := Fin (a.len + 1) → Fin (b.len + 1)) ((fun (f : a ⟶ b) ↦ (Hom.toOrderHom f).toFun) x)
    ((fun (f : a ⟶ b) ↦ (Hom.toOrderHom f).toFun) x_1)
⊢ x = x_1

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
a b : SimplexCategory
f g : a ⟶ b
h : f = g
x : Fin (a.len + 1)
rw 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))
⊢ 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))

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
tauto tauto₁ 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)
tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ 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) a)
⊢ Monotone (β := Fin (y.len + 1)) fun (x : Fin (x.len + 1)) ↦ i

Tactic:
tauto
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ ⦋0⦌.const ⦋0⦌ 0 = 𝟙 ⦋0⦌

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
i : Fin (y.len + 1)
a : Fin (x.len + 1)
⊢ (Hom.toOrderHom (x.const y i) : (a : Fin (x.len + 1)) → Fin (y.len + 1)) a = i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y z : SimplexCategory
f : y ⟶ z
i : Fin (y.len + 1)
⊢ x.const y i ≫ f = x.const z ((Hom.toOrderHom f : (a : Fin (y.len + 1)) → Fin (z.len + 1)) i)

Tactic:
rfl

Premises used: OrderHom.comp, SimplexCategory.const, SimplexCategory.Hom.comp, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
i : Fin (m.len + 1)
rw : n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i) : (a : Fin (⦋0⦌.len + 1)) → Fin (m.len + 1)) 0)
⊢ n.const m i = CategoryStruct.comp (Y := ⦋0⦌) (n.const ⦋0⦌ 0) (⦋0⦌.const m i)

Tactic:
rw [const_comp]

Premises used: SimplexCategory.const_comp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
i : Fin (m.len + 1)
⊢ n.const m i = n.const m ((Hom.toOrderHom (⦋0⦌.const m i) : (a : Fin (⦋0⦌.len + 1)) → Fin (m.len + 1)) 0)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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) : ℕ)
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
i : Fin (⦋0⦌.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) : ℕ)

Tactic:
h0 ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
i : Fin (⦋0⦌.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) : ℕ)

Tactic:
exact h0 ▸ rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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:
match i with | 0 => exact h0 ▸ rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
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) :
        ℕ)
⊢ f = ⦋0⦌.const n ((Hom.toOrderHom f : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) 0)

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
x : Fin (⦋0⦌.len + 1)
⊢ (↑((Hom.toOrderHom f : (a : Fin (⦋0⦌.len + 1)) → Fin (n.len + 1)) 0) : ℕ) =
    (↑((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))
          0) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
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:
match x with | 0 => rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : ⦋0⦌ ⟶ n
⊢ ∃ (a : Fin (n.len + 1)), f = ⦋0⦌.const n a

Tactic:
⟨_, eq_const_of_zero _⟩

Premises used: SimplexCategory.eq_const_of_zero, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : n ⟶ ⦋0⦌
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))
⊢ f = n.const ⦋0⦌ 0

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

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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) : ℕ)
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
i : Fin (⦋1⦌.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) : ℕ)

Tactic:
h0 ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
i : Fin (⦋1⦌.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) : ℕ)

Tactic:
exact h0 ▸ rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
i : Fin (⦋1⦌.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) : ℕ)

Tactic:
h1 ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
i : Fin (⦋1⦌.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) : ℕ)

Tactic:
exact h1 ▸ rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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:
match i with
  | 0 => exact h0 ▸ rfl
  | 1 => exact h1 ▸ rfl
-- 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) 0
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

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

Premises used: Exists.intro, SimplexCategory.Hom.toOrderHom, Or.inl, OfNat.ofNat, DFunLike.coe
-- 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) 0
refine : f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
refine .inl ⟨f.toOrderHom 0, ?_⟩
-- 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) 0
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))
⊢ f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)

Tactic:
ext i : 3
-- 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) 0
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
    ((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))
      0)

Tactic:
rfl
-- 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) 0
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 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))
      1)

Tactic:
e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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) 0
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 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))
      1)

Tactic:
exact e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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) 0
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:
match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
-- 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) 1
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

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

Premises used: Exists.intro, SimplexCategory.Hom.toOrderHom, Or.inl, OfNat.ofNat, DFunLike.coe
-- 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) 1
refine : f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
refine .inl ⟨f.toOrderHom 0, ?_⟩
-- 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) 1
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))
⊢ f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)

Tactic:
ext i : 3
-- 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) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)
    ((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))
      0)

Tactic:
rfl
-- 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) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 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))
      1)

Tactic:
e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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) 1
i : Fin (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋1⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 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))
      1)

Tactic:
exact e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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) 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⦌.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:
match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
-- 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
h : f = 𝟙 ⦋1⦌
⊢ (∃ (a : Fin (⦋1⦌.len + 1)), f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
right
-- 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
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))
⊢ f = 𝟙 ⦋1⦌

Tactic:
ext i : 3
-- 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)) 0)
    ((Hom.toOrderHom (𝟙 ⦋1⦌) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)

Tactic:
e0

Premises used: Fin.ofNat
-- 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)) 0)
    ((Hom.toOrderHom (𝟙 ⦋1⦌) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 0)

Tactic:
exact e0
-- 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)) 1)
    ((Hom.toOrderHom (𝟙 ⦋1⦌) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1)

Tactic:
e1

Premises used: Fin.ofNat
-- 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)) 1)
    ((Hom.toOrderHom (𝟙 ⦋1⦌) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋1⦌.len + 1)) 1)

Tactic:
exact e1