awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
refine_1 :
  Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (X _⦋{ dim := n,
                          simplex :=
                            (ConcreteCategory.hom (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
            (simplex
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌)))) :
          (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌)) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (N.mk (↑y : X _⦋m⦌) ⋯).simplex :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
⊢ Membership.mem (γ := Set (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (Subfunctor.obj
      (subcomplex
        (mk (dim := n) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌))))
      (Opposite.op ⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
    (N.mk (↑y : X _⦋m⦌) ⋯).simplex

Tactic:
refine ⟨(section_ f).op, this ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this_1 : IsSplitEpi f
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) (X _⦋m⦌)) (β := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op)) :
      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
refine_1 :
  Eq (α := X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) : (a : X _⦋n⦌) → X _⦋m⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌) :
          X _⦋m⦌) :
      X _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ Eq (α := (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (X _⦋{ dim := n,
                          simplex :=
                            (ConcreteCategory.hom (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌))
            (simplex
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌)))) :
          (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑y : X _⦋m⦌) ⋯).dim⦌)) :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
        (N.mk (↑y : X _⦋m⦌) ⋯).simplex :
      (fun (X : Type u) ↦ X) (X _⦋n⦌))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
refine_2 :
  Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) ((N.mk (↑y : X _⦋m⦌) ⋯).subcomplex.obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)
⊢ subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑y : X _⦋m⦌))) ≤
    (N.mk (↑y : X _⦋m⦌) ⋯).subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]

Premises used: SSet.Subcomplex.ofSimplex_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) ((N.mk (↑y : X _⦋m⦌) ⋯).subcomplex.obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)

Tactic:
⟨f.op, rfl⟩

Premises used: Set.Mem, Quiver.Hom.op, setOf, Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ Membership.mem (α := X _⦋n⦌) (γ := Set (X _⦋n⦌)) ((N.mk (↑y : X _⦋m⦌) ⋯).subcomplex.obj (Opposite.op ⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋m⦌) → X _⦋n⦌) (↑y : X _⦋m⦌) : X _⦋n⦌)

Tactic:
exact ⟨f.op, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
y₁ y₂ : X.N
h₁ : y₁.subcomplex = x.subcomplex
h₂ : y₂.subcomplex = x.subcomplex
rw : x.subcomplex = y₂.subcomplex
rw₁ rw₂ : x.subcomplex = x.subcomplex
⊢ y₁.subcomplex = y₂.subcomplex

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
⊢ x.toN.subcomplex = x.subcomplex

Tactic:
x.existsUnique_n.exists.choose_spec

Premises used: Exists.choose_spec, ExistsUnique.exists, SSet.S.existsUnique_n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
⊢ x.toN.subcomplex = x.subcomplex

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
y : X.N
h : y.subcomplex = x.subcomplex
⊢ x.toN.subcomplex = x.subcomplex

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
y : X.N
hy : x.toN = y
obtain :
  ∀ (n : ℕ) (x : X _⦋n⦌) (hy : { dim := n, simplex := x : X.S }.toN = y),
    ∃! f : ⦋{ dim := n, simplex := x : X.S }.dim⦌ ⟶ ⦋y.dim⦌,
      Epi f ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋{ dim := n, simplex := x }.dim⦌))
            y.simplex =
          { dim := n, simplex := x : X.S }.simplex
⊢ ∃! f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌,
    Epi f ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
          y.simplex =
        x.simplex

Tactic:
obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
y : X.N
n : ℕ
x : X _⦋n⦌
hy : { dim := n, simplex := x : X.S }.toN = y
obtain :
  ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌),
    Epi f →
      ∀ (z : (↑(X.nonDegenerate m) : Type u))
        (hy :
          toN
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌))) =
            y),
        ∃! f_1 :
          ⦋dim.{u} (X := X)
                (mk (dim := n)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                    (↑z : X _⦋m⦌)))⦌ ⟶
            ⦋y.dim⦌,
          Epi f_1 ∧
            Eq (α :=
              (fun (X : Type u) ↦ X)
                (X _⦋dim.{u} (X := X)
                    (mk (dim := n)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                        (↑z : X _⦋m⦌)))⦌))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) →
                      (fun (X : Type u) ↦ X)
                        (X _⦋{ dim := n,
                              simplex :=
                                (ConcreteCategory.hom (X.map f.op) :
                                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                                  (↑z : X _⦋m⦌) }.dim⦌))
                  y.simplex :
                (fun (X : Type u) ↦ X)
                  (X _⦋dim.{u} (X := X)
                      (mk (dim := n)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                          (↑z : X _⦋m⦌)))⦌))
              (simplex
                  (mk (dim := n)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                        (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                      (↑z : X _⦋m⦌))) :
                X _⦋dim.{u} (X := X)
                    (mk (dim := n)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                          (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                        (↑z : X _⦋m⦌)))⦌)
