awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf₁ : SplitEpi f₁
hf₁' :
  (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (m + 1)) → Fin (n + 1))
      ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x) =
    x
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))

Tactic:
simpa [g, hf₁'] using (SimplexCategory.congr_toOrderHom_apply (g_eq_id hy₁ hy₂ hf₁)
      (f₁.toOrderHom x)).symm

Premises used: SimplexCategory.congr_toOrderHom_apply, _private.0.SSet.unique_nonDegenerate.g_eq_id, _private.0.SSet.unique_nonDegenerate.g, SimplexCategory.Hom.toOrderHom, Eq.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
a :
  ∃ (hf₁ : SplitEpi f₁),
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom f₂ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))

Tactic:
suffices ∃ (hf₁ : SplitEpi f₁), hf₁.section_.toOrderHom (f₁.toOrderHom x) = x by
    obtain ⟨hf₁, hf₁'⟩ := this
    dsimp at hf₁'
    simpa [g, hf₁'] using (SimplexCategory.congr_toOrderHom_apply (g_eq_id hy₁ hy₂ hf₁)
      (f₁.toOrderHom x)).symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
a :
  ∀ (hf : SplitEpi f₁),
    ∃ (hf₁ : SplitEpi f₁),
      (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
        x
⊢ ∃ (hf₁ : SplitEpi f₁),
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x

Tactic:
obtain ⟨⟨hf⟩⟩ := isSplitEpi_of_epi f₁

Premises used: CategoryTheory.isSplitEpi_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
y : Fin (m + 1)
dsimp :
  (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1))
      (if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x then x
      else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (m + 1)) → Fin (n + 1)) y) =
    y
⊢ (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y

Tactic:
dsimp [α]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
y : Fin (m + 1)
pos :
  ∀ (hy : y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x),
    (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x = y
neg :
  ∀ (hy : ¬y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x),
    (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1))
        ((SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (m + 1)) → Fin (n + 1)) y) =
      y
⊢ (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1))
      (if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x then x
      else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (m + 1)) → Fin (n + 1)) y) =
    y

Tactic:
split_ifs with hy
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
y : Fin (m + 1)
hy : y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x
pos pos₁ :
  Eq (α := Fin (m + 1)) ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x : Fin (m + 1))
    ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x : Fin (m + 1))
⊢ (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x = y

Tactic:
rw [hy]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
y : Fin (m + 1)
hy : ¬y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1)) x
⊢ (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (n + 1)) → Fin (m + 1))
      ((SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (m + 1)) → Fin (n + 1)) y) =
    y

Tactic:
apply SimplexCategory.congr_toOrderHom_apply hf.id

Premises used: CategoryTheory.SplitEpi.id, SimplexCategory.congr_toOrderHom_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
⊢ ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y

Tactic:
have hα₁ (y : Fin (m + 1)) : f₁.toOrderHom (α y) = y := by
    dsimp [α]
    split_ifs with hy
    · rw [hy]
    · apply SimplexCategory.congr_toOrderHom_apply hf.id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁_1 : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁_1 : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂_1 : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂_1 : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
by_contra! : ∀ (h' : α y₂ < α y₁), False
⊢ α y₁ ≤ α y₂

Tactic:
by_contra! h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁_1 : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁_1 : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂_1 : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂_1 : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
this : y₂ ≤ y₁
⊢ y₁ = y₂

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁_1 : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁_1 : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂_1 : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂_1 : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
this : y₂ ≤ y₁
⊢ False

Tactic:
simp [show y₁ = y₂ by lia] at h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁_1 : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁_1 : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂_1 : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂_1 : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
suffices : y₂ ≤ y₁
⊢ False

Tactic:
suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by lia] at h'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁_1 : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁_1 : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂_1 : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂_1 : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
⊢ y₂ ≤ y₁

Tactic:
simpa only [hα₁] using f₁.toOrderHom.monotone h'.le

Premises used: OrderHom.monotone, LT.lt.le, SimplexCategory.Hom.toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
⊢ Monotone α

Tactic:
have hα₂ : Monotone α := by
    rintro y₁ y₂ h
    by_contra! h'
    suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by lia] at h'
    simpa only [hα₁] using f₁.toOrderHom.monotone h'.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
hα₂ : Monotone α
a :
  ∀ (x : Fin (⦋m⦌.len + 1)),
    Eq (α := Fin (⦋m⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom
              (SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ : Fin (⦋m⦌.len + 1) →o Fin (⦋n⦌.len + 1) } ≫ f₁) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m⦌.len + 1))
          x :
        Fin (⦋m⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom (𝟙 ⦋m⦌) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x : Fin (⦋m⦌.len + 1))
⊢ SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ : Fin (⦋m⦌.len + 1) →o Fin (⦋n⦌.len + 1) } ≫ f₁ = 𝟙 ⦋m⦌

Tactic:
ext : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
hα₂ : Monotone α
x_2 : Fin (⦋m⦌.len + 1)
⊢ Eq (α := Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom
            (SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ : Fin (⦋m⦌.len + 1) →o Fin (⦋n⦌.len + 1) } ≫ f₁) :
          (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m⦌.len + 1))
        x_2 :
      Fin (⦋m⦌.len + 1))
    ((SimplexCategory.Hom.toOrderHom (𝟙 ⦋m⦌) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x_2 : Fin (⦋m⦌.len + 1))

Tactic:
apply hα₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
hα₂ : Monotone α
⊢ (SimplexCategory.Hom.toOrderHom
          (SplitEpi.section_ (f := f₁)
            { section_ := SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ }, id := ⋯ }) :
        (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
      ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
    x

Tactic:
simp [α]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x_1 : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f₁
y₁ : (↑(X.nonDegenerate m) : Type u)
hy₁ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₁.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₁ : X _⦋m⦌)
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : (↑(X.nonDegenerate m) : Type u)
hy₂ :
  x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f₂.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      (↑y₂ : X _⦋m⦌)
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : (y : Fin (m + 1)) → Fin (n + 1) :=
  fun (y : Fin (m + 1)) ↦
    if y = (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x then x
    else (SimplexCategory.Hom.toOrderHom hf.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) (α y) = y
hα₂ : Monotone α
⊢ ∃ (hf₁ : SplitEpi f₁),
    (SimplexCategory.Hom.toOrderHom hf₁.section_ : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((SimplexCategory.Hom.toOrderHom f₁ : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1)) x) =
      x

Tactic:
exact ⟨{ section_ := SimplexCategory.Hom.mk ⟨α, hα₂⟩, id := by ext : 3; apply hα₁ },
    by simp [α]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
rw :
  (∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
        x) ↔
    ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f),
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌)))
        (↑x : X _⦋n⦌)
⊢ Membership.mem (γ := Set (↑(A.obj (op ⦋n⦌)) : Type u)) (A.toSSet.degenerate n) x ↔ (↑x : X _⦋n⦌) ∈ X.degenerate n

Tactic:
rw [SSet.mem_degenerate_iff, SSet.mem_degenerate_iff]

Premises used: SSet.mem_degenerate_iff