awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
change :
  Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i ≫ f.app (op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌) ≫ SimplicialObject.σ T i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ T i) :
          (a : (fun (X : Type u_1) ↦ X) (T _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
            x :
          (fun (X : Type u_1) ↦ X) (T _⦋n⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))

Tactic:
change (S.σ i ≫ f.app (op ⦋n + 1⦌)) x = (f.app (op ⦋n⦌) ≫ T.σ i) x

Premises used: CategoryTheory.ConcreteCategory.hom, HAdd.hAdd, SimplexCategory.mk, Opposite.op, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, DFunLike.coe, CategoryTheory.NatTrans.app, CategoryTheory.SimplicialObject.σ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i ≫ f.app (op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌) ≫ SimplicialObject.σ T i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))

Tactic:
congr_hom (SimplicialObject.σ_naturality f i) x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i ≫ f.app (op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌) ≫ SimplicialObject.σ T i) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        x :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))

Tactic:
exact congr_hom (SimplicialObject.σ_naturality f i) x

Premises used: CategoryTheory.SimplicialObject.σ_naturality, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
obj :
  ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Δ[n].obj x),
    x_1 ∈ ∂Δ[n].obj x ↔
      Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ) x) x_1
⊢ ∂Δ[n] = ⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
obj :
  (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) ↔
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
⊢ x_1 ∈ ∂Δ[n].obj x ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ) x) x_1

Tactic:
simp [stdSimplex.face_obj, boundary, Function.Surjective]

Premises used: SSet.stdSimplex.face_obj, SSet.boundary, Function.Surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
rw : ∀ (i : Fin (n + 1)), HasDimensionLT.{u_1} (Subcomplex.toSSet (X := Δ[n]) (stdSimplex.face {i}ᶜ)) n
⊢ HasDimensionLT.{u_1} ∂Δ[n].toSSet n

Tactic:
rw [boundary_eq_iSup, hasDimensionLT_iSup_iff]

Premises used: SSet.hasDimensionLT_iSup_iff, SSet.boundary_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Finset.card (α := Fin (n + 1)) {i}ᶜ ≤ n

Tactic:
simp [Finset.card_compl]

Premises used: Finset.card_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
⊢ HasDimensionLT.{u_1} (Subcomplex.toSSet (X := Δ[n]) (stdSimplex.face {i}ᶜ)) n

Tactic:
exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])

Premises used: SSet.stdSimplex.hasDimensionLT_face
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
rw :
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Subfunctor.obj (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ) (op ⦋d⦌)) s ↔
    ∃ (j : Fin (n + 1)), j ∉ Set.range (ι := Fin (d + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (∂Δ[n].obj (op ⦋d⦌)) s ↔
    ∃ (j : Fin (n + 1)), j ∉ Set.range (ι := Fin (d + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))

Tactic:
rw [boundary_eq_iSup]

Premises used: SSet.boundary_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Subfunctor.obj (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ) (op ⦋d⦌)) s ↔
    ∃ (j : Fin (n + 1)), j ∉ Set.range (ι := Fin (d + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
rw : LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ) (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ)
⊢ stdSimplex.face {i}ᶜ ≤ ∂Δ[n]

Tactic:
rw [boundary_eq_iSup]

Premises used: SSet.boundary_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
⊢ LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ) (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ)

Tactic:
le_iSup (fun (i : Fin (n +1)) ↦ stdSimplex.face {i}ᶜ) i

Premises used: Compl.compl, SSet.stdSimplex.face, le_iSup, Singleton.singleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
⊢ LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ) (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ)

Tactic:
exact le_iSup (fun (i : Fin (n +1)) ↦ stdSimplex.face {i}ᶜ) i

Premises used: Compl.compl, SSet.stdSimplex.face, le_iSup, Singleton.singleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
rw : ∀ (x : Fin (n + 1)), objMk OrderHom.id ∉ Subfunctor.obj (face {x}ᶜ) (op ⦋n⦌)
⊢ objMk OrderHom.id ∉ ∂Δ[n].obj (op ⦋n⦌)

