awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
x : X _⦋n⦌
mp : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x → x ∈ X.degenerate n
⊢ x ∈ X.degenerate n ⊓ A.obj (op ⦋n⦌) ↔ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x

Tactic:
simp only [Set.inf_eq_inter, Set.mem_inter_iff, and_iff_right_iff_imp]

Premises used: Set.mem_inter_iff, and_iff_right_iff_imp, Set.inf_eq_inter
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
x : X _⦋n⦌
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
⊢ x ∈ X.degenerate n

Tactic:
simp [← A.mem_degenerate_iff ⟨x, hx⟩, h, Set.top_eq_univ, Set.mem_univ]

Premises used: SSet.Subcomplex.mem_degenerate_iff, Set.top_eq_univ, Subtype.mk, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
⊢ A.obj (op ⦋n⦌) ⊆ X.degenerate n

Tactic:
simp only [Set.inf_eq_inter, Set.inter_eq_right] at h

Premises used: Set.inter_eq_right, Set.inf_eq_inter
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
mpr :
  ∀ (x : A.toSSet _⦋n⦌),
    Membership.mem (γ := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) x ↔ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) ⊤ x
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : A.obj (op ⦋n⦌) ⊆ X.degenerate n
x : A.toSSet _⦋n⦌
⊢ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) x ↔ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) ⊤ x

Tactic:
simpa [A.mem_degenerate_iff] using h x.prop

Premises used: SSet.Subcomplex.mem_degenerate_iff, Subtype.prop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
rw :
  ∀ (n : ℕ),
    X.nonDegenerate n ⊆
      Subfunctor.obj
        (⨆ (x : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
          ofSimplex (↑(x.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋x.fst⦌))
        (op ⦋n⦌)
⊢ Eq.{u + 1} (α := X.Subcomplex)
    (⨆ (x : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
      ofSimplex (↑(x.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋x.fst⦌))
    ⊤

Tactic:
rw [eq_top_iff_contains_nonDegenerate]

Premises used: SSet.Subcomplex.eq_top_iff_contains_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
simp : ∃ (a : ℕ), ∃ a_1 ∈ X.nonDegenerate a, Membership.mem (γ := Set (X _⦋n⦌)) ((ofSimplex a_1).obj (op ⦋n⦌)) x
⊢ Membership.mem (γ := Set (X _⦋n⦌))
    (Subfunctor.obj
      (⨆ (x : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
        ofSimplex (↑(x.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋x.fst⦌))
      (op ⦋n⦌))
    x

Tactic:
simp only [Subfunctor.iSup_obj, Set.mem_iUnion, Sigma.exists,
    Subtype.exists, exists_prop]

Premises used: Sigma.exists, Set.mem_iUnion, Subtype.exists, exists_prop, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ ∃ (a : ℕ), ∃ a_1 ∈ X.nonDegenerate a, Membership.mem (γ := Set (X _⦋n⦌)) ((ofSimplex a_1).obj (op ⦋n⦌)) x

Tactic:
⟨n, x, hx, mem_ofSimplex_obj x⟩

Premises used: And.intro, SSet.Subcomplex.mem_ofSimplex_obj, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ ∃ (a : ℕ), ∃ a_1 ∈ X.nonDegenerate a, Membership.mem (γ := Set (X _⦋n⦌)) ((ofSimplex a_1).obj (op ⦋n⦌)) x

Tactic:
exact ⟨n, x, hx, mem_ofSimplex_obj x⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.degenerate n
f : X ⟶ Y
obtain :
  ∀ (m : ℕ) (hm : m < n) (g : ⦋n⦌ ⟶ ⦋m⦌) (y : X _⦋m⦌),
    Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
              y :
            (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))

Tactic:
obtain ⟨m, hm, g, y, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
n : ℕ
f : X ⟶ Y
m : ℕ
hm : m < n
g : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
rw rw₁ :
  Eq (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map g.op) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋m⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋m⦌))
            y :
          (fun (X : Type u) ↦ X) (Y _⦋m⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map g.op) : (a : Y _⦋m⦌) → Y _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋m⦌)) : (a : X _⦋m⦌) → Y _⦋m⦌) y : Y _⦋m⦌) :
      Y _⦋n⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map g.op) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋m⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (Y _⦋m⦌))
            y :
          (fun (X : Type u) ↦ X) (Y _⦋m⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            y :
          (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))

Tactic:
rw [NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
n : ℕ
f : X ⟶ Y
m : ℕ
hm : m < n
g : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
            y :
          (fun (X : Type u) ↦ X) (X _⦋n⦌)) :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))

Tactic:
exact ⟨m, hm, g, f.app _ y, by rw [NatTrans.naturality_apply]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
f : X ⟶ Y
n : ℕ
⊢ X.degenerate n ⊆
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ⁻¹'
      Y.degenerate n

Tactic:
fun _ hx ↦ degenerate_app_apply hx f

