awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X Y : SSet
B : Y.Subcomplex
e : X ≅ Y
x : (B.preimage e.hom).N
⊢ S.simplex (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN)) ∉
    B.obj (Opposite.op ⦋S.dim.{u} (X := Y) (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN))⦌)

Tactic:
x.notMem

Premises used: Set.Mem, setOf, Set.preimage, SSet.Subcomplex.N.notMem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X Y : SSet
B : Y.Subcomplex
e : X ≅ Y
x : (B.preimage e.hom).N
⊢ S.simplex (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN)) ∉
    B.obj (Opposite.op ⦋S.dim.{u} (X := Y) (N.toS ((SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN))⦌)

Tactic:
exact x.notMem

Premises used: SSet.Subcomplex.N.notMem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
⊢ A.preimage e.inv = B

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
obtain :
  ∀ (hA : (A.preimage e.inv).preimage e.hom = A) (y : (A.preimage e.inv).N),
    S.simplex (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN)) ∉
      A.obj (Opposite.op ⦋S.dim.{u} (X := X) (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN))⦌)
⊢ S.simplex (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN)) ∉
    A.obj (Opposite.op ⦋S.dim.{u} (X := X) (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN))⦌)

Tactic:
obtain rfl : A.preimage e.inv = B := by aesop

Premises used: SSet.Subcomplex.preimage, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
e : X ≅ Y
hA : (A.preimage e.inv).preimage e.hom = A
y : (A.preimage e.inv).N
⊢ S.simplex (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN)) ∉
    A.obj (Opposite.op ⦋S.dim.{u} (X := X) (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN))⦌)

Tactic:
y.notMem

