awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
f : x ⟶ y
hf : Function.Bijective (Hom.toOrderHom f).toFun
⊢ IsIso f

Tactic:
haveI : IsIso ((forget SimplexCategory).map f) := (isIso_iff_bijective _).mpr hf
  isIso_of_reflects_iso f (forget SimplexCategory)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.forget, SimplexCategory
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Mono f
⊢ IsIso f ↔ n.len = m.len

Tactic:
⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩

Premises used: Iff.intro, SimplexCategory.len_eq_of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Mono f
refine : ∀ (h : n.len = m.len), IsIso f
⊢ IsIso f ↔ n.len = m.len

Tactic:
refine ⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Mono f
h : n.len = m.len
⊢ n = m

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Mono f
h : n.len = m.len
obtain : ∀ (f : n ⟶ n) [hf : Mono f] (h : n.len = n.len), IsIso f
⊢ IsIso f

Tactic:
obtain rfl : n = m := by aesop

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : n ⟶ n
hf : Mono f
h : n.len = n.len
⊢ 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

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : n ⟶ n
hf : Mono f
h : n.len = n.len
hf₁ :
  Function.Injective (α := Fin (n.len + 1)) (β := Fin (n.len + 1))
    (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (n.len + 1))
⊢ n.len = n.len

Tactic:
rw [mono_iff_injective] at hf

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
rwa rwa₁ rwa₂ rwa₃ : Function.Injective (Hom.toOrderHom f).toFun
⊢ Function.Surjective (Hom.toOrderHom f).toFun

Tactic:
rwa [← Finite.injective_iff_surjective]

Premises used: Finite.injective_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
⊢ IsIso f

Tactic:
exact isIso_of_bijective ⟨hf, by rwa [← Finite.injective_iff_surjective]⟩

Premises used: SimplexCategory.isIso_of_bijective, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
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))
⊢ Mono (δ i)

Tactic:
rw [mono_iff_injective]

Premises used: SimplexCategory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
⊢ 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:
Fin.succAbove_right_injective

Premises used: Fin.succAbove, Fin.succAbove_right_injective, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
⊢ 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:
exact Fin.succAbove_right_injective

Premises used: Fin.succAbove_right_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Epi f
⊢ IsIso f ↔ n.len = m.len

Tactic:
⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩

Premises used: Iff.intro, SimplexCategory.len_eq_of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Epi f
refine : ∀ (h : n.len = m.len), IsIso f
⊢ IsIso f ↔ n.len = m.len

Tactic:
refine ⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Epi f
h : n.len = m.len
⊢ n = m

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n m : SimplexCategory
f : n ⟶ m
hf : Epi f
h : n.len = m.len
obtain : ∀ (f : n ⟶ n) [hf : Epi f] (h : n.len = n.len), IsIso f
⊢ IsIso f

Tactic:
obtain rfl : n = m := by aesop

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : n ⟶ n
hf : Epi f
h : n.len = n.len
⊢ 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

Premises used: SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : SimplexCategory
f : n ⟶ n
hf : Epi f
h : n.len = n.len
hf₁ :
  Function.Surjective (α := Fin (n.len + 1)) (β := Fin (n.len + 1))
    (⇑(Hom.toOrderHom f) : (a : Fin (n.len + 1)) → Fin (n.len + 1))
⊢ n.len = n.len

Tactic:
rw [epi_iff_surjective] at hf

Premises used: SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
rwa rwa₁ rwa₂ rwa₃ : Function.Surjective (Hom.toOrderHom f).toFun
⊢ Function.Injective (Hom.toOrderHom f).toFun

Tactic:
rwa [Finite.injective_iff_surjective]

Premises used: Finite.injective_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
⊢ IsIso f

Tactic:
exact isIso_of_bijective ⟨by rwa [Finite.injective_iff_surjective], hf⟩

Premises used: SimplexCategory.isIso_of_bijective, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X Y : SimplexCategory
f : X ⟶ Y
h : Mono f
h_1 : Epi f
rw : X.len = Y.len
⊢ IsIso f

Tactic:
rw [isIso_iff_of_epi]

Premises used: SimplexCategory.isIso_iff_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
X Y : SimplexCategory
f : X ⟶ Y
h : Mono f
h_1 : Epi 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:
X Y : SimplexCategory
f : X ⟶ Y
h : Mono f
h_1 : Epi f
⊢ X.len = Y.len

Tactic:
exact 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:
x y : SimplexCategory
e : x ≅ y
i : Fin (x.len + 1)
⊢ (Hom.toOrderHom e.inv : (a : Fin (y.len + 1)) → Fin (x.len + 1))
      ((Hom.toOrderHom e.hom : (a : Fin (x.len + 1)) → Fin (y.len + 1)) i) =
    i

Tactic:
simpa only using congr_arg (fun φ => (Hom.toOrderHom φ) i) e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, congr_arg, SimplexCategory.Hom.toOrderHom, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x y : SimplexCategory
e : x ≅ y
i : Fin (y.len + 1)
⊢ (Hom.toOrderHom e.hom : (a : Fin (x.len + 1)) → Fin (y.len + 1))
      ((Hom.toOrderHom e.inv : (a : Fin (y.len + 1)) → Fin (x.len + 1)) i) =
    i

Tactic:
simpa only using congr_arg (fun φ => (Hom.toOrderHom φ) i) e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, congr_arg, SimplexCategory.Hom.toOrderHom, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
e : x ≅ x
⊢ 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)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
⊢ 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)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
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
⊢ RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
      (orderIsoOfIso (Iso.refl x)) =
    Finset.orderEmbOfFin Finset.univ h