Tactic:
rw [boundary_eq_iSup, Subfunctor.iSup_obj, Set.mem_iUnion, not_exists]

Premises used: Set.mem_iUnion, not_exists, SSet.boundary_eq_iSup, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
hi :
  Membership.mem (γ := Set (stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)) (Subfunctor.obj (face {i}ᶜ) (op ⦋n⦌))
    (objMk OrderHom.id)
⊢ Membership.mem (γ := Finset (Fin (⦋n⦌.len + 1)))
    (Finset.image (α := Fin ((unop (op ⦋n⦌)).len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom
            (((objEquiv : Δ[n] _⦋n⦌ ≃ (unop (op ⦋n⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋n⦌) → unop (op ⦋n⦌) ⟶ ⦋n⦌)
              (objMk OrderHom.id))) :
        (a : Fin ((unop (op ⦋n⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
      ⊤)
    i

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
hi :
  Membership.mem (γ := Set (stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)) (Subfunctor.obj (face {i}ᶜ) (op ⦋n⦌))
    (objMk OrderHom.id)
⊢ False

Tactic:
simpa using @hi i (by aesop)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
⊢ ∂Δ[n] ≤ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Subfunctor.obj ⊤ (op ⦋n⦌)) (stdSimplex.objMk OrderHom.id)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n
h₁ :
  ∀ (x : Δ[n] _⦋m⦌),
    Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x
⊢ Eq (α := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) Set.univ

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n
x : Δ[n] _⦋m⦌
h₁ :
  ∀ (f : unop (op ⦋m⦌) ⟶ ⦋n⦌),
    Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
      Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x ↔ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) Set.univ x

Tactic:
obtain ⟨f, rfl⟩ := stdSimplex.objEquiv.symm.surjective x

Premises used: Equiv.surjective, Equiv.symm, SSet.stdSimplex.objEquiv, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ :
  Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)
⊢ Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌) ↔
    Membership.mem.{u, u} (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) Set.univ
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)

Tactic:
simp only [Set.mem_univ, iff_true]

Premises used: iff_true, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ :
  ∀ (h : m < 0) (f : unop (op ⦋m⦌) ⟶ ⦋0⦌),
    Membership.mem.{u, u} (α := Δ[0] _⦋m⦌) (γ := Set (Δ[0] _⦋m⦌)) (Subfunctor.obj ∂Δ[0] (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋0⦌) → Δ[0] _⦋m⦌) f : Δ[0] _⦋m⦌)
h₂ :
  ∀ (n : ℕ) (h : m < n + 1) (f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌),
    Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) f : Δ[n + 1] _⦋m⦌)
⊢ Membership.mem (α := Δ[n] _⦋m⦌) (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) f : Δ[n] _⦋m⦌)

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m : ℕ
h : m < 0
f : unop (op ⦋m⦌) ⟶ ⦋0⦌
⊢ Membership.mem.{u, u} (α := Δ[0] _⦋m⦌) (γ := Set (Δ[0] _⦋m⦌)) (Subfunctor.obj ∂Δ[0] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋0⦌) → Δ[0] _⦋m⦌) f : Δ[0] _⦋m⦌)

Tactic:
simp at h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf :
  Function.Surjective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n + 1⦌.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n + 1⦌.len + 1))
⊢ Epi f

Tactic:
rw [← SimplexCategory.epi_iff_surjective] at hf

Premises used: SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Epi f
⊢ n + 1 ≤ m

Tactic:
have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Epi f
this : n + 1 ≤ m
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
h₁ :
  ∀ (i : Fin (n + 2)) (q : unop (op ⦋m⦌) ⟶ ⦋n⦌),
    Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)
⊢ Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) f : Δ[n + 1] _⦋m⦌)

Tactic:
obtain ⟨i, q, rfl⟩ := SimplexCategory.eq_comp_δ_of_not_surjective f (fun hf ↦ by
      rw [← SimplexCategory.epi_iff_surjective] at hf
      have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
      lia)

