awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
S : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)
A : Δ[n].Subcomplex
obtain :
  ∀ (x : (↑(Δ[n].nonDegenerate d) : Type u)),
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
        (↑((Equiv.symm nonDegenerateEquiv' :
                (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
              (((nonDegenerateEquiv' :
                      (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                    (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                  x :
                (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
          Δ[n] _⦋d⦌) ↔
      face
          (↑(((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x) :
            Finset (Fin (n + 1))) ≤
        A
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            S) :
        Δ[n] _⦋d⦌) ↔
    face (↑S : Finset (Fin (n + 1))) ≤ A

Tactic:
obtain ⟨x, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
A : Δ[n].Subcomplex
x : (↑(Δ[n].nonDegenerate d) : Type u)
rw :
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌) ≤ A
rw₁ :
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n] _⦋d⦌) ↔ Subcomplex.ofSimplex (↑x : Δ[n] _⦋d⦌) ≤ A
rw₂ rw₃ :
  Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n] _⦋d⦌) ↔
    Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌)) (↑x : Δ[n] _⦋d⦌)
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (A.obj (op ⦋d⦌))
      (↑((Equiv.symm nonDegenerateEquiv' :
              (a : (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) → (↑(Δ[n].nonDegenerate d) : Type u))
            (((nonDegenerateEquiv' :
                    (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                  (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
                x :
              (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))) :
        Δ[n] _⦋d⦌) ↔
    face
        (↑(((nonDegenerateEquiv' :
                  (↑(Δ[n].nonDegenerate d) : Type u) ≃ (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type)) :
                (a : (↑(Δ[n].nonDegenerate d) : Type u)) → (↑{S : Finset (Fin (n + 1)) | #S = d + 1} : Type))
              x) :
          Finset (Fin (n + 1))) ≤
      A

Tactic:
rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff]

Premises used: Equiv.symm_apply_apply, SSet.Subcomplex.ofSimplex_le_iff, SSet.stdSimplex.face_nonDegenerateEquiv'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d : SimplexCategoryᵒᵖ
rw : Finite (unop d ⟶ n)
⊢ Finite.{u + 1} ((stdSimplex.obj n).obj d)

Tactic:
rw [objEquiv.finite_iff]

Premises used: Equiv.finite_iff, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d : SimplexCategoryᵒᵖ
⊢ Finite (unop d ⟶ n)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
mk : ∀ (n : ℕ), SSet.Finite.{u} Δ[n]
⊢ SSet.Finite.{u} (stdSimplex.obj n)

Tactic:
induction n using SimplexCategory.rec with | _ n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
⊢ SSet.Finite.{u} Δ[n]

Tactic:
finite_of_hasDimensionLT _ (n + 1) inferInstance

Premises used: SSet.finite_of_hasDimensionLT, inferInstance, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
⊢ SSet.Finite.{u} Δ[n]

Tactic:
exact finite_of_hasDimensionLT _ (n + 1) inferInstance

Premises used: SSet.finite_of_hasDimensionLT, inferInstance, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : ℕ
x : X _⦋n⦌
obtain :
  ∀ (f : Δ[n] ⟶ X),
    SSet.Finite.{u}
      (Subcomplex.toSSet (X := X) (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ X) → X _⦋n⦌) f)))
⊢ SSet.Finite.{u} (Subcomplex.ofSimplex x).toSSet

Tactic:
obtain ⟨f, rfl⟩ := yonedaEquiv.surjective x

Premises used: SSet.yonedaEquiv, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : ℕ
f : Δ[n] ⟶ X
rw : SSet.Finite.{u} (Subcomplex.range f).toSSet
⊢ SSet.Finite.{u}
    (Subcomplex.toSSet (X := X) (Subcomplex.ofSimplex (n := n) ((yonedaEquiv : (a : Δ[n] ⟶ X) → X _⦋n⦌) f)))

Tactic:
rw [← Subcomplex.range_eq_ofSimplex]

Premises used: SSet.Subcomplex.range_eq_ofSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
X : SSet
n : ℕ
f : Δ[n] ⟶ X
⊢ SSet.Finite.{u} (Subcomplex.range f).toSSet

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
generalize : ∀ (m : ℕ) (hm : #S = m), HasDimensionLT.{u} (face S).toSSet d
⊢ HasDimensionLT.{u} (face S).toSSet d

Tactic:
generalize hm : S.card = m

Premises used: Finset.card
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m
zero : ∀ (hm : #S = 0), HasDimensionLT.{u} (face S).toSSet d
succ : ∀ (m : ℕ) (hm : #S = m + 1), HasDimensionLT.{u} (face S).toSSet d
⊢ HasDimensionLT.{u} (face S).toSSet d

Tactic:
obtain _ | m := m
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
hm rwa rwa₁ rwa₂ rwa₃ : #S = 0
⊢ S = ∅

Tactic:
rwa [← Finset.card_eq_zero]

Premises used: Finset.card_eq_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
hm : #S = 0
zero :
  ∀ (hd : card (α := Fin (n + 1)) ∅ ≤ d) (hm : card (α := Fin (n + 1)) ∅ = 0),
    HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) (face ∅)) d
⊢ HasDimensionLT.{u} (face S).toSSet d

Tactic:
obtain rfl : S = ∅ := by rwa [← Finset.card_eq_zero]

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
hd : card (α := Fin (n + 1)) ∅ ≤ d
hm : card (α := Fin (n + 1)) ∅ = 0
zero : HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) ⊥) d
⊢ HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) (face ∅)) d

Tactic:
rw [face_empty]

Premises used: SSet.stdSimplex.face_empty
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d : ℕ
hd : card (α := Fin (n + 1)) ∅ ≤ d
hm : card (α := Fin (n + 1)) ∅ = 0
⊢ HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) ⊥) d

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ Fintype.card ↥S = m + 1

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
succ : HasDimensionLT.{u} Δ[m] d
⊢ HasDimensionLT.{u} (face S).toSSet d

Tactic:
rw [← hasDimensionLT_iff_of_iso
      (isoOfRepresentableBy (faceRepresentableBy S m (monoEquivOfFin S (by simpa))))]

Premises used: monoEquivOfFin, Membership.mem, Subtype, SSet.stdSimplex.faceRepresentableBy, SSet.hasDimensionLT_iff_of_iso, SSet.stdSimplex.isoOfRepresentableBy
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ HasDimensionLT.{u} Δ[m] d

Tactic:
hasDimensionLT_of_le _ (m + 1) _

Premises used: SSet.hasDimensionLT_of_le, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ HasDimensionLT.{u} Δ[m] d

Tactic:
exact hasDimensionLT_of_le _ (m + 1) _

Premises used: SSet.hasDimensionLT_of_le, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
⊢ LE.le.{u} (α := Δ[n].Subcomplex)
    (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌))) ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x_1 : SimplexCategoryᵒᵖ