Premises used: Set.Mem, setOf, Set.Subset, SSet.degenerate_app_apply, Set.preimage, SSet.degenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
f : X ⟶ Y
n : ℕ
⊢ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ''
      X.degenerate n ⊆
    Y.degenerate n

Tactic:
simpa using degenerate_le_preimage f n

Premises used: SSet.degenerate_le_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
n : ℕ
x : X _⦋n⦌
mp :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) →
    x ∈ X.degenerate n
mpr :
  x ∈ X.degenerate n →
    Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    x ∈ X.degenerate n

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
n : ℕ
x : X _⦋n⦌
hy :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ x ∈ X.degenerate n

Tactic:
simpa [← comp_apply, ← NatTrans.comp_app] using degenerate_app_apply hy (inv f)

Premises used: SSet.degenerate_app_apply, CategoryTheory.comp_apply, CategoryTheory.inv, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n →
    Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌))

Tactic:
fun hx ↦ degenerate_app_apply hx f

Premises used: SSet.degenerate_app_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n →
    Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌))

Tactic:
exact fun hx ↦ degenerate_app_apply hx f

Premises used: SSet.degenerate_app_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X Y : SSet
f : X ⟶ Y
inst : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    x ∈ X.nonDegenerate n

Tactic:
simp [mem_nonDegenerate_iff_notMem_degenerate,
    degenerate_iff_of_isIso]

Premises used: SSet.mem_nonDegenerate_iff_notMem_degenerate, SSet.degenerate_iff_of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x_1 : (↑(X.nonDegenerate n) : Type u)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Membership.mem (α := Y _⦋n⦌) (Y.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
y : Y _⦋n⦌
hy : y ∈ Y.nonDegenerate n
⊢ Membership.mem (α := X _⦋n⦌) (X.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        y :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
⊢ (fun (x : (↑(Y.nonDegenerate n) : Type u)) ↦
        (match (motive := (↑(Y.nonDegenerate n) : Type u) → (↑(X.nonDegenerate n) : Type u)) x with
          | ⟨y, hy⟩ =>
            Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (op ⦋n⦌)) :
                  (a : (fun (X : Type u) ↦ X) (Y _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                y)
              ⋯ :
          (↑(X.nonDegenerate n) : Type u)))
      ((fun (x : (↑(X.nonDegenerate n) : Type u)) ↦
          (match (motive := (↑(X.nonDegenerate n) : Type u) → (↑(Y.nonDegenerate n) : Type u)) x with
            | ⟨x, hx⟩ =>
              Subtype.mk (p := fun (x : Y _⦋n⦌) ↦ x ∈ Y.nonDegenerate n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
                  x)
                ⋯ :
            (↑(Y.nonDegenerate n) : Type u)))
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n_1 : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x : (↑(Y.nonDegenerate n) : Type u)
⊢ (fun (x : (↑(X.nonDegenerate n) : Type u)) ↦
        (match (motive := (↑(X.nonDegenerate n) : Type u) → (↑(Y.nonDegenerate n) : Type u)) x with
          | ⟨x, hx⟩ =>
            Subtype.mk (p := fun (x : Y _⦋n⦌) ↦ x ∈ Y.nonDegenerate n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (op ⦋n⦌)) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
                x)
              ⋯ :
          (↑(Y.nonDegenerate n) : Type u)))
      ((fun (x : (↑(Y.nonDegenerate n) : Type u)) ↦
          (match (motive := (↑(Y.nonDegenerate n) : Type u) → (↑(X.nonDegenerate n) : Type u)) x with
            | ⟨y, hy⟩ =>
              Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (Y _⦋n⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  y)
                ⋯ :
            (↑(X.nonDegenerate n) : Type u)))
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst : Mono f
x : X _⦋n⦌
rw :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.toRange f).app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Subcomplex.range f).toSSet _⦋n⦌))
            x) :
        Y _⦋n⦌) ∈
      Y.degenerate n
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    x ∈ X.degenerate n

Tactic:
rw [← degenerate_iff_of_isIso (Subcomplex.toRange f) x,
    Subcomplex.mem_degenerate_iff]

Premises used: SSet.Subcomplex.toRange, SSet.Subcomplex.mem_degenerate_iff, SSet.degenerate_iff_of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst : Mono f
x : X _⦋n⦌
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.degenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.toRange f).app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Subcomplex.range f).toSSet _⦋n⦌))
            x) :
        Y _⦋n⦌) ∈
      Y.degenerate n

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst : Mono f
x : X _⦋n⦌
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)) ↔
    x ∈ X.nonDegenerate n

Tactic:
simp [mem_nonDegenerate_iff_notMem_degenerate, degenerate_iff_of_mono]

Premises used: SSet.degenerate_iff_of_mono, SSet.mem_nonDegenerate_iff_notMem_degenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
⊢ X.degenerate n = Set.univ

Tactic:
HasDimensionLT.degenerate_eq_top n hn

Premises used: SSet.HasDimensionLT.degenerate_eq_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
⊢ X.nonDegenerate n = ∅

