awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x_2 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
y : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) x
h :
  Eq (α :=
    (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)) ↦
              Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
                Membership.mem (γ := Set (Y _⦋n⦌))
                  (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) x)
                (↑x : Y _⦋n⦌) ⋯) :
          (a : (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u)) →
            (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
        (Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          x hx) :
      (fun (X : Type u) ↦ X)
        (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) →
            (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
        y :
      (fun (X : Type u) ↦ X)
        (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) : Type u))
⊢ Eq.{u + 1} (α := Y _⦋n⦌)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)) ↦
                Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
                  Membership.mem (γ := Set (Y _⦋n⦌))
                    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op ⦋n⦌)) x)
                  (↑x : Y _⦋n⦌) ⋯) :
            (a : (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          (Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
            Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
              x)
            x hx)) :
      Y _⦋n⦌)
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          y) :
      Y _⦋n⦌)

Tactic:
rw [Subtype.ext_iff] at h

Premises used: Subtype.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x_1 : SimplexCategoryᵒᵖ
n : ℕ
x_2 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
y : (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) x
h :
  x =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          y) :
      Y _⦋n⦌)
subst :
  ∀
    (hx :
      Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                (a : sigmaStdSimplex i d _⦋n⦌) →
                  (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
              y) :
          Y _⦋n⦌)),
    ∃ (x₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
                (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
            x₁ =
          Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
            Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
              x)
            (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                    (a : sigmaStdSimplex i d _⦋n⦌) →
                      (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                  y) :
              Y _⦋n⦌)
            hx ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            x₁ =
          y
⊢ ∃ (x₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
          x₁ =
        Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          x hx ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
          x₁ =
        y

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y)) :
      Y _⦋n⦌)
⊢ ∃ (x₁ : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
          x₁ =
        Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                  (a : sigmaStdSimplex i d _⦋n⦌) →
                    (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  y)) :
            Y _⦋n⦌)
          hx ∧
      Eq (α := (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            x₁ :
          (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y :
          (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))

Tactic:
⟨c.ιSigmaBoundary.app _ ⟨y, ?_⟩, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Subtype.mk, And.intro, Exists.intro, SSet.relativeCellComplexOfMono.Cell.ιSigmaBoundary, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y)) :
      Y _⦋n⦌)
⊢ Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌)) : (a : Δ[d] _⦋n⦌) → Y _⦋n⦌) y : Y _⦋n⦌)

Tactic:
rw [dsimp% congr($(c.ι_b_ι).app (op ⦋n⦌) y)] at hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌)) : (a : Δ[d] _⦋n⦌) → Y _⦋n⦌) y : Y _⦋n⦌)
refine_1 :
  Membership.mem (γ := Set (Δ[d] _⦋n⦌))
    ((Subcomplex.preimage ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) c.map).obj (op ⦋n⦌)) y
refine_1₁ :
  Membership.mem (γ := Set (Δ[d] _⦋n⦌))
    (Set.preimage (β := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌))) :
        (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)))
    y
refine_1₂ refine_1₃ refine_1₄ refine_1₅ :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (γ := Set ((fun (X : Type u) ↦ X) (Y _⦋n⦌)))
    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        y :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) y

Tactic:
rwa [← c.preimage_map, Subcomplex.preimage_obj, Set.mem_preimage]

Premises used: SSet.relativeCellComplexOfMono.Cell.preimage_map, SSet.Subcomplex.preimage_obj, Set.mem_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y)) :
      Y _⦋n⦌)
⊢ (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaBoundary.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (∂Δ[d].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
            (Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) x) y
              ⋯))) :
      Y _⦋n⦌) =
    (↑(Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                  (a : sigmaStdSimplex i d _⦋n⦌) →
                    (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  y)) :
            Y _⦋n⦌)
          hx) :
      Y _⦋n⦌)

Tactic:
congr($(c.ι_t_ι_eq_ι_l_b_ι).app _ ⟨y, _⟩)

Premises used: Eq.mpr, SSet.relativeCellComplexOfMono.Cell.ι_b_ι, SSet.relativeCellComplexOfMono.Cell.preimage_map, congrArg, CategoryTheory.ConcreteCategory.hom, Membership.mem, CategoryTheory.Subfunctor.obj, Eq.mp, id, SSet.relativeCellComplexOfMono.Cell.ι_t_ι_eq_ι_l_b_ι, SSet.Subcomplex.preimage_obj, Subtype.mk, SimplexCategory.mk, Opposite.op, SSet.skeletonOfMono, propext, SSet.relativeCellComplexOfMono.Cell.map, Eq.symm, DFunLike.coe, CategoryTheory.NatTrans.app, Set.mem_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y)) :
      Y _⦋n⦌)
