awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
a : Δ[n] _⦋n⦌
ha : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (A.obj (op ⦋n⦌)) a
h₁ :
  a ∉
    singleton (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
      ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
          (𝟙 (unop (op ⦋n⦌))) :
        stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
⊢ Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].degenerate n) a

Tactic:
rw [mem_degenerate_iff_notMem_nonDegenerate, nonDegenerate_top_dim]

Premises used: SSet.mem_degenerate_iff_notMem_nonDegenerate, SSet.stdSimplex.nonDegenerate_top_dim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha :
  Membership.mem (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
        (𝟙 (unop (op ⦋n⦌))) :
      stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
⊢ A ≤ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha :
  Membership.mem (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
        (𝟙 (unop (op ⦋n⦌))) :
      stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
⊢ ⊤ ≤ A

Tactic:
simpa [← ofSimplex_objEquiv_symm_id]

Premises used: SSet.stdSimplex.ofSimplex_objEquiv_symm_id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha :
  Membership.mem (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (A.obj (op ⦋n⦌))
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
        (𝟙 (unop (op ⦋n⦌))) :
      stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
⊢ False

Tactic:
exact h (le_antisymm (by simp) (by simpa [← ofSimplex_objEquiv_symm_id]))

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
⊢ A ≤ ∂Δ[n] ↔ A ≠ ⊤

Tactic:
⟨fun h ↦ ?_, fun hA ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
refine_1 : ∀ (h : A ≤ ∂Δ[n]), A ≠ ⊤
refine_2 : ∀ (hA : A ≠ ⊤), A ≤ ∂Δ[n]
⊢ A ≤ ∂Δ[n] ↔ A ≠ ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun hA ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ False

Tactic:
lt_irrefl _ (lt_of_le_of_lt h (boundary_lt_top n))

Premises used: lt_of_le_of_lt, lt_irrefl, SSet.boundary_lt_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt h (boundary_lt_top n))

Premises used: lt_of_le_of_lt, lt_irrefl, SSet.boundary_lt_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
⊢ HasDimensionLT.{u} A.toSSet n

Tactic:
have := subcomplex_hasDimensionLT_of_neq_top A hA
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
refine_2 :
  ∀ (n_1 : ℕ) (x : (↑(Δ[n].nonDegenerate n_1) : Type u)),
    Membership.mem (γ := Set (Δ[n] _⦋n_1⦌)) (A.obj (op ⦋n_1⦌)) (↑x : Δ[n] _⦋n_1⦌) →
      Membership.mem (γ := Set (Δ[n] _⦋n_1⦌)) (∂Δ[n].obj (op ⦋n_1⦌)) (↑x : Δ[n] _⦋n_1⦌)
⊢ A ≤ ∂Δ[n]

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Premises used: SSet.Subcomplex.le_iff_contains_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
h₂ :
  Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (A.obj (op ⦋m⦌))
    (↑(Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x) x h₁) :
      Δ[n] _⦋m⦌)
refine_2 : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌))
    (↑(Subtype.mk (p := fun (x : Δ[n] _⦋m⦌) ↦ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x) x h₁) :
      Δ[n] _⦋m⦌)

Tactic:
dsimp at h₂ ⊢
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
h₂ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (A.obj (op ⦋m⦌)) x
pos : ∀ (h₃ : m < n), Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
neg : ∀ (h₃ : n ≤ m), Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x

Tactic:
by_cases! h₃ : m < n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
h₂ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (A.obj (op ⦋m⦌)) x
h₃ : m < n
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x

Tactic:
simp [boundary_obj_eq_univ m n h₃]

Premises used: SSet.boundary_obj_eq_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
this : HasDimensionLT.{u} A.toSSet n
m : ℕ
x : Δ[n] _⦋m⦌
h₁ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
h₂ : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (A.obj (op ⦋m⦌)) x
h₃ : n ≤ m
⊢ Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (∂Δ[n].obj (op ⦋m⦌)) x