Tactic:
simp [nonDegenerate, X.degenerate_eq_univ_of_hasDimensionLT d n hn]

Premises used: SSet.nonDegenerate, SSet.degenerate_eq_univ_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
d : ℕ
inst : X.HasDimensionLT d
by_contra! : ∀ (this : d ≤ n), False
⊢ n < d

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
d : ℕ
inst : X.HasDimensionLT d
this : d ≤ n
obtain : ∀ (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
n d : ℕ
inst : X.HasDimensionLT d
this : d ≤ n
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ False

Tactic:
simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d n this] at hx

Premises used: SSet.nonDegenerate_eq_empty_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
d : ℕ
inst : X.HasDimensionLE d
⊢ n ≤ d

Tactic:
Nat.le_of_lt_succ (X.dim_lt_of_nonDegenerate x (d + 1))

Premises used: SSet.dim_lt_of_nonDegenerate, HAdd.hAdd, Nat.le_of_lt_succ, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
n : ℕ
inst_1 : X.HasDimensionLT n
k : ℕ
⊢ X.HasDimensionLT (n + k)

Tactic:
X.hasDimensionLT_of_le n _

Premises used: SSet.hasDimensionLT_of_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
A : X.Subcomplex
n : ℕ
hd : d ≤ n
h :
  ∀ (x : A.toSSet _⦋n⦌),
    Membership.mem (γ := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) x ↔ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) ⊤ x
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
d : ℕ
inst : X.HasDimensionLT d
A : X.Subcomplex
n : ℕ
hd : d ≤ n
x : A.toSSet _⦋n⦌
⊢ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) x ↔ Membership.mem (γ := Set (A.toSSet _⦋n⦌)) ⊤ x

Tactic:
simp [A.mem_degenerate_iff, X.degenerate_eq_univ_of_hasDimensionLT d n hd]

Premises used: SSet.degenerate_eq_univ_of_hasDimensionLT, SSet.Subcomplex.mem_degenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
A B : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
⊢ A ≤ B ↔ ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)

Tactic:
⟨fun h i hi a ⟨ha, _⟩ ↦ h _ ha, fun h ↦ ?_⟩

Premises used: Membership.mem, CategoryTheory.Subfunctor.obj, _private.0.SSet.Subcomplex.le_iff_of_hasDimensionLT.match_1, SimplexCategory.mk, Opposite.op, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
A B : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
refine : ∀ (h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)), A ≤ B
⊢ A ≤ B ↔ ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)

Tactic:
refine ⟨fun h i hi a ⟨ha, _⟩ ↦ h _ ha, fun h ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
A B : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)
rw :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ A ≤ B

Tactic:
rw [le_iff_contains_nonDegenerate]

Premises used: SSet.Subcomplex.le_iff_contains_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
A B : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)

Tactic:
h _ (X.dim_lt_of_nonDegenerate x d) ⟨hx, x.prop⟩

Premises used: SSet.dim_lt_of_nonDegenerate, Subtype.prop, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
A B : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) (↑x : X _⦋n⦌)

Tactic:
exact h _ (X.dim_lt_of_nonDegenerate x d) ⟨hx, x.prop⟩

Premises used: SSet.dim_lt_of_nonDegenerate, Subtype.prop, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X : SSet
A : X.Subcomplex
d : ℕ
inst : X.HasDimensionLT d
⊢ A = ⊤ ↔ ∀ i < d, X.nonDegenerate i ⊆ A.obj (op ⦋i⦌)

Tactic:
simp [← top_le_iff, le_iff_of_hasDimensionLT ⊤ A d]

Premises used: SSet.Subcomplex.le_iff_of_hasDimensionLT, top_le_iff, Top.top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
d : ℕ
inst_1 : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
h : ∀ (x : X _⦋n⦌), x ∈ X.degenerate n ↔ Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x
⊢ X.degenerate n = ⊤

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
d : ℕ
inst_1 : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
h :
  Membership.mem (γ := Set (Y _⦋n⦌)) Set.univ
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.toRange f).app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Subcomplex.range f).toSSet _⦋n⦌))
            x) :
        Y _⦋n⦌) ↔
    Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x
⊢ x ∈ X.degenerate n ↔ Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x

Tactic:
rw [← degenerate_iff_of_isIso (Subcomplex.toRange f),
      Subcomplex.mem_degenerate_iff, Y.degenerate_eq_univ_of_hasDimensionLT d n hn]

Premises used: SSet.Subcomplex.toRange, SSet.degenerate_eq_univ_of_hasDimensionLT, SSet.Subcomplex.mem_degenerate_iff, SSet.degenerate_iff_of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
d : ℕ
inst_1 : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ Membership.mem (γ := Set (Y _⦋n⦌)) Set.univ
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.toRange f).app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Subcomplex.range f).toSSet _⦋n⦌))
            x) :
        Y _⦋n⦌) ↔
    Membership.mem (γ := Set (X _⦋n⦌)) ⊤ x

Tactic:
simp