Premises used: Set.Mem, setOf, Set.preimage, SSet.Subcomplex.N.notMem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
e : X ≅ Y
hA : (A.preimage e.inv).preimage e.hom = A
y : (A.preimage e.inv).N
⊢ S.simplex (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN)) ∉
    A.obj (Opposite.op ⦋S.dim.{u} (X := X) (N.toS (((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN))⦌)

Tactic:
exact y.notMem

Premises used: SSet.Subcomplex.N.notMem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x : A.N
⊢ (fun (y : B.N) ↦ { toN := ((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN, notMem := ⋯ : A.N })
      ((fun (x : A.N) ↦ { toN := (SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN, notMem := ⋯ : B.N }) x) =
    x

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
x : B.N
⊢ (fun (x : A.N) ↦ { toN := (SSet.N.orderIsoOfIso e : (a : X.N) → Y.N) x.toN, notMem := ⋯ : B.N })
      ((fun (y : B.N) ↦ { toN := ((SSet.N.orderIsoOfIso e).symm : (a : Y.N) → X.N) y.toN, notMem := ⋯ : A.N }) x) =
    x

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
⊢ ∃ (x : A.N) (f : ⦋n⦌ ⟶ ⦋x.dim⦌),
    Epi f ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          x.simplex =
        s

Tactic:
⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, S.map_toNπ_op_apply _⟩⟩

Premises used: SSet.S.toNπ, inferInstance, And.intro, Exists.intro, SSet.S.toN, SSet.Subcomplex.N.mk', SSet.S.map_toNπ_op_apply, SSet.S.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
refine :
  ∀
    (h :
      Membership.mem (γ := Set (X _⦋{ dim := n, simplex := s : X.S }.toN.dim⦌))
        (A.obj (Opposite.op ⦋{ dim := n, simplex := s : X.S }.toN.dim⦌)) { dim := n, simplex := s : X.S }.toN.simplex),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) s
⊢ ∃ (x : A.N) (f : ⦋n⦌ ⟶ ⦋x.dim⦌),
    Epi f ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          x.simplex =
        s

Tactic:
refine ⟨⟨(S.mk s).toN, fun h ↦ hs ?_⟩, ⟨(S.mk s).toNπ, inferInstance, S.map_toNπ_op_apply _⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h :
  Membership.mem (γ := Set (X _⦋{ dim := n, simplex := s : X.S }.toN.dim⦌))
    (A.obj (Opposite.op ⦋{ dim := n, simplex := s : X.S }.toN.dim⦌)) { dim := n, simplex := s : X.S }.toN.simplex
simp : ∀ (h : ofSimplex { dim := n, simplex := s : X.S }.toN.simplex ≤ A), ofSimplex s ≤ A
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) s

Tactic:
simp only [← ofSimplex_le_iff] at h ⊢

Premises used: SSet.Subcomplex.ofSimplex_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
n : ℕ
s : X _⦋n⦌
A : X.Subcomplex
hs : s ∉ A.obj (Opposite.op ⦋n⦌)
h : ofSimplex { dim := n, simplex := s : X.S }.toN.simplex ≤ A
⊢ ofSimplex s ≤ A

Tactic:
simpa using h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
n : SimplexCategoryᵒᵖ
inst : X.Nonempty
⊢ Nonempty.{u + 1} (X.obj n)

Tactic:
⟨X.map (SimplexCategory.const n.unop ⦋0⦌ 0).op (Classical.arbitrary _)⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, Nonempty.intro, CategoryTheory.Functor.map, SimplexCategory.const, SimplexCategory.mk, Classical.arbitrary, OfNat.ofNat, DFunLike.coe, Opposite.unop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
inst : X.Nonempty
⊢ Membership.mem (γ := Set (X _⦋0⦌)) (X.nonDegenerate 0) (Classical.arbitrary (X _⦋0⦌))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
inst : X.Nonempty
⊢ Nonempty.{u + 1} X.S

Tactic:
⟨S.mk (dim := 0) (Classical.arbitrary _)⟩

Premises used: Nonempty.intro, Classical.arbitrary, SSet.S.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
T : Type u
inst : Preorder T
inst_1 : Nonempty T
⊢ SSet.Nonempty.{u} (nerve T)

Tactic:
⟨.mk₀ (Classical.arbitrary _)⟩

Premises used: Nonempty.intro, Classical.arbitrary, CategoryTheory.ComposableArrows.mk₀
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
n : SimplexCategory
⊢ SSet.Nonempty.{u_1} (stdSimplex.obj n)

Tactic:
⟨stdSimplex.objEquiv.symm (SimplexCategory.const _ _ 0)⟩

Premises used: Nonempty.intro, SimplexCategory.const, Equiv.symm, OfNat.ofNat, DFunLike.coe, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X Y : SSet
f : Y ⟶ X
inst : Y.Nonempty
⊢ X.Nonempty

Tactic:
⟨f.app _ (Classical.arbitrary _)⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Nonempty.intro, Classical.arbitrary, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
simp : IsEmpty.{u + 1} (X _⦋0⦌) ↔ X.HasDimensionLT 0
⊢ ¬X.Nonempty ↔ X.HasDimensionLT 0

Tactic:
simp only [not_nonempty_iff]

Premises used: not_nonempty_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
⊢ IsEmpty.{u + 1} (X _⦋0⦌) ↔ X.HasDimensionLT 0

Tactic:
⟨fun _ ↦ ⟨fun n hn ↦ ?_⟩, fun _ ↦ ⟨fun x ↦ ?_⟩⟩

Premises used: SSet.HasDimensionLT.mk, IsEmpty.mk, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
refine_1 : IsEmpty.{u + 1} (X _⦋0⦌) → ∀ (n : ℕ) (hn : 0 ≤ n), X.degenerate n = ⊤
refine_2 : X.HasDimensionLT 0 → ∀ (x : X _⦋0⦌), False
⊢ IsEmpty.{u + 1} (X _⦋0⦌) ↔ X.HasDimensionLT 0

Tactic:
refine ⟨fun _ ↦ ⟨fun n hn ↦ ?_⟩, fun _ ↦ ⟨fun x ↦ ?_⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
h : IsEmpty.{u + 1} (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ IsEmpty.{u + 1} ((fun (X : Type u) ↦ X) (X _⦋n⦌))

Tactic:
have := Function.isEmpty (X.map (⦋0⦌.const ⦋n⦌ 0).op)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
h : IsEmpty.{u + 1} (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
this : IsEmpty.{u + 1} ((fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ X.degenerate n = ⊤

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
h : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ Membership.mem (γ := Set (X _⦋0⦌)) (X.nonDegenerate 0) x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
h : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False

Tactic:
exact (lt_self_iff_false _).1 (X.dim_lt_of_nonDegenerate ⟨x, by simp⟩ 0)

Premises used: SSet.dim_lt_of_nonDegenerate, Subtype.mk, lt_self_iff_false, Iff.mp, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : ¬X.Nonempty
⊢ IsEmpty.{u + 1} (X _⦋0⦌)

Tactic:
simp only [not_nonempty_iff] at hX

Premises used: not_nonempty_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
⊢ ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)

Tactic:
have (n : SimplexCategoryᵒᵖ) : IsEmpty (X.obj n) :=
    Function.isEmpty (X.map (⦋0⦌.const n.unop 0).op)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x : SSet
x_1 x_2 : SimplexCategoryᵒᵖ
x_3 : x_1 ⟶ x_2
h :
  ∀ (x_4 : X.obj x_1),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map x_3 ≫ ↾fun (x_5 : X.obj x_2) ↦ isEmptyElim (p := fun (x_6 : X.obj x_2) ↦ x.obj x_2) x_5))
        x_4 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x_5 : X.obj x_1) ↦ isEmptyElim (p := fun (x_6 : X.obj x_1) ↦ x.obj x_1) x_5) ≫ x.map x_3))
        x_4