⊢ ∃! f : ⦋{ dim := n, simplex := x : X.S }.dim⦌ ⟶ ⦋y.dim⦌,
    Epi f ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋{ dim := n, simplex := x }.dim⦌))
          y.simplex =
        { dim := n, simplex := x : X.S }.simplex

Tactic:
obtain ⟨m, f, _, z, rfl⟩ := X.exists_nonDegenerate x

Premises used: SSet.exists_nonDegenerate, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  toN
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    y
⊢ y.subcomplex =
    subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌)))

Tactic:
rw [toN_eq_iff] at hy

Premises used: SSet.S.toN_eq_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  y.subcomplex =
    subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌)))
rw :
  subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    (N.mk (↑z : X _⦋m⦌) ⋯).subcomplex
⊢ y = N.mk (↑z : X _⦋m⦌) ⋯

Tactic:
rw [← N.subcomplex_injective_iff, hy]

Premises used: SSet.N.subcomplex_injective_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  y.subcomplex =
    subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌)))
⊢ subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    (N.mk (↑z : X _⦋m⦌) ⋯).subcomplex

Tactic:
subcomplex_eq_of_epi _ _ f rfl

Premises used: SSet.S.subcomplex_eq_of_epi, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  y.subcomplex =
    subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌)))
⊢ subcomplex
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    (N.mk (↑z : X _⦋m⦌) ⋯).subcomplex

Tactic:
exact subcomplex_eq_of_epi _ _ f rfl

Premises used: SSet.S.subcomplex_eq_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  toN
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    N.mk (↑z : X _⦋m⦌) ⋯
⊢ ∃! f_1 :
    ⦋dim.{u} (X := X)
          (mk (dim := n)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
              (↑z : X _⦋m⦌)))⦌ ⟶
      ⦋(N.mk (↑z : X _⦋m⦌) ⋯).dim⦌,
    Epi f_1 ∧
      Eq (α :=
        (fun (X : Type u) ↦ X)
          (X _⦋dim.{u} (X := X)
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌)))⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑z : X _⦋m⦌) ⋯).dim⦌)) →
                (fun (X : Type u) ↦ X)
                  (X _⦋{ dim := n,
                        simplex :=
                          (ConcreteCategory.hom (X.map f.op) :
                              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                            (↑z : X _⦋m⦌) }.dim⦌))
            (N.mk (↑z : X _⦋m⦌) ⋯).simplex :
          (fun (X : Type u) ↦ X)
            (X _⦋dim.{u} (X := X)
                (mk (dim := n)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                    (↑z : X _⦋m⦌)))⦌))
        (simplex
            (mk (dim := n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                (↑z : X _⦋m⦌))) :
          X _⦋dim.{u} (X := X)
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌)))⦌)

Tactic:
existsUnique_of_exists_of_unique ⟨f, inferInstance, rfl⟩
    (fun f₁ f₂ ⟨_, hf₁⟩ ⟨_, hf₂⟩ ↦ unique_nonDegenerate_map _ _ _ _ hf₁.symm _ _ hf₂.symm)

Premises used: SSet.S.simplex, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, inferInstance, existsUnique_of_exists_of_unique, _private.0.SSet.S.existsUnique_toNπ.match_1, CategoryTheory.Functor.map, And.intro, Exists.intro, Eq.symm, Subtype.val, Eq, SSet.unique_nonDegenerate_map, DFunLike.coe, rfl, SSet.S.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
z : (↑(X.nonDegenerate m) : Type u)
hy :
  toN
      (mk (dim := n)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
          (↑z : X _⦋m⦌))) =
    N.mk (↑z : X _⦋m⦌) ⋯
⊢ ∃! f_1 :
    ⦋dim.{u} (X := X)
          (mk (dim := n)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
              (↑z : X _⦋m⦌)))⦌ ⟶
      ⦋(N.mk (↑z : X _⦋m⦌) ⋯).dim⦌,
    Epi f_1 ∧
      Eq (α :=
        (fun (X : Type u) ↦ X)
          (X _⦋dim.{u} (X := X)
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌)))⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f_1.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(N.mk (↑z : X _⦋m⦌) ⋯).dim⦌)) →
                (fun (X : Type u) ↦ X)
                  (X _⦋{ dim := n,
                        simplex :=
                          (ConcreteCategory.hom (X.map f.op) :
                              (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                            (↑z : X _⦋m⦌) }.dim⦌))
            (N.mk (↑z : X _⦋m⦌) ⋯).simplex :
          (fun (X : Type u) ↦ X)
            (X _⦋dim.{u} (X := X)
                (mk (dim := n)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                    (↑z : X _⦋m⦌)))⦌))
        (simplex
            (mk (dim := n)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                (↑z : X _⦋m⦌))) :
          X _⦋dim.{u} (X := X)
              (mk (dim := n)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋m⦌)) → (fun (X : Type u) ↦ X) (X _⦋n⦌))
                  (↑z : X _⦋m⦌)))⦌)

