awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf : Epi f
y : X _⦋m⦌
h :
  ∀ (i : Fin (n + 1)) (θ : ⦋n⦌ ⟶ ⦋m⦌) (hf : Epi (SimplexCategory.σ i ≫ θ)),
    Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌))
      (⋃ (i : Fin (n + 1)),
        Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i ≫ θ).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
          y :
        (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
⊢ Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 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 + 1⦌))
        y :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))

Tactic:
obtain ⟨i, θ, rfl⟩ := SimplexCategory.eq_σ_comp_of_not_injective f (fun hf ↦ by
      rw [← SimplexCategory.mono_iff_injective] at hf
      have := SimplexCategory.le_of_mono f
      lia)

Premises used: SimplexCategory.eq_σ_comp_of_not_injective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n m : ℕ
hm : m < n + 1
y : X _⦋m⦌
i : Fin (n + 1)
θ : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi (SimplexCategory.σ i ≫ θ)
⊢ Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i ≫ θ).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
        y :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx :
  Membership.mem (γ := Set (X _⦋n + 1⦌))
    (⋃ (i : Fin (n + 1)),
      Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)))
    x
⊢ ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x

Tactic:
simp only [Set.mem_iUnion, Set.mem_range] at hx

Premises used: Set.mem_range, Set.mem_iUnion
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx :
  ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
h :
  ∀ (i : Fin (n + 1)) (y : X _⦋n⦌),
    Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y : X _⦋n + 1⦌)
⊢ Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1)) x

Tactic:
obtain ⟨i, y, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
i : Fin (n + 1)
y : X _⦋n⦌
⊢ Membership.mem (α := X _⦋n + 1⦌) (γ := Set (X _⦋n + 1⦌)) (X.degenerate (n + 1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y : X _⦋n + 1⦌)

Tactic:
apply σ_mem_degenerate

Premises used: SSet.σ_mem_degenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
⊢ Membership.mem (γ := Set (X _⦋0⦌)) (X.nonDegenerate 0) x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
⊢ x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋0⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      (↑(Subtype.mk (p := fun (x : X _⦋0⦌) ↦ Membership.mem (γ := Set (X _⦋0⦌)) (X.nonDegenerate 0) x) x ⋯) : X _⦋0⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋0⦌
⊢ ∃ (m : ℕ) (f : ⦋0⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
        (↑y : X _⦋m⦌)

Tactic:
exact ⟨0, 𝟙 _, inferInstance, ⟨x, by simp⟩, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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 : X _⦋n + 1⦌
pos :
  ∀ (hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x),
    ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
          (↑y : X _⦋m⦌)
neg :
  ∀ (hx : x ∉ X.nonDegenerate (n + 1)),
    ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
          (↑y : X _⦋m⦌)
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
        (↑y : X _⦋m⦌)

Tactic:
by_cases hx : x ∈ X.nonDegenerate (n + 1)

Premises used: SSet.nonDegenerate, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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 : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
⊢ x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (𝟙 ⦋n + 1⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
      (↑(Subtype.mk (p := fun (x : X _⦋n + 1⦌) ↦ Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x) x
            hx) :
        X _⦋n + 1⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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 : X _⦋n + 1⦌
hx : Membership.mem (γ := Set (X _⦋n + 1⦌)) (X.nonDegenerate (n + 1)) x
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
        (↑y : X _⦋m⦌)

Tactic:
exact ⟨n + 1, 𝟙 _, inferInstance, ⟨x, hx⟩, by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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 : X _⦋n + 1⦌
hx : x ∉ X.nonDegenerate (n + 1)
⊢ ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x

Tactic:
simp only [← mem_degenerate_iff_notMem_nonDegenerate,
          degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx

Premises used: Set.mem_range, SSet.mem_degenerate_iff_notMem_nonDegenerate, Set.mem_iUnion, SSet.degenerate_eq_iUnion_range_σ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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 : X _⦋n + 1⦌
hx :
  ∃ (i : Fin (n + 1)) (y : X _⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y = x
neg :
  ∀ (i : Fin (n + 1)) (y : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y_1 : (↑(X.nonDegenerate m) : Type u)),
      Eq (α := X _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y : X _⦋n + 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 + 1⦌))
            (↑y_1 : X _⦋m⦌) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
        (↑y : X _⦋m⦌)

Tactic:
obtain ⟨i, y, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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⦌)
i : Fin (n + 1)
y : X _⦋n⦌
neg :
  ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (hf : Epi f) (z : (↑(X.nonDegenerate m) : Type u)),
    ∃ (m_1 : ℕ) (f_1 : ⦋n + 1⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1) (y : (↑(X.nonDegenerate m_1) : Type u)),
      Eq (α := X _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 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⦌))
                (↑z : X _⦋m⦌) :
              (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
          X _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m_1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
            (↑y : X _⦋m_1⦌) :
          (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
⊢ ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y_1 : (↑(X.nonDegenerate m) : Type u)),
    Eq (α := X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) y : X _⦋n + 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 + 1⦌))
          (↑y_1 : X _⦋m⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))

Tactic:
obtain ⟨m, f, hf, z, rfl⟩ := hn y

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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⦌)
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : (↑(X.nonDegenerate m) : Type u)
simp :
  Eq (α := X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑z : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑z : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n + 1⦌)
⊢ Eq (α := X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 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⦌))
            (↑z : X _⦋m⦌) :
          (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
      X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i ≫ f).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
        (↑z : X _⦋m⦌) :
      (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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⦌)
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : (↑(X.nonDegenerate m) : Type u)
⊢ Eq (α := X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑z : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n + 1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑z : X _⦋m⦌) : X _⦋n⦌) :
      X _⦋n + 1⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 n : ℕ