⊢ (X.map x_3 ≫ ↾fun (x_4 : X.obj x_2) ↦ isEmptyElim (p := fun (x_5 : X.obj x_2) ↦ x.obj x_2) x_4) =
    (↾fun (x_4 : X.obj x_1) ↦ isEmptyElim (p := fun (x_5 : X.obj x_1) ↦ x.obj x_1) x_4) ≫ x.map x_3

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x_1 : SSet
x_2 x_3 : SimplexCategoryᵒᵖ
x_4 : x_2 ⟶ x_3
x : X.obj x_2
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map x_4 ≫ ↾fun (x : X.obj x_3) ↦ isEmptyElim (p := fun (x : X.obj x_3) ↦ x_1.obj x_3) x))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X.obj x_2) ↦ isEmptyElim (p := fun (x : X.obj x_2) ↦ x_1.obj x_2) x) ≫ x_1.map x_4))
      x

Tactic:
isEmptyElim x

Premises used: isEmptyElim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x_1 : SSet
x_2 x_3 : SimplexCategoryᵒᵖ
x_4 : x_2 ⟶ x_3
x : X.obj x_2
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map x_4 ≫ ↾fun (x : X.obj x_3) ↦ isEmptyElim (p := fun (x : X.obj x_3) ↦ x_1.obj x_3) x))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X.obj x_2) ↦ isEmptyElim (p := fun (x : X.obj x_2) ↦ x_1.obj x_2) x) ≫ x_1.map x_4))
      x

Tactic:
exact isEmptyElim x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x : SSet
x_1 : X ⟶ x
w :
  ∀ (n : SimplexCategoryᵒᵖ) (x_2 : X.obj n),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app n)).toFun x_2 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (x : SSet.{u}) ↦
                ({
                    app := fun (x_3 : SimplexCategoryᵒᵖ) ↦
                      ↾fun (x_4 : X.obj x_3) ↦ isEmptyElim (p := fun (x_5 : X.obj x_3) ↦ x.obj x_3) x_4,
                    naturality := ⋯ } :
                  NatTrans X x))
              x)
            n))
        x_2
