awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
mp :
  (∃ (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⦌)
mpr :
  (∃ (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⦌)) →
    ∃ (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) (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⦌)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : A.toSSet _⦋m⦌
⊢ ∃ (m_1 : ℕ) (_ : m_1 < n) (f_1 : ⦋n⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m_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⦌)))
      (↑((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⦌))
            y) :
        X _⦋n⦌)

Tactic:
⟨m, hm, f, inferInstance, y.val, rfl⟩

Premises used: inferInstance, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : A.toSSet _⦋m⦌
⊢ ∃ (m_1 : ℕ) (_ : m_1 < n) (f_1 : ⦋n⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1),
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (X _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (X _⦋m_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⦌)))
      (↑((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⦌))
            y) :
        X _⦋n⦌)

Tactic:
exact ⟨m, hm, f, inferInstance, y.val, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
mpr :
  ∀ (x : X _⦋n⦌) (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋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⦌)))
          (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx) :
            X _⦋n⦌)) →
      ∃ (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⦌)))
          (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx)
⊢ (∃ (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⦌)) →
    ∃ (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

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
hx :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((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 :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ ∃ (m_1 : ℕ) (_ : m_1 < n) (f_1 : ⦋n⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1),
    Membership.mem (α := A.toSSet _⦋n⦌) (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m_1⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f_1.op)) :
          (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m_1⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) 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)
          hx :
        { x : X _⦋n⦌ // Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x })

Tactic:
⟨m, hm, f, inferInstance, ⟨y, ?_⟩, rfl⟩

Premises used: inferInstance, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
hx :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((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 :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
mpr : Membership.mem (γ := Set (X _⦋m⦌)) (A.obj (op ⦋m⦌)) y
⊢ ∃ (m_1 : ℕ) (_ : m_1 < n) (f_1 : ⦋n⦌ ⟶ ⦋m_1⦌) (_ : Epi f_1),
    Membership.mem (α := A.toSSet _⦋n⦌) (γ := Set ((fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Set.range (ι := (fun (X : Type u) ↦ X) (A.toSSet _⦋m_1⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (A.toSSet.map f_1.op)) :
          (a : (fun (X : Type u) ↦ X) (A.toSSet _⦋m_1⦌)) → (fun (X : Type u) ↦ X) (A.toSSet _⦋n⦌)))
      (Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) 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)
          hx :
        { x : X _⦋n⦌ // Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x })

Tactic:
refine ⟨m, hm, f, inferInstance, ⟨y, ?_⟩, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
hx :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((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 :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ IsSplitEpi f

Tactic:
have := isSplitEpi_of_epi f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : X _⦋m⦌
hx :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((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 :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
this : IsSplitEpi f
⊢ Membership.mem (γ := Set (X _⦋m⦌)) (A.obj (op ⦋m⦌)) y

Tactic:
simpa [Set.mem_preimage, ← op_comp, ← comp_apply, ← Functor.map_comp] using
      A.map (section_ f).op hx

Premises used: CategoryTheory.op_comp, Quiver.Hom.op, CategoryTheory.Subfunctor.map, CategoryTheory.comp_apply, CategoryTheory.section_, CategoryTheory.Functor.map_comp, Set.mem_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
x : (↑(A.obj (op ⦋n⦌)) : Type u)
rw : x ∉ A.toSSet.degenerate n ↔ (↑x : X _⦋n⦌) ∈ X.nonDegenerate n
rw₁ : x ∉ A.toSSet.degenerate n ↔ (↑x : X _⦋n⦌) ∉ X.degenerate n
rw₂ rw₃ : (↑x : X _⦋n⦌) ∉ X.degenerate n ↔ (↑x : X _⦋n⦌) ∉ X.degenerate n
⊢ Membership.mem (γ := Set (↑(A.obj (op ⦋n⦌)) : Type u)) (A.toSSet.nonDegenerate n) x ↔
    (↑x : X _⦋n⦌) ∈ X.nonDegenerate n

Tactic:
rw [mem_nonDegenerate_iff_notMem_degenerate,
    mem_nonDegenerate_iff_notMem_degenerate, mem_degenerate_iff]

Premises used: SSet.Subcomplex.mem_degenerate_iff, SSet.mem_nonDegenerate_iff_notMem_degenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
mp :
  A ≤ B →
    ∀ (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⦌)
mpr :
  (∀ (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
⊢ A ≤ B ↔
    ∀ (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⦌)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
⊢ A ≤ B →
    ∀ (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⦌)

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n : ℕ
x : X _⦋n⦌
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
mpr :
  ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌),
    Epi f →
      ∀ (a : A.toSSet _⦋m⦌) (ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a)
        (ha' :
          Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx =
            (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⦌))
              (↑(Subtype.mk (p := fun (x : A.toSSet _⦋m⦌) ↦
                    Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) x) a ha) :
                A.toSSet _⦋m⦌)),
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x

Tactic:
obtain ⟨m, f, _, ⟨a, ha⟩, ha'⟩ := exists_nonDegenerate A ⟨x, hx⟩

Premises used: SSet.Subcomplex.toSSet, SSet.exists_nonDegenerate, Subtype.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n : ℕ
x : X _⦋n⦌
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a
ha' :
  Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x) x hx =
    (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⦌))
      (↑(Subtype.mk (p := fun (x : A.toSSet _⦋m⦌) ↦
            Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) x) a ha) :
        A.toSSet _⦋m⦌)
⊢ x =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)

Tactic:
simp only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
      Subfunctor.toFunctor_map] at ha'

Premises used: CategoryTheory.Subfunctor.toFunctor_obj, CategoryTheory.Subfunctor.toFunctor_map, Subtype.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n : ℕ
x : X _⦋n⦌
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a
ha' :
  x =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
mpr :
  ∀
    (hx :
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                    Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌))
                      ⋯) :
                (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
              a) :
          X _⦋n⦌)),
    Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌))
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                  Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
              (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
            a) :
        X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x

