awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
s : X.N
__S : X.S := s.cast ⋯
⊢ Membership.mem (γ := Set (X _⦋(s.cast ⋯).dim⦌)) (X.nonDegenerate (s.cast ⋯).dim) (s.cast ⋯).simplex

Tactic:
s.nonDegenerate

Premises used: Set.Mem, cast, SSet.N.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
s : X.N
__S : X.S := s.cast ⋯
⊢ Membership.mem (γ := Set (X _⦋(s.cast ⋯).dim⦌)) (X.nonDegenerate (s.cast ⋯).dim) (s.cast ⋯).simplex

Tactic:
exact s.nonDegenerate

Premises used: SSet.N.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
s : X.N
d : ℕ
hd : s.dim = d
subst : s.cast ⋯ = s
⊢ s.cast hd = s

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

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
⊢ LE.le.{u} (α := X.Subcomplex) (⨆ (s : X.N), s.subcomplex) ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
rw :
  ∀ (i : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
    Subcomplex.ofSimplex (↑(i.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋i.fst⦌) ≤
      ⨆ (s : X.N), s.subcomplex
⊢ LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (s : X.N), s.subcomplex)

Tactic:
rw [← Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top X, iSup_le_iff]

Premises used: SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, iSup_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
d : ℕ
s : X _⦋d⦌
hs : s ∈ X.nonDegenerate d
⊢ LE.le.{u} (α := X.Subcomplex)
    (Subcomplex.ofSimplex (n :=
      Sigma.fst (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))
        (Sigma.mk (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u)) d
          (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) s hs)))
      (↑(Sigma.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))
            (Sigma.mk (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u)) d
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) s hs))) :
        X _⦋⟨d, ⟨s, hs⟩⟩.fst⦌))
    (Subcomplex.ofSimplex (n :=
      Sigma.fst (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))
        (Sigma.mk (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u)) d
          (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) s hs)))
      (↑(Sigma.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))
            (Sigma.mk (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u)) d
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) s hs))) :
        X _⦋⟨d, ⟨s, hs⟩⟩.fst⦌))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
d : ℕ
s : X _⦋d⦌
hs : s ∈ X.nonDegenerate d
⊢ LE.le.{u} (α := X.Subcomplex)
    (Subcomplex.ofSimplex (n :=
      Sigma.fst (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))
        (Sigma.mk (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u)) d
          (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) s hs)))
      (↑(Sigma.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))
            (Sigma.mk (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u)) d
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦ x ∈ X.nonDegenerate d) s hs))) :
        X _⦋⟨d, ⟨s, hs⟩⟩.fst⦌))
    (⨆ (s : X.N), s.subcomplex)

Tactic:
exact le_trans (by rfl) (le_iSup _ (N.mk _ hs))

Premises used: SSet.N.mk, le_iSup, le_trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
rw :
  (∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
⊢ A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]

Premises used: SSet.Subcomplex.le_iff_contains_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
⟨fun h s ↦ ?_, fun h n x hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
refine_1 :
  ∀
    (h :
      ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
        Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
          Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌))
    (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
refine_2 :
  ∀ (h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B) (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u))
    (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)),
    Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ (∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
refine ⟨fun h s ↦ ?_, fun h n x hx ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : (mk (↑x : X _⦋n⦌) ⋯).subcomplex ≤ A
refine_1 :
  ∀ (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)),
    Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ (mk (↑x : X _⦋n⦌) ⋯).subcomplex ≤ B

Tactic:
simp only [Subfunctor.ofSection_le_iff, mk_dim, mk_simplex] at hx ⊢

Premises used: SSet.N.mk_dim, SSet.N.mk_simplex, CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)

Tactic:
h _ _ hx

Premises used: Set.Mem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)

Tactic:
exact h _ _ hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
s : X.N
refine_1 :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    (mk (↑x : X _⦋n⦌) ⋯).subcomplex ≤ A → (mk (↑x : X _⦋n⦌) ⋯).subcomplex ≤ B
⊢ s.subcomplex ≤ A → s.subcomplex ≤ B

Tactic:
induction s using N.induction with
    | mk n x =>
      intro hx
      simp only [Subfunctor.ofSection_le_iff, mk_dim, mk_simplex] at hx ⊢
      exact h _ _ hx

Premises used: SSet.N.mk, SSet.N.mk_dim, SSet.N.mk_simplex, CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ (mk (↑x : X _⦋n⦌) ⋯).subcomplex ≤ A

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
A B : X.Subcomplex
h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
⊢ Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)

Tactic:
simpa using h (N.mk _ x.prop) (by simpa)

Premises used: SSet.N.mk, Subtype.prop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x : X.op.N
⊢ Membership.mem (α := X _⦋x.dim⦌) (γ := Set (X _⦋x.dim⦌)) (X.nonDegenerate x.dim)
    ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex : X _⦋x.dim⦌)

Tactic:
simpa only [opObjEquiv_mem_nonDegenerate_iff] using x.nonDegenerate

