awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
f : ⦋1⦌ ⟶ ⦋2⦌
⊢ f = δ 0 ∨ f = δ 1 ∨ f = δ 2 ∨ ∃ (a : Fin (⦋2⦌.len + 1)), f = ⦋1⦌.const ⦋2⦌ a

Tactic:
match eq_of_one_to_two f with
  | .inl ⟨0, h⟩ => .inl h
  | .inl ⟨1, h⟩ => .inr (.inl h)
  | .inl ⟨2, h⟩ => .inr (.inr (.inl h))
  | .inr h => .inr (.inr (.inr h))

Premises used: SimplexCategory.eq_of_one_to_two, Exists, SimplexCategory.δ, SimplexCategory.const, SimplexCategory.mk, Or.inl, Or, OfNat.ofNat, Eq, _private.0.SimplexCategory.eq_of_one_to_two'.match_1, Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
Δ₁ Δ₂ : SimplexCategory
f : Δ₁ ⟶ Δ₂
⊢ LinOrd.Hom.hom (skeletalFunctor.map f).hom = Hom.toOrderHom f

Tactic:
rfl

Premises used: SimplexCategory.Hom.toOrderHom, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
len : X.len = Y.len
⊢ X = Y

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X.len = Y.len

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
suffices : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X = Y

Tactic:
suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1)) by
    ext
    simpa
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
f : Fin (X.len + 1) ≃ Fin (Y.len + 1)
⊢ Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))

Tactic:
apply Fintype.card_congr

Premises used: Fintype.card_congr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X Y : SimplexCategory
h : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (X.len + 1) ≃ Fin (Y.len + 1)

Tactic:
exact ((skeletalFunctor ⋙ forget NonemptyFinLinOrd).mapIso I).toEquiv

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Functor.comp, SimplexCategory.skeletalFunctor, CategoryTheory.forget, CategoryTheory.Functor.mapIso, NonemptyFinLinOrd
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x x_1 : SimplexCategory
f g : x ⟶ x_1
h : skeletalFunctor.map f = skeletalFunctor.map g
a :
  ∀ (x_2 : Fin (x.len + 1)),
    Eq (α := Fin (x_1.len + 1)) ((Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))
      ((Hom.toOrderHom g : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))
⊢ f = g

Tactic:
ext : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x x_1 : SimplexCategory
f g : x ⟶ x_1
h : skeletalFunctor.map f = skeletalFunctor.map g
x_2 : Fin (x.len + 1)
⊢ Eq (α := Fin (x_1.len + 1)) ((Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))
    ((Hom.toOrderHom g : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))

Tactic:
CategoryTheory.congr_fun h _

Premises used: CategoryTheory.congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x x_1 : SimplexCategory
f g : x ⟶ x_1
h : skeletalFunctor.map f = skeletalFunctor.map g
x_2 : Fin (x.len + 1)
⊢ Eq (α := Fin (x_1.len + 1)) ((Hom.toOrderHom f : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))
    ((Hom.toOrderHom g : (a : Fin (x.len + 1)) → Fin (x_1.len + 1)) x_2 : Fin (x_1.len + 1))

Tactic:
exact CategoryTheory.congr_fun h _

Premises used: CategoryTheory.congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
⊢ Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1

Tactic:
have aux : Fintype.card X = Fintype.card X - 1 + 1 :=
          (Nat.succ_pred_eq_of_pos <| Fintype.card_pos_iff.mpr ⟨⊥⟩).symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
⊢ StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))

