awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
⊢ (∃ (f :
      ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                  (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
                x.simplex)
              ⋯).dim⦌ ⟶
        ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
            (a :
                Y _⦋(mk
                      ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                        y.simplex)
                      ⋯).dim⦌) →
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                    ⋯).dim⦌)
          (mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).simplex =
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
              x.simplex)
            ⋯).simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
exists_congr (fun f ↦ ?_)

Premises used: exists_congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
refine :
  ∀
    (f :
      ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                  (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
                x.simplex)
              ⋯).dim⦌ ⟶
        ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
            (a :
                Y _⦋(mk
                      ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                        y.simplex)
                      ⋯).dim⦌) →
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                    ⋯).dim⦌)
          (mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).simplex =
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
              x.simplex)
            ⋯).simplex ↔
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
⊢ (∃ (f :
      ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                  (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
                x.simplex)
              ⋯).dim⦌ ⟶
        ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
            (a :
                Y _⦋(mk
                      ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                        y.simplex)
                      ⋯).dim⦌) →
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                    ⋯).dim⦌)
          (mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).simplex =
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
              x.simplex)
            ⋯).simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
refine exists_congr (fun f ↦ ?_)

Premises used: exists_congr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
f :
  ⦋(mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
            x.simplex)
          ⋯).dim⦌ ⟶
    ⦋(mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
            y.simplex)
          ⋯).dim⦌
dsimp :
  Eq (α := Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) : (a : Y _⦋y.dim⦌) → Y _⦋x.dim⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex :
            Y _⦋y.dim⦌) :
        Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex :
        Y _⦋x.dim⦌) ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
          (a :
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌) y.simplex)
                    ⋯).dim⦌) →
            Y _⦋(mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                  ⋯).dim⦌)
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex)
            ⋯).simplex =
      (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
            x.simplex)
          ⋯).simplex ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
dsimp at f ⊢
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
rw :
  Eq (α := Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex :
            X _⦋x.dim⦌) :
        Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex :
        Y _⦋x.dim⦌) ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
⊢ Eq (α := Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) : (a : Y _⦋y.dim⦌) → Y _⦋x.dim⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex :
            Y _⦋y.dim⦌) :
        Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex :
        Y _⦋x.dim⦌) ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
rw [← NatTrans.naturality_apply e.hom f.op]

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ Eq (α := Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex :
            X _⦋x.dim⦌) :
        Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex :
        Y _⦋x.dim⦌) ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
(e.app _).toEquiv.apply_eq_iff_eq

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Iso.app, Equiv.apply_eq_iff_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ Eq (α := Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex :
            X _⦋x.dim⦌) :
        Y _⦋x.dim⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex :
        Y _⦋x.dim⦌) ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex

Tactic:
exact (e.app _).toEquiv.apply_eq_iff_eq

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Iso.app, Equiv.apply_eq_iff_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
a : x ≤ x_1
a₁ : x_1 ≤ x
⊢ x = x_1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
a : x.subcomplex ≤ x_1.subcomplex
a₁ a₂ : x_1.subcomplex ≤ x_1.subcomplex
⊢ x ≤ x_1

Tactic:
rw [N.le_iff, h]

Premises used: SSet.N.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x x_1 : X.N
h : x.subcomplex = x_1.subcomplex
a : x_1.subcomplex ≤ x.subcomplex
a₁ a₂ : x_1.subcomplex ≤ x_1.subcomplex
⊢ x_1 ≤ x

Tactic:
rw [N.le_iff, h]