Premises used: SimplexCategory.eq_comp_δ_of_not_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ :
  Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj (stdSimplex.face {i}ᶜ) (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)
⊢ Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj ∂Δ[n + 1] (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)

Tactic:
apply face_singleton_compl_le_boundary i

Premises used: SSet.face_singleton_compl_le_boundary
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ :
  LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.map (SimplexCategory.δ i)).app (op ⦋m⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n + 1] _⦋m⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) q : Δ[n] _⦋m⦌)))
    (Subcomplex.ofSimplex (n := n)
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
⊢ Membership.mem.{u, u} (α := Δ[n + 1] _⦋m⦌) (γ := Set (Δ[n + 1] _⦋m⦌)) (Subfunctor.obj (stdSimplex.face {i}ᶜ) (op ⦋m⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : ⦋m⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋m⦌) (q ≫ SimplexCategory.δ i) : Δ[n + 1] _⦋m⦌)

Tactic:
rw [stdSimplex.face_singleton_compl, stdSimplex.objEquiv_symm_comp,
      ← Subcomplex.ofSimplex_le_iff]

Premises used: SSet.Subcomplex.ofSimplex_le_iff, SSet.stdSimplex.objEquiv_symm_comp, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m n : ℕ
h : m < n + 1
i : Fin (n + 2)
q : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((stdSimplex.map (SimplexCategory.δ i)).app (op ⦋m⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[n] _⦋m⦌)) → (fun (X : Type u) ↦ X) (Δ[n + 1] _⦋m⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋m⦌) ⟶ ⦋n⦌) → Δ[n] _⦋m⦌) q : Δ[n] _⦋m⦌)))
    (Subcomplex.ofSimplex (n := n)
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))

Tactic:
apply Subcomplex.ofSimplex_map_le

Premises used: SSet.Subcomplex.ofSimplex_map_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
obj :
  ∀ (m : SimplexCategoryᵒᵖ) (x : Δ[0].obj m),
    Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ∂Δ[0] m) x ↔
      Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ⊥ m) x
⊢ Eq.{u + 1} (α := Δ[0].Subcomplex) ∂Δ[0] ⊥

Tactic:
ext m x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m : SimplexCategoryᵒᵖ
x : Δ[0].obj m
obj :
  Function.Surjective (α := Fin ((unop m).len + 1)) (β := Fin 1)
    (⇑(stdSimplex.asOrderHom x) : (a : Fin ((unop m).len + 1)) → Fin 1)
⊢ Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ∂Δ[0] m) x ↔
    Membership.mem (γ := Set (Δ[0].obj m)) (Subfunctor.obj ⊥ m) x

Tactic:
simp only [boundary, Nat.reduceAdd, Set.mem_setOf_eq, Subfunctor.bot_obj, Set.bot_eq_empty,
    Set.mem_empty_iff_false, iff_false, Decidable.not_not]

Premises used: iff_false, Nat.reduceAdd, Set.mem_setOf_eq, Set.bot_eq_empty, CategoryTheory.Subfunctor.bot_obj, SSet.boundary, Set.mem_empty_iff_false, Decidable.not_not
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m : SimplexCategoryᵒᵖ
x_1 : Δ[0].obj m
x : Fin 1
⊢ (stdSimplex.asOrderHom x_1 : (a : Fin ((unop m).len + 1)) → Fin 1) 0 = x

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
m : SimplexCategoryᵒᵖ
x_1 : Δ[0].obj m
x : Fin 1
⊢ ∃ (a : Fin ((unop m).len + 1)), (stdSimplex.asOrderHom x_1 : (a : Fin ((unop m).len + 1)) → Fin 1) a = x

Tactic:
exact ⟨0, by subsingleton⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
obj :
  ∀ (d : ℕ) (j : Δ[n] _⦋d⦌),
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) ((∂Δ[n].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌))).obj (op ⦋d⦌)) j ↔
      Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (∂Δ[n].obj (op ⦋d⦌)) j
⊢ ∂Δ[n].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌)) = ∂Δ[n]