Tactic:
subst ha'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a
hx :
  Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
⊢ (↑a : X _⦋m⦌) ∈ X.nonDegenerate m

Tactic:
rw [mem_nonDegenerate_iff] at ha

Premises used: SSet.Subcomplex.mem_nonDegenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : Membership.mem (γ := Set (A.toSSet _⦋m⦌)) (A.toSSet.nonDegenerate m) a
hx :
  Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
ha₁ : (↑a : X _⦋m⦌) ∈ X.nonDegenerate m
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)

Tactic:
rw [mem_nonDegenerate_iff] at ha

Premises used: SSet.Subcomplex.mem_nonDegenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : (↑a : X _⦋m⦌) ∈ X.nonDegenerate m
hx :
  Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)

Tactic:
B.map f.op (h _ ⟨_, ha⟩ a.prop)

Premises used: Set.Mem, Quiver.Hom.op, setOf, CategoryTheory.Subfunctor.map, Subtype.mk, Set.preimage, Subtype.prop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
a : A.toSSet _⦋m⦌
ha : (↑a : X _⦋m⦌) ∈ X.nonDegenerate m
hx :
  Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(A.obj (op ⦋m⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : X _⦋n⦌) ↦ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑x : X _⦋m⦌)) ⋯) :
            (a : (↑(A.obj (op ⦋m⦌)) : Type u)) → (↑(A.obj (op ⦋n⦌)) : Type u))
          a) :
      X _⦋n⦌)

Tactic:
exact B.map f.op (h _ ⟨_, ha⟩ a.prop)

Premises used: Quiver.Hom.op, CategoryTheory.Subfunctor.map, Subtype.mk, Subtype.prop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (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⦌)
n : SimplexCategory
x : X.obj (op n)
hx : Membership.mem (γ := Set (X.obj (op n))) (A.obj (op n)) x
mpr :
  ∀ (n : ℕ) ⦃x : X _⦋n⦌⦄ (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x),
    Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (op ⦋n⦌)) x
⊢ Membership.mem (γ := Set (X.obj (op n))) (B.obj (op n)) x

Tactic:
induction n using SimplexCategory.rec with | _ n =>
    obtain ⟨m, f, _, ⟨a, ha⟩, ha'⟩ := exists_nonDegenerate A ⟨x, hx⟩
    simp only [Subfunctor.toFunctor_obj, Subtype.ext_iff,
      Subfunctor.toFunctor_map] at ha'
    subst ha'
    rw [mem_nonDegenerate_iff] at ha
    exact B.map f.op (h _ ⟨_, ha⟩ a.prop)

Premises used: SSet.Subcomplex.toSSet, CategoryTheory.Subfunctor.toFunctor_obj, SSet.exists_nonDegenerate, CategoryTheory.Subfunctor.toFunctor_map, SSet.Subcomplex.mem_nonDegenerate_iff, Subtype.ext_iff, Subtype.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
⊢ A = ⊤ ↔ ∀ (n : ℕ), X.nonDegenerate n ⊆ A.obj (op ⦋n⦌)

Tactic:
simpa using le_iff_contains_nonDegenerate ⊤ A

Premises used: SSet.Subcomplex.le_iff_contains_nonDegenerate, Top.top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
mp : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤ → X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)
mpr : X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌) → Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤ ↔ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
Goal:
X : SSet
A : X.Subcomplex
n : ℕ
h : Eq.{u + 1} (α := Set (A.toSSet _⦋n⦌)) (A.toSSet.degenerate n) ⊤
mp : ∀ (x : X _⦋n⦌), x ∈ X.degenerate n ⊓ A.obj (op ⦋n⦌) ↔ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (op ⦋n⦌)) x
⊢ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

Tactic:
ext x