awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (⦋1⦌.len + 1)
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)
    ((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))
      0)

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

Tactic:
e1.trans e0.symm

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

Tactic:
exact e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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 (⦋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))

Tactic:
match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
-- 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) 1
⊢ (∃ (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) 1
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
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) 1
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 (⦋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
-- 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) 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 (⦋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))
      0)

Tactic:
rfl
-- 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) 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 (⦋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))
      1)

Tactic:
e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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) 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 (⦋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))
      1)

Tactic:
exact e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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) 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 (⦋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))

Tactic:
match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
-- 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) 2
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:
.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) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 2
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) 2
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⦌.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
-- 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) 2
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⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)) :
        (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1))
      0)

Tactic:
rfl
-- 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) 2
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⦌.const ⦋2⦌ ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0)) :
        (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1))
      1)

Tactic:
e1.trans e0.symm

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

Tactic:
exact e1.trans e0.symm

Premises used: Eq.symm, Eq.trans
-- 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) 2
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⦌.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))

Tactic:
match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
-- 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) 0
⊢ LE.le (α := Fin (⦋2⦌.len + 1)) 1 0

Tactic:
rw [e0, e1] at this
-- 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) 0
this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 1 0
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1

Tactic:
rw [e0, e1] at this
-- 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) 0
this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 1 0
e0₁ : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 1
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0

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

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this : LE.le (α := Fin (⦋2⦌.len + 1)) 1 0
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) 0
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
exact Not.elim (by decide) this

Premises used: Not.elim
-- 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) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
⊢ LE.le (α := Fin (⦋2⦌.len + 1)) 2 0

Tactic:
rw [e0, e1] at this
-- 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) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 2 0
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2

Tactic:
rw [e0, e1] at this
-- 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) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 2 0
e0₁ : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0

Tactic:
rw [e0, e1] at this
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this : LE.le (α := Fin (⦋2⦌.len + 1)) 2 0
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 0
⊢ ¬LE.le (α := Fin (⦋2⦌.len + 1)) 2 0

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this : LE.le (α := Fin (⦋2⦌.len + 1)) 2 0
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
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:
exact Not.elim (by decide) this

Premises used: Not.elim
-- 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) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ LE.le (α := Fin (⦋2⦌.len + 1)) 2 1

Tactic:
rw [e0, e1] at this
-- 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) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 2 1
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2

Tactic:
rw [e0, e1] at this
-- 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) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
this₁ : LE.le (α := Fin (⦋2⦌.len + 1)) 2 1
e0₁ : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
⊢ Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1

Tactic:
rw [e0, e1] at this
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this : LE.le (α := Fin (⦋2⦌.len + 1)) 2 1
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
e1 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 1) 1
⊢ ¬LE.le (α := Fin (⦋2⦌.len + 1)) 2 1

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
this : LE.le (α := Fin (⦋2⦌.len + 1)) 2 1
e0 : Eq (α := Fin (⦋2⦌.len + 1)) ((Hom.toOrderHom f : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋2⦌.len + 1)) 0) 2
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:
exact Not.elim (by decide) this

Premises used: Not.elim
-- 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)
⊢ (∃ (i : Fin (HAdd.hAdd (α := ℕ) 1 2)), f = δ i) ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
match e0 : f.toOrderHom 0, e1 : f.toOrderHom 1 with
  | 1, 2 =>
    refine .inl ⟨0, ?_⟩
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1
  | 0, 2 =>
    refine .inl ⟨1, ?_⟩
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1
  | 0, 1 =>
    refine .inl ⟨2, ?_⟩
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1
  | 0, 0 | 1, 1 | 2, 2 =>
    refine .inr ⟨f.toOrderHom 0, ?_⟩
    ext i : 3
    match i with
    | 0 => rfl
    | 1 => exact e1.trans e0.symm
  | 1, 0 | 2, 0 | 2, 1 =>
    rw [e0, e1] at this
    exact Not.elim (by decide) this