Tactic:
ext ⟨⟨d⟩⟩ j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
obj :
  (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) ↔
    ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) ((∂Δ[n].op.preimage (Iso.inv (stdSimplex.opIso ⦋n⦌))).obj (op ⦋d⦌)) j ↔
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (∂Δ[n].obj (op ⦋d⦌)) j

Tactic:
simp only [Subcomplex.preimage_obj, Set.mem_preimage, stdSimplex.opIso_inv_app_hom_apply,
    Subcomplex.mem_op_obj_iff, mem_boundary_iff_notMem_range, Set.mem_range,
    stdSimplex.opObjEquiv_opObjEquiv_symm_apply, not_exists]

Premises used: Set.mem_range, not_exists, SSet.Subcomplex.mem_op_obj_iff, SSet.Subcomplex.preimage_obj, SSet.mem_boundary_iff_notMem_range, SSet.stdSimplex.opObjEquiv_opObjEquiv_symm_apply, Set.mem_preimage, SSet.stdSimplex.opIso_inv_app_hom_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
obj :
  (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) →
    ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1
obj₁ :
  (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1) →
    ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1
⊢ (∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1) ↔
    ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = k
l : Fin (d + 1)
h : (j : (a : Fin (d + 1)) → Fin (n + 1)) l = k.rev
⊢ Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) l.rev.rev) = k

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = k
⊢ ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = j_1

Tactic:
exact ⟨k.rev, fun l _ ↦ hk l.rev (by aesop)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = k
l : Fin (d + 1)
h : Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) l.rev) = k.rev
⊢ (j : (a : Fin (d + 1)) → Fin (n + 1)) l.rev = k

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬(j : (a : Fin (d + 1)) → Fin (n + 1)) x = k
⊢ ∃ (j_1 : Fin (n + 1)), ∀ (x : Fin (d + 1)), ¬Fin.rev ((j : (a : Fin (d + 1)) → Fin (n + 1)) x.rev) = j_1

Tactic:
exact ⟨k.rev, fun l _ ↦ hk l.rev (by aesop)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
h₁ :
  ∀ (a : Δ[n] _⦋i⦌) (ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a),
    Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.degenerate i)
        (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) ↔
      Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
        (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)
⊢ Eq.{u + 1} (α := Set (A.toSSet _⦋i⦌)) (A.toSSet.degenerate i) ⊤

Tactic:
ext ⟨a, ha⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
h₁ :
  Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i)
      (↑(Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) :
        Δ[n] _⦋i⦌) ↔
    Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)
⊢ Membership.mem (γ := Set (A.toSSet _⦋i⦌)) (A.toSSet.degenerate i)
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) ↔
    Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)

Tactic:
rw [A.mem_degenerate_iff]

Premises used: SSet.Subcomplex.mem_degenerate_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
h₁ : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i)
      (↑(Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha) :
        Δ[n] _⦋i⦌) ↔
    Membership.mem (γ := Set (A.toSSet _⦋i⦌)) ⊤
      (Subtype.mk (p := fun (x : Δ[n] _⦋i⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) x) a ha)

Tactic:
simp only [Subfunctor.toFunctor_obj, Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: CategoryTheory.Subfunctor.toFunctor_obj, iff_true, Set.top_eq_univ, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
h₁ : ∀ (hi : n < i), Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a
h₂ :
  ∀ (hi : n ≤ n) (a : Δ[n] _⦋n⦌) (ha : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (A.obj (op ⦋n⦌)) a),
    Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].degenerate n) a
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a

Tactic:
obtain hi | rfl := hi.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi_1 : n ≤ i
a : Δ[n] _⦋i⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (A.obj (op ⦋i⦌)) a
hi : n < i
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) a

Tactic:
simp [Δ[n].degenerate_eq_univ_of_hasDimensionLT (n + 1) i]

Premises used: SSet.degenerate_eq_univ_of_hasDimensionLT, SSet.stdSimplex, HAdd.hAdd, SimplexCategory.mk, OfNat.ofNat, CategoryTheory.Functor.obj