x : Δ[n].obj x_1
h : Membership.mem (γ := Set (Δ[n].obj x_1)) (Subfunctor.obj ⊤ x_1) x
obtain :
  ∀ (f : unop x_1 ⟶ ⦋n⦌),
    Membership.mem.{u, u} (α := Δ[n].obj x_1) (γ := Set (Δ[n].obj x_1)) (Subfunctor.obj ⊤ x_1)
        ((Equiv.symm objEquiv : (a : unop x_1 ⟶ ⦋n⦌) → Δ[n].obj x_1) f : Δ[n].obj x_1) →
      Membership.mem.{u, u} (α := Δ[n].obj x_1) (γ := Set (Δ[n].obj x_1))
        (Subfunctor.obj
          (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌))) x_1)
        ((Equiv.symm objEquiv : (a : unop x_1 ⟶ ⦋n⦌) → Δ[n].obj x_1) f : Δ[n].obj x_1)
⊢ Membership.mem (γ := Set (Δ[n].obj x_1))
    (Subfunctor.obj
      (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌))) x_1)
    x

Tactic:
obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x

Premises used: Equiv.surjective, Equiv.symm, SSet.stdSimplex.objEquiv, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
f : unop x ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n].obj x) (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)
simp :
  ∃ (f_1 : unop x ⟶ ⦋n⦌),
    Eq (α := Δ[n].obj x)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map f_1.op) : (a : Δ[n] _⦋n⦌) → Δ[n].obj x)
          ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
        Δ[n].obj x)
      ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)
⊢ Membership.mem.{u, u} (α := Δ[n].obj x) (γ := Set (Δ[n].obj x))
    (Subfunctor.obj
      (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌))) x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)

Tactic:
simp only [Subcomplex.mem_ofSimplex_obj_iff, op_unop]

Premises used: SSet.Subcomplex.mem_ofSimplex_obj_iff, Opposite.op_unop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
f : unop x ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n].obj x) (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)
⊢ Eq (α := Δ[n].obj x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map f.op) : (a : Δ[n] _⦋n⦌) → Δ[n].obj x)
        ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
      Δ[n].obj x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)

