awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
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
⊢ skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌ ≅ X
have 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))
Tactic: have hf := (Finset.univ.orderEmbOfFin aux).strictMono
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
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))
⊢ 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⦌)
have 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' := sorry }))
                (InducedCategory.homMk
                  (LinOrd.ofHom
                    { toFun := (⇑f.symm : (a : (↑X.toLinOrd : Type)) → Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)),
                      monotone' := sorry })))) :
          (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: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
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))
⊢ 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
have 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' := sorry }))
                (InducedCategory.homMk
                  (LinOrd.ofHom
                    { toFun := (⇑f : (a : Fin (Fintype.card (↑X.toLinOrd : Type) - 1 + 1)) → (↑X.toLinOrd : Type)),
                      monotone' := sorry })))) :
          (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: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
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))
⊢ skeletalFunctor.obj ⦋Fintype.card (↑X.toLinOrd : Type) - 1⦌ ≅ X
have 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))
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 }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
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 (α := 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))
have 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))
Tactic: rw [← hf.le_iff_le]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
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))
    ((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))
have 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))
Tactic: change f (f.symm i) ≤ f (f.symm j)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono f ↔
    Function.Injective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))
have 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))
Tactic: rw [← Functor.mono_map_iff_mono skeletalEquivalence.functor]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi f ↔
    Function.Surjective (α := Fin (n.len + 1)) (β := Fin (m.len + 1))
      (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (m.len + 1))