⊢ x_1 =
    (fun (x : SSet.{u}) ↦
        ({
            app := fun (x_2 : SimplexCategoryᵒᵖ) ↦
              ↾fun (x_3 : X.obj x_2) ↦ isEmptyElim (p := fun (x_4 : X.obj x_2) ↦ x.obj x_2) x_3,
            naturality := ⋯ } :
          NatTrans X x))
      x

Tactic:
ext _ x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x_1 : SSet
x_2 : X ⟶ x_1
n : SimplexCategoryᵒᵖ
x : X.obj n
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (x_2.app n)).toFun x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : SSet.{u}) ↦
              ({
                  app := fun (x_3 : SimplexCategoryᵒᵖ) ↦
                    ↾fun (x_4 : X.obj x_3) ↦ isEmptyElim (p := fun (x_5 : X.obj x_3) ↦ x.obj x_3) x_4,
                  naturality := ⋯ } :
                NatTrans X x))
            x_1)
          n))
      x

Tactic:
isEmptyElim x

Premises used: isEmptyElim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
x_1 : SSet
x_2 : X ⟶ x_1
n : SimplexCategoryᵒᵖ
x : X.obj n
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (x_2.app n)).toFun x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : SSet.{u}) ↦
              ({
                  app := fun (x_3 : SimplexCategoryᵒᵖ) ↦
                    ↾fun (x_4 : X.obj x_3) ↦ isEmptyElim (p := fun (x_5 : X.obj x_3) ↦ x.obj x_3) x_4,
                  naturality := ⋯ } :
                NatTrans X x))
            x_1)
          n))
      x

Tactic:
exact isEmptyElim x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
Goal:
X : SSet
hX : IsEmpty.{u + 1} (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty.{u + 1} (X.obj n)
⊢ IsInitial X

Tactic:
exact IsInitial.ofUniqueHom (fun _ ↦
    { app _ := ↾fun x ↦ isEmptyElim x
      naturality _ _ _  := by ext x; exact isEmptyElim x })
    (fun _ _ ↦ by ext _ x; exact isEmptyElim x)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X : SSet
inst : X.Nonsingular
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x)

Tactic:
mono ⟨x, hx⟩

Premises used: Subtype.mk, SSet.Nonsingular.mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
this :
  ∀ (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n),
    Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X)
      ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
        (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx) : X _⦋n⦌))
⊢ ∀ (x : (↑(X.nonDegenerate n) : Type u)),
    Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X) ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) (↑x : X _⦋n⦌))

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

Tactic:
rw [← nonDegenerate_iff_of_mono f] at hx

Premises used: SSet.nonDegenerate_iff_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := Y)
    ((Equiv.symm yonedaEquiv : (a : Y _⦋n⦌) → Δ[n] ⟶ Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)))

Tactic:
have := mono' _ hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
this :
  Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := Y)
    ((Equiv.symm yonedaEquiv : (a : Y _⦋n⦌) → Δ[n] ⟶ Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          x :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌)))
⊢ Mono (X := Δ[n]) ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ≫ f)

Tactic:
rw [← SSet.yonedaEquiv_symm_comp] at this

Premises used: SSet.yonedaEquiv_symm_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
this : Mono (X := Δ[n]) ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ≫ f)
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X)
    ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌))

Tactic:
mono_of_mono _ f

Premises used: CategoryTheory.mono_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
f : X ⟶ Y
inst : Mono f
inst_1 : Y.Nonsingular
n : ℕ
x : X _⦋n⦌
hx_1 : x ∈ X.nonDegenerate n
hx :
  Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (Y.nonDegenerate n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
this : Mono (X := Δ[n]) ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ≫ f)
⊢ Mono.{u, u + 1} (C := SSet) (X := Δ[n]) (Y := X)
    ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X)
      (↑(Subtype.mk (p := fun (x : X _⦋n⦌) ↦ x ∈ X.nonDegenerate n) x hx_1) : X _⦋n⦌))

Tactic:
exact mono_of_mono _ f