Tactic:
simp [map_objEquiv_symm.{u}]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
f : unop x ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n].obj x) (γ := Set (Δ[n].obj x)) (Subfunctor.obj ⊤ x)
    ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)
⊢ ∃ (f_1 : unop x ⟶ ⦋n⦌),
    Eq (α := Δ[n].obj x)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map f_1.op) : (a : Δ[n] _⦋n⦌) → Δ[n].obj x)
          ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
        Δ[n].obj x)
      ((Equiv.symm objEquiv : (a : unop x ⟶ ⦋n⦌) → Δ[n].obj x) f : Δ[n].obj x)

Tactic:
exact ⟨f, by simp [map_objEquiv_symm.{u}]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
rw :
  StrictMono (α := Fin (n + 1)) (β := Fin (n + 1))
    (⇑((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
            (𝟙 (unop (op ⦋n⦌))) :
          stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌) :
      (a : Fin (n + 1)) → Fin (n + 1))
⊢ Membership.mem.{u, u} (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
        (𝟙 (unop (op ⦋n⦌))) :
      stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)

Tactic:
rw [mem_nonDegenerate_iff_strictMono]

Premises used: SSet.stdSimplex.mem_nonDegenerate_iff_strictMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
⊢ StrictMono (α := Fin (n + 1)) (β := Fin (n + 1))
    (⇑((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
            (𝟙 (unop (op ⦋n⦌))) :
          stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌) :
      (a : Fin (n + 1)) → Fin (n + 1))

Tactic:
fun _ _ h ↦ h

Premises used: StrictMono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
⊢ StrictMono (α := Fin (n + 1)) (β := Fin (n + 1))
    (⇑((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
            (𝟙 (unop (op ⦋n⦌))) :
          stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌) :
      (a : Fin (n + 1)) → Fin (n + 1))

Tactic:
exact fun _ _ h ↦ h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
h :
  ∀ (x : Δ[n] _⦋n⦌),
    Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x ↔
      Membership.mem (γ := Set (Δ[n] _⦋n⦌))
        (singleton (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
          ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
              (𝟙 (unop (op ⦋n⦌))) :
            stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌))
        x
⊢ Eq (α := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    (singleton (α := stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
      ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ unop (op ⦋n⦌)) → stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌)
          (𝟙 (unop (op ⦋n⦌))) :
        stdSimplex.obj (unop (op ⦋n⦌)) _⦋n⦌))

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : Δ[n] _⦋n⦌
⊢ Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x ↔
    x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : Δ[n] _⦋n⦌
h :
  ∀ (h : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x),
    x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)
h₁ :
  x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) →
    Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x
⊢ Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x ↔
    x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
x : Δ[n] _⦋n⦌
h : Membership.mem (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n) x
h₁ :
  ∀ (f : unop (op ⦋n⦌) ⟶ ⦋n⦌)
    (h :
      Membership.mem.{u, u} (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
        ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)),
    Eq.{u + 1} (α := Δ[n] _⦋n⦌) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
      ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌)
⊢ x = (Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌)

Tactic:
obtain ⟨f, rfl⟩ := objEquiv.symm.surjective x

Premises used: Equiv.surjective, Equiv.symm, SSet.stdSimplex.objEquiv, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
⊢ Mono f

Tactic:
simpa using (mem_nonDegenerate_iff_mono _).mp h

Premises used: Iff.mp, SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
⊢ Mono f

Tactic:
have : Mono f := by simpa using (mem_nonDegenerate_iff_mono _).mp h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h :
  Membership.mem.{u, u} (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
this : Mono f
⊢ Eq.{u + 1} (α := Δ[n] _⦋n⦌) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) f : Δ[n] _⦋n⦌)
    ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌)

Tactic:
simpa only [EmbeddingLike.apply_eq_iff_eq] using SimplexCategory.eq_id_of_mono f