Tactic:
have hf := (Finset.univ.orderEmbOfFin aux).strictMono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
hf₁ :
  ∀ (x : (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type)),
    Eq (α := (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
      ((LinOrd.Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := X)
                  (InducedCategory.homMk
                    (LinOrd.ofHom
                      { toFun := (⇑f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type)),
                        monotone' := ⋯ }))
                  (InducedCategory.homMk
                    (LinOrd.ofHom
                      {
                        toFun :=
                          (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)),
                        monotone' := ⋯ })))) :
            (a : (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type)) →
              (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
          x :
        (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
      ((LinOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 (skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌))) :
            (a : (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type)) →
              (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
          x :
        (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
⊢ CategoryStruct.comp (Y := X)
      (InducedCategory.homMk
        (LinOrd.ofHom
          { toFun := (⇑f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type)),
            monotone' := ⋯ }))
      (InducedCategory.homMk
        (LinOrd.ofHom
          { toFun := (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)),
            monotone' := ⋯ })) =
    𝟙 (skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
x : (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type)
⊢ Eq (α := (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := X)
                (InducedCategory.homMk
                  (LinOrd.ofHom
                    { toFun := (⇑f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type)),
                      monotone' := ⋯ }))
                (InducedCategory.homMk
                  (LinOrd.ofHom
                    { toFun := (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)),
                      monotone' := ⋯ })))) :
          (a : (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type)) →
            (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
        x :
      (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
    ((LinOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 (skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌))) :
          (a : (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type)) →
            (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))
        x :
      (↑(skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌).toLinOrd : Type))

Tactic:
apply f.symm_apply_apply

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
hf₁ :
  ∀ (x : (↑X.toLinOrd : Type)),
    Eq (α := (↑X.toLinOrd : Type))
      ((LinOrd.Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌)
                  (InducedCategory.homMk
                    (LinOrd.ofHom
                      {
                        toFun :=
                          (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)),
                        monotone' := ⋯ }))
                  (InducedCategory.homMk
                    (LinOrd.ofHom
                      { toFun := (⇑f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type)),
                        monotone' := ⋯ })))) :
            (a : (↑X.toLinOrd : Type)) → (↑X.toLinOrd : Type))
          x :
        (↑X.toLinOrd : Type))
      ((LinOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 X)) : (a : (↑X.toLinOrd : Type)) → (↑X.toLinOrd : Type)) x :
        (↑X.toLinOrd : Type))
⊢ CategoryStruct.comp (Y := skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌)
      (InducedCategory.homMk
        (LinOrd.ofHom
          { toFun := (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)),
            monotone' := ⋯ }))
      (InducedCategory.homMk
        (LinOrd.ofHom
          { toFun := (⇑f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type)),
            monotone' := ⋯ })) =
    𝟙 X

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
x : (↑X.toLinOrd : Type)
⊢ Eq (α := (↑X.toLinOrd : Type))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌)
                (InducedCategory.homMk
                  (LinOrd.ofHom
                    { toFun := (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)),
                      monotone' := ⋯ }))
                (InducedCategory.homMk
                  (LinOrd.ofHom
                    { toFun := (⇑f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type)),
                      monotone' := ⋯ })))) :
          (a : (↑X.toLinOrd : Type)) → (↑X.toLinOrd : Type))
        x :
      (↑X.toLinOrd : Type))
    ((LinOrd.Hom.hom (InducedCategory.Hom.hom (𝟙 X)) : (a : (↑X.toLinOrd : Type)) → (↑X.toLinOrd : Type)) x :
      (↑X.toLinOrd : Type))

Tactic:
apply f.apply_symm_apply

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
hom :
  Monotone (α := (↑X.1 : Type)) (β := Fin (⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌.len + 1))
    (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1))
⊢ skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌ ≅ X

Tactic:
refine
          { hom := InducedCategory.homMk (LinOrd.ofHom ⟨f, hf.monotone⟩)
            inv := InducedCategory.homMk (LinOrd.ofHom ⟨f.symm, ?_⟩)
            hom_inv_id := by ext; apply f.symm_apply_apply
            inv_hom_id := by ext; apply f.apply_symm_apply }
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
i j : (↑X.1 : Type)
h : i ≤ j
rw :
  LE.le (α := (↑X.toLinOrd : Type))
    ((Finset.orderEmbOfFin Finset.univ aux :
          (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) i :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))
    ((Finset.orderEmbOfFin Finset.univ aux :
          (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) j :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))
⊢ LE.le (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1))
    ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) i :
      Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1))
    ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) j :
      Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1))

Tactic:
rw [← hf.le_iff_le]

Premises used: StrictMono.le_iff_le
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
i j : (↑X.1 : Type)
h : i ≤ j
change :
  LE.le (α := (↑X.toLinOrd : Type))
    ((f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) i :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))
    ((f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) j :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))
⊢ LE.le (α := (↑X.toLinOrd : Type))
    ((Finset.orderEmbOfFin Finset.univ aux :
          (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) i :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))
    ((Finset.orderEmbOfFin Finset.univ aux :
          (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) j :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))

Tactic:
change f (f.symm i) ≤ f (f.symm j)

Premises used: OrderIso.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X : NonemptyFinLinOrd
aux : Fintype.card (↑X.toLinOrd : Type) = Fintype.card (↑X.toLinOrd : Type) - 1 + 1
f : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1) ≃o (↑X.toLinOrd : Type) := monoEquivOfFin (↑X.toLinOrd : Type) aux
hf :
  StrictMono (α := Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) (β := (↑X.toLinOrd : Type))
    (⇑(Finset.orderEmbOfFin Finset.univ aux) :
      (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
i j : (↑X.1 : Type)
h : i ≤ j
⊢ LE.le (α := (↑X.toLinOrd : Type))
    ((f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) i :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))
    ((f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type))
        ((f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) j :
          Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) :
      (↑X.toLinOrd : Type))

Tactic:
simpa only [OrderIso.apply_symm_apply]

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
⊢ ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC := fun (X : SimplexCategory) ↦
      Fin (X.len + 1)) x =
    Fin (x.len + 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
⊢ @ConcreteCategory.hom _ smallCategory (fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1))
      (fun (X Y : SimplexCategory) ↦
        (OrderHom.instFunLike : FunLike (Fin (X.len + 1) →o Fin (Y.len + 1)) (Fin (X.len + 1)) (Fin (Y.len + 1))))
      _ _ _ (𝟙 n : n ⟶ n) =
    OrderHom.id

Tactic:
rfl

Premises used: OrderHom.id, SimplexCategory.Hom.id, SimplexCategory.Hom.toOrderHom, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
⊢ (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ i)) :
      (a : Fin (n + 1)) → Fin (n + 1 + 1)) =
    i.succAbove

Tactic:
rfl

Premises used: Fin.succAbove, rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ i)) :
      (a : Fin (n + 1 + 1)) → Fin (n + 1)) =
    i.predAbove

Tactic:
rfl

Premises used: Fin.predAbove, dite, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
rw :
  Mono (skeletalEquivalence.functor.map f) ↔
    Function.Injective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))
⊢ Mono f ↔
    Function.Injective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))

Tactic:
rw [← Functor.mono_map_iff_mono skeletalEquivalence.functor]

Premises used: SimplexCategory.skeletalEquivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.mono_map_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔
    Function.Injective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))

Tactic:
simp only [skeletalFunctor_obj, skeletalFunctor_map,
    NonemptyFinLinOrd.mono_iff_injective, NonemptyFinLinOrd.coe_of, ConcreteCategory.hom_ofHom]

Premises used: NonemptyFinLinOrd.coe_of, SimplexCategory.skeletalFunctor_obj, SimplexCategory.skeletalFunctor_map, NonemptyFinLinOrd.mono_iff_injective, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
rw :
  Epi (skeletalEquivalence.functor.map f) ↔
    Function.Surjective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))
⊢ Epi f ↔
    Function.Surjective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))

