awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
f : x ⟶ y
inst : IsIso f
⊢ x.len = y.len

Tactic:
le_antisymm (len_le_of_mono f) (len_le_of_epi f)

Premises used: SimplexCategory.len_le_of_mono, SimplexCategory.len_le_of_epi, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : IsIso f
⊢ n = m

Tactic:
len_eq_of_isIso f

Premises used: SimplexCategory.len_eq_of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Epi (σ i)

Tactic:
simpa only [epi_iff_surjective] using Fin.predAbove_surjective i

Premises used: Fin.predAbove_surjective, SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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))
pos : y₂ ≤ y₁
⊢ False

Tactic:
apply not_le.mpr h'

Premises used: not_le, Iff.mpr
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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₂ =
    (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:
(ConcreteCategory.congr_hom (Iso.inv_hom_id
                      (asIso ((forget SimplexCategory).map f))) _).symm

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map, CategoryTheory.forget, SimplexCategory, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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₂ =
    (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:
exact (ConcreteCategory.congr_hom (Iso.inv_hom_id
                      (asIso ((forget SimplexCategory).map f))) _).symm

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map, CategoryTheory.forget, SimplexCategory, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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₁ =
    (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:
(ConcreteCategory.congr_hom (Iso.inv_hom_id
                      (asIso ((forget SimplexCategory).map f))) _).symm

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map, CategoryTheory.forget, SimplexCategory, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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₁ =
    (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:
exact (ConcreteCategory.congr_hom (Iso.inv_hom_id
                      (asIso ((forget SimplexCategory).map f))) _).symm

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map, CategoryTheory.forget, SimplexCategory, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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' := ⋯ }) :
            (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))
⊢ 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

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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' := ⋯ }) :
          (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:
Iso.hom_inv_id_apply (asIso ((forget _).map f)) x

Premises used: CategoryTheory.Functor.map, CategoryTheory.Iso.hom_inv_id_apply, CategoryTheory.forget, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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' := ⋯ }) :
          (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:
exact Iso.hom_inv_id_apply (asIso ((forget _).map f)) x

Premises used: CategoryTheory.Functor.map, CategoryTheory.Iso.hom_inv_id_apply, CategoryTheory.forget, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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' := ⋯ } ≫
                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))
⊢ 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

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
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' := ⋯ } ≫
              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:
Iso.inv_hom_id_apply (asIso ((forget _).map f)) x

Premises used: CategoryTheory.Functor.map, CategoryTheory.forget, CategoryTheory.Iso.inv_hom_id_apply, CategoryTheory.asIso