Premises used: SSet.N.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
trans : { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy
trans₁ : N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y
⊢ { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

Tactic:
trans N.mk x hx = N.mk y hy

Premises used: SSet.N.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy

Tactic:
(N.ext_iff (N.mk x hx) (N.mk y hy)).symm

Premises used: SSet.N.mk, SSet.N.ext_iff, Iff.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x : X.S } = { dim := m, simplex := y } ↔ N.mk x hx = N.mk y hy

Tactic:
exact (N.ext_iff (N.mk x hx) (N.mk y hy)).symm

Premises used: SSet.N.mk, SSet.N.ext_iff, Iff.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
simp :
  N.mk x hx ≤ N.mk y hy ∧ N.mk y hy ≤ N.mk x hx ↔
    Subcomplex.ofSimplex x ≤ Subcomplex.ofSimplex y ∧ Subcomplex.ofSimplex y ≤ Subcomplex.ofSimplex x
⊢ N.mk x hx = N.mk y hy ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

Tactic:
simp only [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ N.mk x hx ≤ N.mk y hy ∧ N.mk y hy ≤ N.mk x hx ↔
    Subcomplex.ofSimplex x ≤ Subcomplex.ofSimplex y ∧ Subcomplex.ofSimplex y ≤ Subcomplex.ofSimplex x

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (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
simp : Membership.mem (γ := Set (X _⦋x.dim⦌)) (y.subcomplex.obj (Opposite.op ⦋x.dim⦌)) x.simplex
⊢ x.subcomplex ≤ y.subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]

Premises used: SSet.Subcomplex.ofSimplex_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (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
⊢ Membership.mem (γ := Set (X _⦋x.dim⦌)) (y.subcomplex.obj (Opposite.op ⦋x.dim⦌)) x.simplex

Tactic:
⟨_, hf⟩

Premises used: Set.Mem, setOf, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (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
⊢ Membership.mem (γ := Set (X _⦋x.dim⦌)) (y.subcomplex.obj (Opposite.op ⦋x.dim⦌)) x.simplex

Tactic:
exact ⟨_, hf⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (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
⊢ x.subcomplex = y.subcomplex

Tactic:
le_antisymm (subcomplex_map_le x y f hf) ?_

Premises used: le_antisymm, SSet.S.subcomplex_map_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (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
refine : y.subcomplex ≤ x.subcomplex
⊢ x.subcomplex = y.subcomplex

Tactic:
refine le_antisymm (subcomplex_map_le x y f hf) ?_

Premises used: le_antisymm, SSet.S.subcomplex_map_le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (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
simp : Membership.mem (γ := Set (X _⦋y.dim⦌)) (x.subcomplex.obj (Opposite.op ⦋y.dim⦌)) y.simplex
⊢ y.subcomplex ≤ x.subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]

Premises used: SSet.Subcomplex.ofSimplex_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (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
⊢ IsSplitEpi f

Tactic:
have := isSplitEpi_of_epi f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (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
this : IsSplitEpi f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (section_ f).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋y.dim⦌))
      x.simplex =
    y.simplex

Tactic:
simp [← hf, ← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst : Epi f
hf :
  (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
this : IsSplitEpi f
⊢ Membership.mem (γ := Set (X _⦋y.dim⦌)) (x.subcomplex.obj (Opposite.op ⦋y.dim⦌)) y.simplex

Tactic:
exact ⟨(section_ f).op, by simp [← hf, ← Functor.map_comp_apply, ← op_comp]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.S
obtain : ∀ (n : ℕ) (x : X _⦋n⦌), ∃ (x_1 : X.N), x_1.subcomplex = { dim := n, simplex := x }.subcomplex
⊢ ∃ (x_1 : X.N), x_1.subcomplex = x.subcomplex

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

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
obtain :
  ∀ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌),
    Epi f →
      ∀ (y : (↑(X.nonDegenerate m) : Type u)),
        ∃ (x : X.N),
          x.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⦌))
                  (↑y : X _⦋m⦌)))
⊢ ∃ (x_1 : X.N), x_1.subcomplex = { dim := n, simplex := x }.subcomplex

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

Premises used: SSet.exists_nonDegenerate, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
⊢ ∃ (x : X.N),
    x.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⦌))
            (↑y : X _⦋m⦌)))

Tactic:
⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩

Premises used: SSet.N.mk, le_antisymm, Subtype.prop, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
refine_1 :
  (N.mk (↑y : X _⦋m⦌) ⋯).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⦌))
          (↑y : X _⦋m⦌)))
refine_2 :
  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
⊢ ∃ (x : X.N),
    x.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⦌))
            (↑y : X _⦋m⦌)))

Tactic:
refine ⟨N.mk _ y.prop, le_antisymm ?_ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
refine_1 :
  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
⊢ (N.mk (↑y : X _⦋m⦌) ⋯).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⦌))
          (↑y : X _⦋m⦌)))

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)
⊢ IsSplitEpi f

Tactic:
have := isSplitEpi_of_epi f
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this : IsSplitEpi f
rw : Mono (X.map f.op)
⊢ 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⦌))

Tactic:
rw [← mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this : IsSplitEpi f
⊢ Mono (X.map f.op)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w : Epi f
y : (↑(X.nonDegenerate m) : Type u)
this : IsSplitEpi f
⊢ 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⦌))

Tactic:
have : Function.Injective (X.map f.op) := by
        rw [← mono_iff_injective]
        infer_instance
-- 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⦌))
⊢ 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:
⟨(section_ f).op, this ?_⟩

Premises used: Set.Mem, Quiver.Hom.op, setOf, Exists.intro, CategoryTheory.section_