hn :
  ∀ (x : X _⦋n⦌),
    ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (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⦌)
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : (↑(X.nonDegenerate m) : Type u)
⊢ ∃ (m_1 : ℕ) (f_1 : ⦋n + 1⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1) (y : (↑(X.nonDegenerate m_1) : Type u)),
    Eq (α := X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X i) : (a : X _⦋n⦌) → X _⦋n + 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⦌))
              (↑z : X _⦋m⦌) :
            (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
        X _⦋n + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m_1⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
          (↑y : X _⦋m_1⦌) :
        (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))

Tactic:
exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
zero :
  ∀ (x : X _⦋0⦌),
    ∃ (m : ℕ) (f : ⦋0⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
          (↑y : X _⦋m⦌)
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (x : X _⦋n⦌),
        ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
          x =
            (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 : X _⦋n + 1⦌),
    ∃ (m : ℕ) (f : ⦋n + 1⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n + 1⦌))
          (↑y : X _⦋m⦌)
⊢ ∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : (↑(X.nonDegenerate m) : Type u)),
    x =
      (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⦌)

Tactic:
induction n with
  | zero =>
      exact ⟨0, 𝟙 _, inferInstance, ⟨x, by simp⟩, by simp⟩
  | succ n hn =>
      by_cases hx : x ∈ X.nonDegenerate (n + 1)
      · exact ⟨n + 1, 𝟙 _, inferInstance, ⟨x, hx⟩, by simp⟩
      · simp only [← mem_degenerate_iff_notMem_nonDegenerate,
          degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
        obtain ⟨i, y, rfl⟩ := hx
        obtain ⟨m, f, hf, z, rfl⟩ := hn y
        exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩

Premises used: Set.mem_range, SSet.mem_degenerate_iff_notMem_nonDegenerate, SSet.nonDegenerate, Set.mem_iUnion, HAdd.hAdd, SSet.degenerate_eq_iUnion_range_σ, OfNat.ofNat, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
inst : Epi f
y : X.obj (op m)
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑x : X _⦋n⦌)
obtain :
  ∀ (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n)
    (hy :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          y =
        (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)),
    IsIso f
⊢ IsIso f

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
m : SimplexCategory
f : ⦋n⦌ ⟶ m
inst : Epi f
y : X.obj (op m)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
hy :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (op m))) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
      y =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)
mk :
  ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) [Epi f] (y : X _⦋m⦌)
    (hy :
      (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 =
        (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)),
    IsIso f
⊢ IsIso f

Tactic:
induction m using SimplexCategory.rec with | _ m
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)
mk :
  ∀ (hx_1 : x ∉ X.degenerate n) (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) [Epi f] (y : X _⦋m⦌)
    (hy :
      (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 =
        (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌)),
    IsIso f
⊢ IsIso f

Tactic:
rw [mem_nonDegenerate_iff_notMem_degenerate] at hx

Premises used: SSet.mem_nonDegenerate_iff_notMem_degenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
mk : ∀ (hf : ¬IsIso f), False
⊢ IsIso f

Tactic:
by_contra hf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
hf : ¬IsIso f
⊢ False

Tactic:
hx ⟨_, not_le.1 (fun h ↦ hf ?_), f, y, hy⟩

Premises used: not_le, Exists.intro, Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
hf : ¬IsIso f
mk : ∀ (h : n ≤ m), IsIso f
⊢ False

Tactic:
refine hx ⟨_, not_le.1 (fun h ↦ hf ?_), f, y, hy⟩

Premises used: not_le, Exists.intro, Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
hf : ¬IsIso f
h : n ≤ m
mk : ⦋n⦌.len = ⦋m⦌.len
⊢ IsIso f

Tactic:
rw [SimplexCategory.isIso_iff_of_epi]

Premises used: SimplexCategory.isIso_iff_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
hf : ¬IsIso f
h : n ≤ m
⊢ ⦋n⦌.len = ⦋m⦌.len

Tactic:
le_antisymm h (SimplexCategory.len_le_of_epi f)

Premises used: SimplexCategory.len_le_of_epi, le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx : x ∉ X.degenerate n
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst : Epi f
y : X _⦋m⦌
hy :
  (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 =
    (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌)
hf : ¬IsIso f
h : n ≤ m
⊢ ⦋n⦌.len = ⦋m⦌.len

Tactic:
exact le_antisymm h (SimplexCategory.len_le_of_epi f)

Premises used: SimplexCategory.len_le_of_epi, le_antisymm