have 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))
Tactic: rw [← Functor.epi_map_iff_epi skeletalEquivalence.functor]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
A B : SimplexCategory
f : A ⟶ B
hf :
  IsIso (X :=
    Functor.obj
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      A)
    (CategoryTheory.Functor.map
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      f)
y₁ y₂ : Fin (B.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬LE.le (α := Fin (A.len + 1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₁ :
        (fun (X : Type) ↦ X)
          (Functor.obj
            (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
            A))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₂ :
        (fun (X : Type) ↦ X)
          (Functor.obj
            (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
            A))
⊢ False
have pos : y₂ ≤ y₁
Tactic: apply not_le.mpr h'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
A B : SimplexCategory
f : A ⟶ B
hf :
  IsIso (X :=
    Functor.obj
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      A)
    (CategoryTheory.Functor.map
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      f)
y₁ y₂ : Fin (B.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬LE.le (α := Fin (A.len + 1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₁ :
        (fun (X : Type) ↦ X)
          (Functor.obj
            (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
            A))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (inv
                (CategoryTheory.Functor.map
                  (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                    (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                  f)) :
            (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
              (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
          y₂ :
        (fun (X : Type) ↦ X)
          (Functor.obj
            (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
            A))
⊢ y₂ ≤ y₁
have h₁ : y₂ =
  (Hom.toOrderHom f : (a : Fin (A.len + 1)) → Fin (B.len + 1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (inv
            (CategoryTheory.Functor.map
              (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
              f)) :
        (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
          (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A))
      y₂)
Tactic: convert! f.toOrderHom.monotone (le_of_not_ge h'')
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
A B : SimplexCategory
f : A ⟶ B
hf :
  IsIso (X :=
    Functor.obj
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      A)
    (CategoryTheory.Functor.map
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      f)
⊢ f ≫
      Hom.mk
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                  (inv
                    (CategoryTheory.Functor.map
                      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                        (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                      f))) :
              (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
                (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A)),
          monotone' := ⋯ } =
    𝟙 A
have a : ∀ (x : Fin (A.len + 1)),
  Eq (α := Fin (A.len + 1))
    ((Hom.toOrderHom
            (f ≫
              Hom.mk
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                          (inv
                            (CategoryTheory.Functor.map
                              (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦
                                Fin (i.len + 1) →o Fin (j.len + 1)) (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                              f))) :
                      (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
                        (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A)),
                  monotone' := sorry }) :
          (a : Fin (A.len + 1)) → Fin (A.len + 1))
        x :
      Fin (A.len + 1))
    ((Hom.toOrderHom (𝟙 A) : (a : Fin (A.len + 1)) → Fin (A.len + 1)) x : Fin (A.len + 1))
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
A B : SimplexCategory
f : A ⟶ B
hf :
  IsIso (X :=
    Functor.obj
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      A)
    (CategoryTheory.Functor.map
      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
        fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
      f)
⊢ Hom.mk
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                  (inv
                    (CategoryTheory.Functor.map
                      (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1))
                        (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                      f))) :
              (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
                (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A)),
          monotone' := ⋯ } ≫
      f =
    𝟙 B
have a : ∀ (x : Fin (B.len + 1)),
  Eq (α := Fin (B.len + 1))
    ((Hom.toOrderHom
            (Hom.mk
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                          (inv
                            (CategoryTheory.Functor.map
                              (forget SimplexCategory (FC := fun (i j : SimplexCategory) ↦
                                Fin (i.len + 1) →o Fin (j.len + 1)) (CC := fun (X : SimplexCategory) ↦ Fin (X.len + 1)))
                              f))) :
                      (a : (fun (X : Type) ↦ X) ((forget SimplexCategory).obj B)) →
                        (fun (X : Type) ↦ X) ((forget SimplexCategory).obj A)),
                  monotone' := sorry } ≫
              f) :
          (a : Fin (B.len + 1)) → Fin (B.len + 1))
        x :
      Fin (B.len + 1))
    ((Hom.toOrderHom (𝟙 B) : (a : Fin (B.len + 1)) → Fin (B.len + 1)) x : Fin (B.len + 1))
Tactic: ext x : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Mono f
⊢ IsIso f ↔ n.len = m.len
have refine : ∀ (h : n.len = m.len), IsIso f
Tactic: refine ⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Mono f
h : n.len = m.len
⊢ IsIso f
have obtain : ∀ (f : n ⟶ n) [hf : Mono f] (h : n.len = n.len), IsIso f
Tactic: obtain rfl : n = m := by aesop
Cleared hypotheses: m, f, hf, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : SimplexCategory
f : n ⟶ n
hf : Mono f
h : n.len = n.len
⊢ IsIso f
have hf₁ : Function.Injective (α := Fin (n.len + 1)) (β := Fin (n.len + 1))
  (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (n.len + 1))
Tactic: rw [mono_iff_injective] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : SimplexCategory
f : n ⟶ n
hf :
  Function.Injective (α := Fin (n.len + 1)) (β := Fin (n.len + 1))
    (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (n.len + 1))
h : n.len = n.len
⊢ Function.Surjective (Hom.toOrderHom f).toFun
have rwa : Function.Injective (Hom.toOrderHom f).toFun
Tactic: rwa [← Finite.injective_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Mono (δ i)
have rw : Function.Injective (α := Fin (⦋n⦌.len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
  (⇑(Hom.toOrderHom (δ i)) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
Tactic: rw [mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Epi f
⊢ IsIso f ↔ n.len = m.len
have refine : ∀ (h : n.len = m.len), IsIso f
Tactic: refine ⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Epi f
h : n.len = m.len
⊢ IsIso f
have obtain : ∀ (f : n ⟶ n) [hf : Epi f] (h : n.len = n.len), IsIso f
Tactic: obtain rfl : n = m := by aesop
Cleared hypotheses: m, f, hf, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : SimplexCategory
f : n ⟶ n
hf : Epi f
h : n.len = n.len
⊢ IsIso f
have hf₁ : Function.Surjective (α := Fin (n.len + 1)) (β := Fin (n.len + 1))
  (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (n.len + 1))
Tactic: rw [epi_iff_surjective] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : SimplexCategory
f : n ⟶ n
hf :
  Function.Surjective (α := Fin (n.len + 1)) (β := Fin (n.len + 1))
    (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (n.len + 1))
h : n.len = n.len
⊢ Function.Injective (Hom.toOrderHom f).toFun
have rwa : Function.Surjective (Hom.toOrderHom f).toFun
Tactic: rwa [Finite.injective_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
X Y : SimplexCategory
f : X ⟶ Y
h : Mono f
h_1 : Epi f
⊢ IsIso f
have rw : X.len = Y.len
Tactic: rw [isIso_iff_of_epi]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
x : SimplexCategory
e : x ≅ x
⊢ e = Iso.refl x
have h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
Tactic: have h : (Finset.univ : Finset (Fin (x.len + 1))).card = x.len + 1 := Finset.card_fin (x.len + 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
⊢ e = Iso.refl x
have eq₁ : RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
    (orderIsoOfIso e) =
  Finset.orderEmbOfFin Finset.univ h
Tactic: have eq₁ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso e) i)