Premises used: EmbeddingLike.apply_eq_iff_eq, SimplexCategory.eq_id_of_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
⊢ Membership.mem.{u, u} (α := Δ[n] _⦋n⦌) (γ := Set (Δ[n] _⦋n⦌)) (Δ[n].nonDegenerate n)
    ((Equiv.symm objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌)

Tactic:
apply objEquiv_symm_id_mem_nonDegenerate

Premises used: SSet.stdSimplex.objEquiv_symm_id_mem_nonDegenerate
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
h : HasDimensionLT.{u} Δ[n] n
⊢ False

Tactic:
(lt_self_iff_false n).1 (Δ[n].dim_lt_of_nonDegenerate
    (nonDegenerateEquiv.2 (.refl _)) n)

Premises used: SSet.dim_lt_of_nonDegenerate, RelEmbedding.refl, SSet.stdSimplex, SSet.stdSimplex.nonDegenerateEquiv, SimplexCategory.mk, lt_self_iff_false, Iff.mp, CategoryTheory.Functor.obj, Equiv.invFun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
d n : ℕ
f : Δ[n].op _⦋d⦌
i : Fin (d + 1)
⊢ Eq (α := Fin (n + 1))
    ((((stdSimplex.opObjEquiv : (a : Δ[n].op _⦋d⦌) → Δ[n] _⦋d⦌) f : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i :
      Fin (n + 1))
    (Fin.rev ((((opObjEquiv : (a : Δ[n].op _⦋d⦌) → Δ[n] _⦋d⦌) f : Δ[n] _⦋d⦌) : (a : Fin (d + 1)) → Fin (n + 1)) i.rev) :
      Fin (n + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
d n : ℕ
f : Δ[n] _⦋d⦌
i : Fin (d + 1)
⊢ Eq (α := Fin (n + 1))
    ((((opObjEquiv : (a : Δ[n].op _⦋d⦌) → Δ[n] _⦋d⦌)
              ((Equiv.symm stdSimplex.opObjEquiv : (a : Δ[n] _⦋d⦌) → Δ[n].op _⦋d⦌) f : Δ[n].op _⦋d⦌) :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    (Fin.rev ((f : (a : Fin (d + 1)) → Fin (n + 1)) i.rev) : Fin (n + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n d d' : ℕ
f : ⦋d⦌ ⟶ ⦋d'⦌
g : Δ[n] _⦋d'⦌
i : Fin (d + 1)
⊢ Eq (α := Fin (n + 1))
    ((((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map (rev.map f).op) : (a : Δ[n] _⦋d'⦌) → Δ[n] _⦋d⦌) g :
            Δ[n] _⦋d⦌) :
          (a : Fin (d + 1)) → Fin (n + 1))
        i :
      Fin (n + 1))
    ((g : (a : Fin (d' + 1)) → Fin (n + 1))
        (Fin.rev
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : Fin (d + 1)) → Fin (d' + 1))
            i.rev)) :
      Fin (n + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
h :
  ∀ (g : (stdSimplex.obj n).op.obj d),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((stdSimplex.obj n).op.map f ≫
            Iso.hom
              ((fun (d : SimplexCategoryᵒᵖ) ↦
                  (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
                d')))
        g =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (d : SimplexCategoryᵒᵖ) ↦
                  (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
                d) ≫
            (stdSimplex.obj n).map f))
        g
⊢ (stdSimplex.obj n).op.map f ≫
      Iso.hom
        ((fun (d : SimplexCategoryᵒᵖ) ↦
            (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
          d') =
    Iso.hom
        ((fun (d : SimplexCategoryᵒᵖ) ↦
            (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
          d) ≫
      (stdSimplex.obj n).map f

Tactic:
ext g
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((stdSimplex.obj n).op.map f ≫
          Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d) ≫
          (stdSimplex.obj n).map f))
      g

Tactic:
stdSimplex.ext _ _ (fun i ↦ ?_)

Premises used: SSet.stdSimplex.ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
h :
  ∀ (i : Fin (len d'.1 + 1)),
    Eq (α := Fin (n.len + 1))
      ((TypeCat.Fun.toFun
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                ((stdSimplex.obj n).op.map f ≫
                  Iso.hom
                    ((fun (d : SimplexCategoryᵒᵖ) ↦
                        (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
                      d')))
              g :
            (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
          i :
        Fin (n.len + 1))
      ((TypeCat.Fun.toFun
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.hom
                    ((fun (d : SimplexCategoryᵒᵖ) ↦
                        (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
                      d) ≫
                  (stdSimplex.obj n).map f))
              g :
            (a : Fin (d'.1.len + 1)) → Fin (n.len + 1))
          i :
        Fin (n.len + 1))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((stdSimplex.obj n).op.map f ≫
          Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d')))
      g =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (d : SimplexCategoryᵒᵖ) ↦
                (Equiv.toIso stdSimplex.opObjEquiv : (stdSimplex.obj n).op.obj d ≅ (stdSimplex.obj n).obj d))
              d) ≫
          (stdSimplex.obj n).map f))
      g

Tactic:
refine stdSimplex.ext _ _ (fun i ↦ ?_)

Premises used: SSet.stdSimplex.ext