Tactic:
simp [← A.mem_nonDegenerate_iff ⟨x, h₂⟩,
        nonDegenerate_eq_empty_of_hasDimensionLT _ _ _ h₃] at h₁

Premises used: SSet.Subcomplex.mem_nonDegenerate_iff, Subtype.mk, SSet.nonDegenerate_eq_empty_of_hasDimensionLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
mp : A = ∂Δ[n] → ∂Δ[n] ≤ A ∧ A ≠ ⊤
mpr : ∂Δ[n] ≤ A ∧ A ≠ ⊤ → A = ∂Δ[n]
⊢ A = ∂Δ[n] ↔ ∂Δ[n] ≤ A ∧ A ≠ ⊤

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
⊢ ∂Δ[n] ≤ ∂Δ[n]

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
⊢ ∂Δ[n] ≤ ∂Δ[n] ∧ ∂Δ[n] ≠ ⊤

Tactic:
exact ⟨by rfl, (boundary_lt_top n).ne⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h₁ : ∂Δ[n] ≤ A
h₂ rwa rwa₁ rwa₂ rwa₃ : A ≠ ⊤
⊢ A ≤ ∂Δ[n]

Tactic:
rwa [le_boundary_iff]

Premises used: SSet.stdSimplex.le_boundary_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
A : Δ[n].Subcomplex
h₁ : ∂Δ[n] ≤ A
h₂ : A ≠ ⊤
⊢ A = ∂Δ[n]

Tactic:
exact le_antisymm (by rwa [le_boundary_iff]) h₁

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Mono (Subcomplex.homOfLE ⋯)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
⊢ faceι i ≫ Subcomplex.ι ∂Δ[n + 1] = Subcomplex.ι (stdSimplex.face {i}ᶜ)

Tactic:
simp [faceι]

Premises used: SSet.boundary.faceι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
simp :
  LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    ∂Δ[n + 1]
⊢ Subcomplex.range (stdSimplex.map (SimplexCategory.δ i)) ≤ ∂Δ[n + 1]

Tactic:
simp only [Subcomplex.range_eq_ofSimplex]

Premises used: SSet.Subcomplex.range_eq_ofSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    ∂Δ[n + 1]

Tactic:
le_trans ?_ (face_singleton_compl_le_boundary i)

Premises used: SSet.face_singleton_compl_le_boundary, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
refine :
  LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    (stdSimplex.face {i}ᶜ)
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    ∂Δ[n + 1]

Tactic:
refine le_trans ?_ (face_singleton_compl_le_boundary i)

Premises used: SSet.face_singleton_compl_le_boundary, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
rw :
  LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    (Subcomplex.ofSimplex (n := n)
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
rw₁ rw₂ :
  LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
    (Subcomplex.ofSimplex (n := n)
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    (stdSimplex.face {i}ᶜ)

Tactic:
rw [stdSimplex.face_singleton_compl, yonedaEquiv_map]

Premises used: SSet.yonedaEquiv_map, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
⊢ ι i ≫ Subcomplex.ι ∂Δ[n + 1] = stdSimplex.δ i

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.CosimplicialObject.δ, CategoryTheory.Functor.comp, TypeCat.Fun.comp, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
rw : ι i = (stdSimplex.faceSingletonComplIso i).hom ≫ faceι i
⊢ (stdSimplex.faceSingletonComplIso i).inv ≫ ι i = faceι i

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso i).hom, Iso.hom_inv_id_assoc]

Premises used: SSet.stdSimplex.faceSingletonComplIso, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
⊢ ι i = (stdSimplex.faceSingletonComplIso i).hom ≫ faceι i

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
rw : Mono (faceι i)
⊢ Mono (ι i)

Tactic:
rw [← mono_comp_iff_of_isIso (stdSimplex.faceSingletonComplIso i).inv,
    faceSingletonComplIso_inv_ι]