Tactic:
have eq₂ :=
    Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso (Iso.refl x)) i)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
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
eq₂ :
  RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
      (orderIsoOfIso (Iso.refl x)) =
    Finset.orderEmbOfFin Finset.univ h
w :
  ∀ (x_1 : Fin (x.len + 1)),
    Eq (α := Fin (x.len + 1)) ((Hom.toOrderHom e.hom : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))
      ((Hom.toOrderHom (Iso.hom (Iso.refl x)) : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))
⊢ e = Iso.refl x

Tactic:
ext : 4
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
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
eq₂ :
  RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
      (orderIsoOfIso (Iso.refl x)) =
    Finset.orderEmbOfFin Finset.univ h
x_1 : Fin (x.len + 1)
⊢ Eq (α := Fin (x.len + 1)) ((Hom.toOrderHom e.hom : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))
    ((Hom.toOrderHom (Iso.hom (Iso.refl x)) : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))

Tactic:
DFunLike.congr_fun (eq₁.trans eq₂.symm) _

Premises used: DFunLike.congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
e : x ≅ x
h : Finset.card (α := Fin (x.len + 1)) Finset.univ = x.len + 1
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
eq₂ :
  RelIso.toRelEmbedding (r := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (x.len + 1)) ↦ x1 ≤ x2)
      (orderIsoOfIso (Iso.refl x)) =
    Finset.orderEmbOfFin Finset.univ h
x_1 : Fin (x.len + 1)
⊢ Eq (α := Fin (x.len + 1)) ((Hom.toOrderHom e.hom : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))
    ((Hom.toOrderHom (Iso.hom (Iso.refl x)) : (a : Fin (x.len + 1)) → Fin (x.len + 1)) x_1 : Fin (x.len + 1))

Tactic:
exact DFunLike.congr_fun (eq₁.trans eq₂.symm) _

Premises used: DFunLike.congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
x : SimplexCategory
f : x ⟶ x
inst : IsIso f
⊢ f = 𝟙 x

Tactic:
congr_arg (fun φ : _ ≅ _ => φ.hom) (iso_eq_iso_refl (asIso f))

Premises used: congr_arg, SimplexCategory.iso_eq_iso_refl, CategoryTheory.Iso.hom, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
h : θ = σ i ≫ δ i.succ ≫ θ
⊢ ∃ (θ' : ⦋n⦌ ⟶ Δ'), θ = σ i ≫ θ'

Tactic:
use δ i.succ ≫ θ

Premises used: Fin.succ, SimplexCategory.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
h :
  ∀ (x : Fin (⦋n + 1⦌.len + 1)),
    Eq (α := Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
      ((Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
⊢ θ = σ i ≫ δ i.succ ≫ θ

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))

Tactic:
simp only [len_mk, σ, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    Function.comp_apply, Fin.predAboveOrderHom_coe]

Premises used: SimplexCategory.len_mk, SimplexCategory.mkHom, SimplexCategory.σ, Fin.predAboveOrderHom_coe, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe, Function.comp_apply, SimplexCategory.comp_toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
pos :
  ∀ (h' : x ≤ i.castSucc),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
          ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
        Fin (Δ'.len + 1))
neg :
  ∀ (h' : ¬x ≤ i.castSucc),
    Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
      ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
          ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
        Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))

Tactic:
by_cases h' : x ≤ Fin.castSucc i

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
pos :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (x.castPred ⋯)) :
      Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (i.predAbove x)) :
      Fin (Δ'.len + 1))

Tactic:
rw [Fin.predAbove_of_le_castSucc i x h']

Premises used: Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
pos :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (i.succ.succAbove (x.castPred ⋯)) : Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1))
        ((Hom.toOrderHom (δ i.succ) : (a : Fin (n + 1)) → Fin (n + 1 + 1)) (x.castPred ⋯)) :
      Fin (Δ'.len + 1))

Tactic:
dsimp [δ]

Premises used: SimplexCategory.δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
pos :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))
rw : (x.castPred ⋯).castSucc < i.succ
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (i.succ.succAbove (x.castPred ⋯)) : Fin (Δ'.len + 1))

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ _]

Premises used: Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
pos pos₁ :
  Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
⊢ Eq (α := Fin (Δ'.len + 1)) ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) x : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (n + 1 + 1)) → Fin (Δ'.len + 1)) (x.castPred ⋯).castSucc : Fin (Δ'.len + 1))

Tactic:
rw [Fin.castSucc_castPred]

Premises used: Fin.castSucc_castPred
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (x.castPred ⋯).castSucc < i.succ

Tactic:
(Fin.castSucc_lt_succ_iff.mpr h')

Premises used: Iff.mpr, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (x.castPred ⋯).castSucc < i.succ

Tactic:
exact (Fin.castSucc_lt_succ_iff.mpr h')

Premises used: Iff.mpr, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : ¬x ≤ i.castSucc
⊢ i.castSucc < x

Tactic:
simp only [not_le] at h'

Premises used: not_le
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
h' : i.castSucc < 0
⊢ False

Tactic:
simp at h'
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi :
  Eq (α := Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.castSucc : Fin (Δ'.len + 1))
    ((Hom.toOrderHom θ : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (Δ'.len + 1)) i.succ : Fin (Δ'.len + 1))
x : Fin (⦋n + 1⦌.len + 1)
h' : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
⊢ x = y.succ

Tactic:
have hy : x = y.succ := (Fin.succ_pred x _).symm