Tactic:
rw [← Functor.epi_map_iff_epi skeletalEquivalence.functor]

Premises used: SimplexCategory.skeletalEquivalence, CategoryTheory.Functor.epi_map_iff_epi, CategoryTheory.Equivalence.functor
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔
    Function.Surjective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))

Tactic:
simp only [skeletalFunctor_obj, skeletalFunctor_map,
    NonemptyFinLinOrd.epi_iff_surjective, NonemptyFinLinOrd.coe_of, ConcreteCategory.hom_ofHom]

Premises used: NonemptyFinLinOrd.coe_of, NonemptyFinLinOrd.epi_iff_surjective, SimplexCategory.skeletalFunctor_obj, SimplexCategory.skeletalFunctor_map, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
f : x ⟶ y
inst rwa rwa₁ rwa₂ rwa₃ : Mono f
⊢ Function.Injective (α := Fin (x.len + 1)) (β := Fin (y.len + 1))
    (⇑(Hom.toOrderHom f) : (a : Fin (x.len + 1)) → Fin (y.len + 1))

Tactic:
rwa [← mono_iff_injective]

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
f : x ⟶ y
inst : Mono f
⊢ x.len ≤ y.len

Tactic:
simpa using Fintype.card_le_of_injective f.toOrderHom.toFun
    (by dsimp; rwa [← mono_iff_injective])

Premises used: Fintype.card_le_of_injective, OrderHom.toFun, SimplexCategory.Hom.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Mono f
⊢ n ≤ m

Tactic:
len_le_of_mono f

Premises used: SimplexCategory.len_le_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
f : x ⟶ y
inst rwa rwa₁ rwa₂ rwa₃ : Epi f
⊢ Function.Surjective (α := Fin (x.len + 1)) (β := Fin (y.len + 1))
    (⇑(Hom.toOrderHom f) : (a : Fin (x.len + 1)) → Fin (y.len + 1))

Tactic:
rwa [← epi_iff_surjective]

Premises used: SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
f : x ⟶ y
inst : Epi f
⊢ y.len ≤ x.len

Tactic:
simpa using Fintype.card_le_of_surjective f.toOrderHom.toFun
    (by dsimp; rwa [← epi_iff_surjective])

Premises used: OrderHom.toFun, SimplexCategory.Hom.toOrderHom, Fintype.card_le_of_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
⊢ m ≤ n

Tactic:
len_le_of_epi f

Premises used: SimplexCategory.len_le_of_epi