Premises used: SSet.stdSimplex.faceSingletonComplIso, SSet.boundary.faceSingletonComplIso_inv_ι, CategoryTheory.Iso.inv, CategoryTheory.mono_comp_iff_of_isIso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Mono (faceι i)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Mono (ι i ≫ Subcomplex.ι ∂Δ[n + 1])

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
w :
  ∀ (m : SimplexCategoryᵒᵖ) (x : Δ[n + 1].obj m)
    (hx : Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
        (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
          Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
        (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
          Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx)
⊢ f = g

Tactic:
ext m ⟨x, hx⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
x : Δ[n + 1].obj m
hx : Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x
⊢ ∃ (i : Fin (n + 1 + 1)) (f : unop m ⟶ ⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map f.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) : Δ[n + 1] _⦋n⦌) =
      x

Tactic:
simp only [boundary_eq_iSup, stdSimplex.face_singleton_compl, Subfunctor.iSup_obj,
    Set.mem_iUnion, Subcomplex.mem_ofSimplex_obj_iff, op_unop] at hx

Premises used: SSet.Subcomplex.mem_ofSimplex_obj_iff, Opposite.op_unop, Set.mem_iUnion, SSet.boundary_eq_iSup, CategoryTheory.Subfunctor.iSup_obj, SSet.stdSimplex.face_singleton_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
x : Δ[n + 1].obj m
hx_1 : Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x
hx :
  ∃ (i : Fin (n + 1 + 1)) (f : unop m ⟶ ⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map f.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) : Δ[n + 1] _⦋n⦌) =
      x
w :
  ∀ (i : Fin (n + 1 + 1)) (y : unop m ⟶ ⦋n⦌)
    (hx :
      Membership.mem (α := Δ[n + 1].obj m) (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
              Δ[n + 1] _⦋n⦌) :
          Δ[n + 1].obj m)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
        (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
          Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
              Δ[n + 1] _⦋n⦌))
          hx) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
        (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
          Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
              Δ[n + 1] _⦋n⦌))
          hx)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx_1) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx_1)

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

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
i : Fin (n + 1 + 1)
y : unop m ⟶ ⦋n⦌
hx :
  Membership.mem (α := Δ[n + 1].obj m) (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) : Δ[n + 1] _⦋n⦌) :
      Δ[n + 1].obj m)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
            Δ[n + 1] _⦋n⦌))
        hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
            Δ[n + 1] _⦋n⦌))
        hx)

Tactic:
ConcreteCategory.congr_hom (congr_app (h i) _) _

Premises used: SimplexCategory.mkHom, Quiver.Hom.unop, SimplexCategory.δ, CategoryTheory.ConcreteCategory.congr_hom, OrderEmbedding.toOrderHom, CategoryTheory.congr_app, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
i : Fin (n + 1 + 1)
y : unop m ⟶ ⦋n⦌
hx :
  Membership.mem (α := Δ[n + 1].obj m) (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) : Δ[n + 1] _⦋n⦌) :
      Δ[n + 1].obj m)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
            Δ[n + 1] _⦋n⦌))
        hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
            Δ[n + 1] _⦋n⦌))
        hx)

Tactic:
exact ConcreteCategory.congr_hom (congr_app (h i) _) _

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
X : SSet
f g : Subcomplex.toSSet (X := Δ[0]) ∂Δ[0] ⟶ X
w :
  ∀ (n : SimplexCategoryᵒᵖ) (x : Δ[0].obj n) (hx : Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app n)).toFun
        (Subtype.mk (p := fun (x : Δ[0].obj n) ↦ Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x) x
          hx) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app n)).toFun
        (Subtype.mk (p := fun (x : Δ[0].obj n) ↦ Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x) x
          hx)
⊢ f = g

Tactic:
ext _ ⟨x, hx⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
X : SSet
f g : Subcomplex.toSSet (X := Δ[0]) ∂Δ[0] ⟶ X
n : SimplexCategoryᵒᵖ
x : Δ[0].obj n
hx : Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app n)).toFun
      (Subtype.mk (p := fun (x : Δ[0].obj n) ↦ Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x) x
        hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app n)).toFun
      (Subtype.mk (p := fun (x : Δ[0].obj n) ↦ Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x) x hx)