Premises used: CategoryTheory.mono_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
e : X ≅ Y
inst : X.Nonsingular
⊢ Y.Nonsingular

Tactic:
.of_mono e.inv

Premises used: SSet.Nonsingular.of_mono, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
A : X.Subcomplex
inst : X.Nonsingular
⊢ Nonsingular.{u} A.toSSet

Tactic:
.of_mono A.ι

Premises used: SSet.Nonsingular.of_mono, SSet.Subcomplex.ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
this :
  ∀ (x : nerve T _⦋n⦌) (hx : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x),
    Mono.{u_1, u_1 + 1} (C := SSet) (X := Δ[n]) (Y := nerve T)
      ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T)
        (↑(Subtype.mk (p := fun (x : nerve T _⦋n⦌) ↦
              Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x) x hx) :
          nerve T _⦋n⦌))
⊢ ∀ (x : (↑((nerve T).nonDegenerate n) : Type u_1)),
    Mono.{u_1, u_1 + 1} (C := SSet) (X := Δ[n]) (Y := nerve T)
      ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) (↑x : nerve T _⦋n⦌))

Tactic:
⟨x, hx⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x
⊢ Function.Injective x.obj

Tactic:
rw [PartialOrder.mem_nerve_nonDegenerate_iff_injective] at hx

Premises used: PartialOrder.mem_nerve_nonDegenerate_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx_1 : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x
hx : Function.Injective x.obj
simp :
  ∀ (k : SimplexCategoryᵒᵖ),
    Function.Injective (α := Δ[n].obj k) (β := (nerve T).obj k)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) k)) :
        (a : Δ[n].obj k) → (nerve T).obj k)
⊢ Mono.{u_1, u_1 + 1} (C := SSet) (X := Δ[n]) (Y := nerve T)
    ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T)
      (↑(Subtype.mk (p := fun (x : nerve T _⦋n⦌) ↦
            Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x) x hx_1) :
        nerve T _⦋n⦌))

Tactic:
simp only [NatTrans.mono_iff_mono_app, mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective, CategoryTheory.NatTrans.mono_iff_mono_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx_1 : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  Eq (α := nerve T _⦋k⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) (Opposite.op ⦋k⦌)) :
          (a : Δ[n] _⦋k⦌) → nerve T _⦋k⦌)
        i :
      nerve T _⦋k⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) (Opposite.op ⦋k⦌)) :
          (a : Δ[n] _⦋k⦌) → nerve T _⦋k⦌)
        j :
      nerve T _⦋k⦌)
h :
  ∀ (l : Fin (k + 1)),
    Eq (α := Fin (n + 1)) ((i : (a : Fin (k + 1)) → Fin (n + 1)) l : Fin (n + 1))
      ((j : (a : Fin (k + 1)) → Fin (n + 1)) l : Fin (n + 1))
⊢ i = j

Tactic:
ext l : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
Goal:
X Y : SSet
T : Type u_1
inst : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx_1 : Membership.mem (γ := Set (nerve T _⦋n⦌)) ((nerve T).nonDegenerate n) x
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  Eq (α := nerve T _⦋k⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) (Opposite.op ⦋k⦌)) :
          (a : Δ[n] _⦋k⦌) → nerve T _⦋k⦌)
        i :
      nerve T _⦋k⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm yonedaEquiv : (a : nerve T _⦋n⦌) → Δ[n] ⟶ nerve T) x) (Opposite.op ⦋k⦌)) :
          (a : Δ[n] _⦋k⦌) → nerve T _⦋k⦌)
        j :
      nerve T _⦋k⦌)
l : Fin (k + 1)
⊢ Eq (α := Fin (n + 1)) ((i : (a : Fin (k + 1)) → Fin (n + 1)) l : Fin (n + 1))
    ((j : (a : Fin (k + 1)) → Fin (n + 1)) l : Fin (n + 1))

Tactic:
hx (Functor.congr_obj hij l)

Premises used: CategoryTheory.Functor.congr_obj