Premises used: SSet.opObjEquiv_mem_nonDegenerate_iff, SSet.N.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
y : X.N
⊢ Membership.mem (α := X.op _⦋y.dim⦌) (γ := Set (X.op _⦋y.dim⦌)) (X.op.nonDegenerate y.dim)
    ((Equiv.symm opObjEquiv : (a : X _⦋y.dim⦌) → X.op _⦋y.dim⦌) y.simplex : X.op _⦋y.dim⦌)

Tactic:
simpa [← opObjEquiv_mem_nonDegenerate_iff] using y.nonDegenerate

Premises used: SSet.opObjEquiv_mem_nonDegenerate_iff, SSet.N.nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.op.N
dsimp :
  mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯ ≤
      mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯ ↔
    x ≤ y
⊢ LE.le (α := X.N)
      (({ toFun := fun (x : X.op.N) ↦ mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯,
              invFun := fun (y : X.N) ↦ mk ((Equiv.symm opObjEquiv : (a : X _⦋y.dim⦌) → X.op _⦋y.dim⦌) y.simplex) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.op.N) → X.N)
          x :
        X.N)
      (({ toFun := fun (x : X.op.N) ↦ mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯,
              invFun := fun (y : X.N) ↦ mk ((Equiv.symm opObjEquiv : (a : X _⦋y.dim⦌) → X.op _⦋y.dim⦌) y.simplex) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.op.N) → X.N)
          y :
        X.N) ↔
    x ≤ y

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.op.N
simp :
  (∃ (f :
      ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
        ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
              X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
          (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
        (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
        x.simplex
⊢ mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯ ≤
      mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯ ↔
    x ≤ y

Tactic:
simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]

Premises used: SSet.Subcomplex.mem_ofSimplex_obj_iff, SSet.Subcomplex.ofSimplex_le_iff, SSet.N.le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.op.N
mp :
  (∃ (f :
      ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
        ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
              X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
          (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
        (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex) →
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
        x.simplex
mpr :
  (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
        x.simplex) →
    ∃ (f :
      ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
        ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
              X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
          (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
        (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex
⊢ (∃ (f :
      ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
        ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
              X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
          (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
        (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
        x.simplex

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.op.N
f :
  ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
    ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
          X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
      (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
    (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map (SimplexCategory.rev.map f).op) :
        (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌)
      y.simplex =
    x.simplex

Tactic:
simp [op_map, dsimp% hf]

Premises used: SSet.op_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.op.N
f :
  ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
    ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
          X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
      (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
    (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex
⊢ ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
      x.simplex

Tactic:
exact ⟨SimplexCategory.rev.map f, by simp [op_map, dsimp% hf]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.op.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex = x.simplex
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.rev.map f).op) :
        (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
          X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
      (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
    (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex

Tactic:
simp [op_map, ← hf]

Premises used: SSet.op_map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X : SSet
x y : X.op.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex = x.simplex
⊢ ∃ (f :
    ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
      ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
            X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
        (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
      (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex

Tactic:
exact ⟨SimplexCategory.rev.map f, by simp [op_map, ← hf]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x : X.N
⊢ (fun (y : Y.N) ↦
        mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋y.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋y.dim⦌))
            y.simplex)
          ⋯)
      ((fun (x : X.N) ↦
          mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
              x.simplex)
            ⋯)
        x) =
    x

Tactic:
simp [N.ext_iff, S.ext_iff']

Premises used: SSet.N.ext_iff, SSet.S.ext_iff'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x : Y.N
⊢ (fun (x : X.N) ↦
        mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
            x.simplex)
          ⋯)
      ((fun (y : Y.N) ↦
          mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋y.dim⦌)) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋y.dim⦌))
              y.simplex)
            ⋯)
        x) =
    x

Tactic:
simp [N.ext_iff, S.ext_iff']

Premises used: SSet.N.ext_iff, SSet.S.ext_iff'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
dsimp :
  mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex)
        ⋯ ≤
      mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
          y.simplex)
        ⋯ ↔
    x ≤ y
⊢ LE.le (α := Y.N)
      (({
              toFun := fun (x : X.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
                    x.simplex)
                  ⋯,
              invFun := fun (y : Y.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋y.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋y.dim⦌))
                    y.simplex)
                  ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.N) → Y.N)
          x :
        Y.N)
      (({
              toFun := fun (x : X.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
                    x.simplex)
                  ⋯,
              invFun := fun (y : Y.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋y.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋y.dim⦌))
                    y.simplex)
                  ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.N) → Y.N)
          y :
        Y.N) ↔
    x ≤ y

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
simp :
  (∃ (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
⊢ mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex)
        ⋯ ≤
      mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
          y.simplex)
        ⋯ ↔
    x ≤ y

Tactic:
simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]

Premises used: SSet.Subcomplex.mem_ofSimplex_obj_iff, SSet.Subcomplex.ofSimplex_le_iff, SSet.N.le_iff