Tactic:
simp at hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
n : ℕ
⊢ I ∂Δ[n].ι

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
zero : ∀ [NeZero (R := ℕ) 0] (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), J Λ[0, i].ι
succ : ∀ (n : ℕ) [NeZero (n + 1)] (i : Fin (n + 1 + 1)), J Λ[n + 1, i].ι
⊢ J Λ[n, i].ι

Tactic:
obtain _ | n := n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
inst : NeZero (R := ℕ) 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ J Λ[0, i].ι

Tactic:
(NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
inst : NeZero (R := ℕ) 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ J Λ[0, i].ι

Tactic:
exact (NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
n : ℕ
inst : NeZero (n + 1)
i : Fin (n + 1 + 1)
succ :
  ∃ (i_1 : ℕ),
    ofHoms (X := fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].toSSet) (Y := fun (i : Fin (i_1 + 2)) ↦ Δ[i_1 + 1])
      (fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].ι) Λ[n + 1, i].ι
⊢ J Λ[n + 1, i].ι

Tactic:
simp only [J, iSup_iff]

Premises used: SSet.modelCategoryQuillen.J, CategoryTheory.MorphismProperty.iSup_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
n : ℕ
inst : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ ∃ (i_1 : ℕ),
    ofHoms (X := fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].toSSet) (Y := fun (i : Fin (i_1 + 2)) ↦ Δ[i_1 + 1])
      (fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].ι) Λ[n + 1, i].ι

Tactic:
⟨n, ⟨i⟩⟩

Premises used: Exists.intro, CategoryTheory.MorphismProperty.ofHoms.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
n : ℕ
inst : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ ∃ (i_1 : ℕ),
    ofHoms (X := fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].toSSet) (Y := fun (i : Fin (i_1 + 2)) ↦ Δ[i_1 + 1])
      (fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].ι) Λ[n + 1, i].ι

Tactic:
exact ⟨n, ⟨i⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
n : ℕ
⊢ monomorphisms SSet ∂Δ[n].ι

Tactic:
monomorphisms.infer_property _

Premises used: CategoryTheory.MorphismProperty.monomorphisms.infer_property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
n : ℕ
⊢ monomorphisms SSet ∂Δ[n].ι

Tactic:
exact monomorphisms.infer_property _

Premises used: CategoryTheory.MorphismProperty.monomorphisms.infer_property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
h : J f
⊢ ∃ (i : ℕ),
    ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦ Δ[i + 1])
      (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) f

Tactic:
simp only [J, iSup_iff] at h

Premises used: SSet.modelCategoryQuillen.J, CategoryTheory.MorphismProperty.iSup_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
h :
  ∃ (i : ℕ),
    ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦ Δ[i + 1])
      (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) f
obtain : ∀ (n : ℕ) ⦃X Y : SSet.{u}⦄ (i : Fin (n + 2)), monomorphisms SSet Λ[n + 1, i].ι
⊢ monomorphisms SSet f

Tactic:
obtain ⟨n, ⟨i⟩⟩ := h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
n : ℕ
X Y : SSet
i : Fin (n + 2)
⊢ monomorphisms SSet Λ[n + 1, i].ι

Tactic:
monomorphisms.infer_property _

Premises used: CategoryTheory.MorphismProperty.monomorphisms.infer_property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
n : ℕ
X Y : SSet
i : Fin (n + 2)
⊢ monomorphisms SSet Λ[n + 1, i].ι

Tactic:
exact monomorphisms.infer_property _

Premises used: CategoryTheory.MorphismProperty.monomorphisms.infer_property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
⊢ cofibrations SSet = monomorphisms SSet

Tactic:
rfl

Premises used: HomotopicalAlgebra.cofibrations, rfl