⊢ (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((t i d).app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaBoundary.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (∂Δ[d].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
            (Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) x) y
              ⋯))) :
      Y _⦋n⦌) =
    (↑(Subtype.mk (p := fun (x : Y _⦋n⦌) ↦
          Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
            x)
          (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
                  (a : sigmaStdSimplex i d _⦋n⦌) →
                    (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
                    (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
                  y)) :
            Y _⦋n⦌)
          hx) :
      Y _⦋n⦌)

Tactic:
exact congr($(c.ι_t_ι_eq_ι_l_b_ι).app _ ⟨y, _⟩)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y)) :
      Y _⦋n⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaBoundary.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (∂Δ[d].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
            (Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) x) y ⋯) :
          (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        y :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))

Tactic:
congr($(c.ι_l).app _ ⟨y, _⟩)

Premises used: Eq.mpr, SSet.relativeCellComplexOfMono.Cell.ι_b_ι, SSet.relativeCellComplexOfMono.Cell.preimage_map, congrArg, CategoryTheory.ConcreteCategory.hom, SSet.relativeCellComplexOfMono.Cell.ι_l, Membership.mem, CategoryTheory.Subfunctor.obj, Eq.mp, id, SSet.Subcomplex.preimage_obj, Subtype.mk, SimplexCategory.mk, Opposite.op, SSet.skeletonOfMono, propext, SSet.relativeCellComplexOfMono.Cell.map, Eq.symm, DFunLike.coe, CategoryTheory.NatTrans.app, Set.mem_preimage
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
x_1 : (fun (X : Type u) ↦ X) (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌)) : Type u)
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  Membership.mem (γ := Set (Y _⦋n⦌)) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op ⦋n⦌))
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op ⦋n⦌)) :
            (a : sigmaStdSimplex i d _⦋n⦌) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op ⦋n⦌)) : Type u))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
            y)) :
      Y _⦋n⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaBoundary.app (op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) (∂Δ[d].toSSet _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌))
            (Subtype.mk (p := fun (x : Δ[d] _⦋n⦌) ↦ Membership.mem (γ := Set (Δ[d] _⦋n⦌)) (∂Δ[d].obj (op ⦋n⦌)) x) y ⋯) :
          (fun (X : Type u) ↦ X) (sigmaBoundary i d _⦋n⦌)) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        y :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))

Tactic:
exact congr($(c.ι_l).app _ ⟨y, _⟩)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
rw : ⊤ ≤ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)
⊢ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d) = ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx :
  Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    x
h :
  Membership.mem (γ :=
    Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
      Membership.mem (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
      x hx)
⊢ Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) x ∨
    ∃ i_1 ∈ Y.nonDegenerate d,
      (∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = i_1) ∧
        Membership.mem (γ := Set (Y.obj (op n))) ((Subcomplex.ofSimplex i_1).obj (op n)) x

Tactic:
simp only [skeletonOfMono_succ, Subfunctor.range_obj, Set.mem_range, not_exists,
    Subfunctor.max_obj, Subfunctor.iSup_obj, Set.iUnion_coe_set, Set.mem_union, Set.mem_iUnion,
    exists_prop] at hx

Premises used: Set.mem_union, Set.mem_range, CategoryTheory.Subfunctor.max_obj, Set.mem_iUnion, Set.iUnion_coe_set, not_exists, exists_prop, CategoryTheory.Subfunctor.range_obj, CategoryTheory.Subfunctor.iSup_obj, SSet.skeletonOfMono_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx_1 :
  Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    x
h :
  Membership.mem (γ :=
    Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
      Membership.mem (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
      x hx_1)
hx : Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) x
⊢ Membership.mem (γ := Set (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) : Type u))
    (Set.range (ι := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u))
        (⇑{
              toFun := fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u)) ↦
                Subtype.mk (p := fun (x : Y.obj (op n)) ↦
                  Membership.mem (γ := Set (Y.obj (op n)))
                    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
                  (↑x : Y.obj (op n)) ⋯ } :
          (a : (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op n)) : Type u)) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)) ∪
      Set.range (ι := (sigmaStdSimplex i d).obj (op n))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n))) :
          (a : (sigmaStdSimplex i d).obj (op n)) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
      Membership.mem (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
      x hx_1)

Tactic:
Or.inl ⟨⟨x, hx⟩, rfl⟩

Premises used: Set.union, Set.Mem, setOf, Subtype.mk, Exists.intro, Or.inl, rfl