Tactic:
refine existsUnique_of_exists_of_unique ⟨f, inferInstance, rfl⟩
    (fun f₁ f₂ ⟨_, hf₁⟩ ⟨_, hf₂⟩ ↦ unique_nonDegenerate_map _ _ _ _ hf₁.symm _ _ hf₂.symm)

Premises used: existsUnique_of_exists_of_unique, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
⊢ Epi x.toNπ

Tactic:
(existsUnique_toNπ rfl).exists.choose_spec.1

Premises used: Exists.choose_spec, ExistsUnique.exists, SSet.S.toNπ, And.left, SSet.S.existsUnique_toNπ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map x.toNπ.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋x.toN.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      x.toN.simplex =
    x.simplex

Tactic:
(existsUnique_toNπ rfl).exists.choose_spec.2

Premises used: Exists.choose_spec, ExistsUnique.exists, SSet.S.toNπ, And.right, SSet.S.existsUnique_toNπ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
⊢ x.toN.dim ≤ x.dim

Tactic:
SimplexCategory.le_of_epi x.toNπ

Premises used: SSet.S.toNπ, SimplexCategory.le_of_epi
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
s : A.N
⊢ ∃ (t : X.N) (ht : t.simplex ∉ A.obj (Opposite.op ⦋t.dim⦌)), s = { toN := t, notMem := ht }

Tactic:
⟨s.toN, s.notMem, rfl⟩

Premises used: SSet.Subcomplex.N.toN, Exists.intro, SSet.Subcomplex.N.notMem, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
s : A.N
⊢ ∃ (n : ℕ) (x : X _⦋n⦌) (hx : x ∈ X.nonDegenerate n) (hx' : x ∉ A.obj (Opposite.op ⦋n⦌)), s = mk x hx hx'

Tactic:
⟨s.dim, s.simplex, s.nonDegenerate, s.notMem, rfl⟩

Premises used: SSet.S.simplex, SSet.Subcomplex.N.toN, SSet.N.toS, SSet.S.dim, Exists.intro, SSet.N.nonDegenerate, SSet.Subcomplex.N.notMem, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
x y : A.N
⊢ x = y ↔ x.toN = y.toN

Tactic:
grind [cases SSet.Subcomplex.N]

Premises used: SSet.Subcomplex.N
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
pos : ∀ (hs : s.subcomplex ≤ A), motive s
neg : ∀ (hs : ¬s.subcomplex ≤ A), motive s
⊢ motive s

Tactic:
by_cases hs : s.subcomplex ≤ A

Premises used: SSet.S.subcomplex, SSet.N.toS
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : s.subcomplex ≤ A
⊢ motive s

Tactic:
mem s hs
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : s.subcomplex ≤ A
⊢ motive s

Tactic:
exact mem s hs
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : ¬s.subcomplex ≤ A
⊢ s.simplex ∉ A.obj (Opposite.op ⦋s.dim⦌)

Tactic:
simpa using hs
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
motive : X.N → Prop
mem : ∀ (s : X.N), s.subcomplex ≤ A → motive s
notMem : ∀ (s : A.N), motive s.toN
s : X.N
hs : ¬s.subcomplex ≤ A
⊢ motive s

Tactic:
exact notMem (.mk' s (by simpa using hs))

Premises used: SSet.Subcomplex.N.mk'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
x y : A.N
rw : x.toN = y.toN ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }
rw₁ rw₂ : x.toS = y.toS ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }
⊢ x = y ↔ { dim := x.dim, simplex := x.simplex : X.S } = { dim := y.dim, simplex := y.simplex }

Tactic:
rw [N.ext_iff, SSet.N.ext_iff]

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
x x_1 : A.N
⊢ x.toN = x_1.toN → x = x_1

Tactic:
simp [ext_iff]

Premises used: SSet.Subcomplex.N.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
x y : A.N
⊢ x ≤ y ↔ x.toN ≤ y.toN

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
x y : A.N
⊢ x < y ↔ x.toN < y.toN

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
s : A.N
d : ℕ
hd : s.dim = d
subst : s.cast ⋯ = s
⊢ s.cast hd = s

Tactic:
subst hd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
Goal:
X : SSet
A : X.Subcomplex
s : A.N
⊢ s.cast ⋯ = s

Tactic:
rfl
-- 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
subst :
  ∀ (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))⦌)
⊢ 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:
subst hA