awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
hi : n + 1 ≤ i
h :
  ∀ (x : Δ[n] _⦋i⦌),
    Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x ↔ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) ⊤ x
⊢ Eq.{u + 1} (α := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) ⊤

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
h : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x ↔ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) ⊤ x

Tactic:
simp only [Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: iff_true, Set.top_eq_univ, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
h : ∀ (hx : x ∉ Δ[n].degenerate i), False
⊢ Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].degenerate i) x

Tactic:
by_contra hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Set (Δ[n] _⦋i⦌)) (Δ[n].nonDegenerate i) x
⊢ Mono (C := SimplexCategory) (X := unop (op ⦋i⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x)

Tactic:
rwa [← mem_nonDegenerate_iff_mono]

Premises used: SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
⊢ Mono (C := SimplexCategory) (X := unop (op ⦋i⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x)

Tactic:
have : Mono (objEquiv x) := by rwa [← mem_nonDegenerate_iff_mono]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
this :
  Mono (C := SimplexCategory) (X := unop (op ⦋i⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x)
⊢ (unop (op ⦋i⦌)).len ≤ ⦋n⦌.len

Tactic:
have := SimplexCategory.len_le_of_mono (objEquiv x)
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n i : ℕ
hi : n + 1 ≤ i
x : Δ[n] _⦋i⦌
hx : x ∉ Δ[n].degenerate i
this_1 :
  Mono (C := SimplexCategory) (X := unop (op ⦋i⦌)) (Y := ⦋n⦌)
    (((objEquiv : Δ[n] _⦋i⦌ ≃ (unop (op ⦋i⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋i⦌) → unop (op ⦋i⦌) ⟶ ⦋n⦌) x)
this : i ≤ n
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
x_1 : { x : Fin (n + 1 + 1) // x ≠ i }
x : Fin (n + 1 + 1)
hx : x ≠ i
⊢ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x

Tactic:
simpa using hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
x_1 : ↥{i}ᶜ
x : Fin (n + 2)
hx : Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x
⊢ x ≠ i

Tactic:
simpa using hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Eq.{u + 1} (α := Δ[n + 1].Subcomplex) (face {i}ᶜ)
    (Subcomplex.ofSimplex (n := n) ((Equiv.symm objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (δ i)))

Tactic:
face_eq_ofSimplex _ _ (finSuccAboveOrderIsoFinset i)

Premises used: Fin.succAbove, Option.casesOn', SimplexCategory.mkHom, SSet.stdSimplex.face_eq_ofSimplex, SimplexCategory.δ, SSet.stdSimplex.finSuccAboveOrderIsoFinset, OrderHom.comp, OrderEmbedding.toOrderHom, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i : Fin (n + 2)
⊢ (faceSingletonComplIso i).hom ≫ Subcomplex.ι (face {i}ᶜ) = stdSimplex.δ i

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Fin.succAbove, Option.casesOn', CategoryTheory.CosimplicialObject.δ, CategoryTheory.Functor.comp, OrderHom.comp, TypeCat.Fun.comp, CategoryTheory.Functor.whiskerRight, SimplexCategory.Hom.comp, rfl, ite, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
refine_1 : ∀ (k : Fin n), Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove ((i.castPred ⋯).succAbove k))
refine_2 :
  ∀ (x x_1 : Fin n)
    (hk :
      Eq (α := ↥{i, j}ᶜ)
        ((fun (k : Fin n) ↦
            Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
              (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
          x)
        ((fun (k : Fin n) ↦
            Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
              (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
          x_1)),
    x = x_1
refine_3 :
  ∀ (x : ↥{i, j}ᶜ) (l : Fin (n + 2)) (hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ l),
    ∃ (a : Fin n),
      (fun (k : Fin n) ↦
            Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
              (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
          a =
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) l hl
⊢ Fin n ≃ ↥{i, j}ᶜ

Tactic:
refine Equiv.ofBijective
      (fun k ↦ ⟨j.succAbove ((i.castPred (Fin.ne_last_of_lt h)).succAbove k), ?_⟩)
        ⟨fun _ _ hk ↦ ?_, fun ⟨l, hl⟩ ↦ ?_⟩

Premises used: And.intro, Equiv.ofBijective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
k : Fin n
⊢ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove ((i.castPred ⋯).succAbove k))

Tactic:
grind [compl_insert, mem_compl, Fin.succAbove, Fin.castPred]

Premises used: Fin.succAbove, Fin.castPred, Finset.compl_insert, Finset.mem_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x x_1 : Fin n
hk :
  Eq (α := ↥{i, j}ᶜ)
    ((fun (k : Fin n) ↦
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
          (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
      x)
    ((fun (k : Fin n) ↦
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
          (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
      x_1)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hk :
      Eq (α := Fin (n + 2))
        (↑((fun (k : Fin n) ↦
                Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
                  (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
              x) :
          Fin (n + 2))
        (↑((fun (k : Fin n) ↦
                Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
                  (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
              x_1) :
          Fin (n + 2))),
    Eq (α := Fin (n + 1 + 1))
      ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
              fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb :
            (a : Fin n) → Fin (n + 1 + 1))
          x :
        Fin (n + 1 + 1))
      ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
              fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb :
            (a : Fin n) → Fin (n + 1 + 1))
          x_1 :
        Fin (n + 1 + 1))
⊢ Eq (α := Fin (n + 1 + 1))
    ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
            fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb :
          (a : Fin n) → Fin (n + 1 + 1))
        x :
      Fin (n + 1 + 1))
    ((RelEmbedding.trans (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) (t :=
            fun (x1 x2 : Fin (n + 1 + 1)) ↦ x1 ≤ x2) (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb :
          (a : Fin n) → Fin (n + 1 + 1))
        x_1 :
      Fin (n + 1 + 1))

Tactic:
rwa [Subtype.ext_iff] at hk

Premises used: Subtype.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x x_1 : Fin n
hk :
  Eq (α := ↥{i, j}ᶜ)
    ((fun (k : Fin n) ↦
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
          (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
      x)
    ((fun (k : Fin n) ↦
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
          (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
      x_1)
⊢ x = x_1

Tactic:
exact ((Fin.succAboveOrderEmb (i.castPred (Fin.ne_last_of_lt h))).trans
        (Fin.succAboveOrderEmb j)).injective (by rwa [Subtype.ext_iff] at hk)

Premises used: RelEmbedding.injective, Fin.castPred, Fin.succAboveOrderEmb, RelEmbedding.trans, Fin.ne_last_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ l
⊢ l ∈ Set.range j.succAbove

Tactic:
grind [Fin.range_succAbove, mem_compl, Fin.succAbove]

Premises used: Fin.succAbove, Finset.mem_compl, Fin.range_succAbove
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ l
refine_3 :
  ∀ (m : Fin (n + 1)) (hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove m)),
    ∃ (a : Fin n),
      (fun (k : Fin n) ↦
            Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
              (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
          a =
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m)
          hl
⊢ ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) l hl

Tactic:
obtain ⟨m, rfl⟩ : l ∈ Set.range j.succAbove := by
        grind [Fin.range_succAbove, mem_compl, Fin.succAbove]

Premises used: Fin.succAbove, Set.range, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove m)
⊢ m ∈ Set.range (i.castPred ⋯).succAbove

Tactic:
grind [Fin.range_succAbove, compl_insert, Fin.succAbove, Fin.castPred]

Premises used: Fin.succAbove, Fin.castPred, Finset.compl_insert, Fin.range_succAbove
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove m)
refine_3 :
  ∀ (k : Fin n) (hk : (i.castPred ⋯).succAbove k = m),
    ∃ (a : Fin n),
      (fun (k : Fin n) ↦
            Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
              (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
          a =
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m)
          hl
⊢ ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m) hl

Tactic:
obtain ⟨k, hk⟩ : m ∈ Set.range (i.castPred (Fin.ne_last_of_lt h)).succAbove := by
        grind [Fin.range_succAbove, compl_insert, Fin.succAbove, Fin.castPred]

Premises used: Fin.succAbove, Fin.castPred, Set.range, Fin.ne_last_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove m)
k : Fin n
hk : (i.castPred ⋯).succAbove k = m
⊢ (fun (k : Fin n) ↦
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
          (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
      k =
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m) hl

Tactic:
simp [hk]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
x : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ (j.succAbove m)
k : Fin n
hk : (i.castPred ⋯).succAbove k = m
⊢ ∃ (a : Fin n),
    (fun (k : Fin n) ↦
          Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x)
            (j.succAbove ((i.castPred ⋯).succAbove k)) ⋯)
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i, j}ᶜ x) (j.succAbove m) hl

Tactic:
exact ⟨k, by simp [hk]⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i < j
k : Fin n
⊢ (↑((finOrderIsoPairCompl i j h : (a : Fin n) → ↥{i, j}ᶜ) k) : Fin (n + 2)) = j.succAbove ((i.castPred ⋯).succAbove k)

Tactic:
rfl

Premises used: Fin.succAbove, rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ (facePairComplIso i j h).hom ≫ Subcomplex.ι (face {i, j}ᶜ) = stdSimplex.δ (i.castPred ⋯) ≫ stdSimplex.δ j

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, Fin.succAbove, CategoryTheory.CosimplicialObject.δ, OrderHom.comp, TypeCat.Fun.comp, CategoryTheory.Functor.whiskerRight, SimplexCategory.Hom.comp, rfl, ite, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
rw : stdSimplex.δ (i.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i
⊢ (facePairComplIso i j h).hom ≫ Subcomplex.ι (face {i, j}ᶜ) = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i

Tactic:
rw [facePairComplIso_hom_ι]

Premises used: SSet.stdSimplex.facePairComplIso_hom_ι
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
obtain :
  ∀ (i : Fin (n + 2)) (h : i.castSucc < j),
    stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i.castSucc
⊢ stdSimplex.δ (i.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i

Tactic:
obtain ⟨i, rfl⟩ := i.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Premises used: Fin.eq_castSucc_of_ne_last, Fin.ne_last_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
h : i.castSucc < j
obtain :
  ∀ (j : Fin (n + 2)) (h : i.castSucc < j.succ),
    stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc
⊢ stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i.castSucc

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)

Premises used: Fin.eq_succ_of_ne_zero, Fin.ne_zero_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
dsimp : stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc
⊢ stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
⊢ i ≤ j

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
rw : stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ j ≫ stdSimplex.δ i.castSucc
rw₁ rw₂ : stdSimplex.δ j ≫ stdSimplex.δ i.castSucc = stdSimplex.δ j ≫ stdSimplex.δ i.castSucc
⊢ stdSimplex.δ i ≫ stdSimplex.δ j.succ = stdSimplex.δ (j.succ.pred ⋯) ≫ stdSimplex.δ i.castSucc

Tactic:
rw [Fin.pred_succ, stdSimplex.δ_comp_δ (by grind)]

Premises used: CategoryTheory.CosimplicialObject.δ_comp_δ, Fin.pred_succ, SSet.stdSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ LE.le.{u} (α := Δ[n + 1 + 1].Subcomplex) (face {i, j}ᶜ) (face {i}ᶜ)

Tactic:
simp [face_le_face_iff]

Premises used: SSet.stdSimplex.face_le_face_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso i).inv = (facePairComplIso i j h).inv ≫ stdSimplex.δ (j.pred ⋯)

Tactic:
simp [← cancel_mono (faceSingletonComplIso i).hom,
    ← cancel_mono (Subcomplex.ι _), ← cancel_epi (facePairComplIso i j h).hom,
    facePairComplIso_hom_ι']

Premises used: SSet.stdSimplex.facePairComplIso_hom_ι', CategoryTheory.cancel_mono, SSet.stdSimplex.facePairComplIso, SSet.stdSimplex.faceSingletonComplIso, SSet.Subcomplex.ι, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ LE.le.{u} (α := Δ[n + 1 + 1].Subcomplex) (face {i, j}ᶜ) (face {j}ᶜ)

Tactic:
simp [face_le_face_iff]

Premises used: SSet.stdSimplex.face_le_face_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso j).inv = (facePairComplIso i j h).inv ≫ stdSimplex.δ (i.castPred ⋯)

Tactic:
simp [← cancel_mono (faceSingletonComplIso j).hom,
    ← cancel_mono (Subcomplex.ι _), ← cancel_epi (facePairComplIso i j h).hom,
    facePairComplIso_hom_ι]

Premises used: CategoryTheory.cancel_mono, SSet.stdSimplex.facePairComplIso, SSet.stdSimplex.facePairComplIso_hom_ι, SSet.stdSimplex.faceSingletonComplIso, SSet.Subcomplex.ι, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
⊢ CategoryStruct.comp (Y := Subcomplex.toSSet (X := Δ[1]) (face {0})) (Iso.hom (faceSingletonIso 0))
      (Subcomplex.ι (face {0})) =
    stdSimplex.δ 1

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
⊢ CategoryStruct.comp (Y := Subcomplex.toSSet (X := Δ[1]) (face {1})) (Iso.hom (faceSingletonIso 1))
      (Subcomplex.ι (face {1})) =
    stdSimplex.δ 0

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
dsimp :
  card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1))
        (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
          (a : Fin (m + 1)) → Fin (n + 1))
        univ) =
    m + 1
⊢ Membership.mem (γ := Set (Finset (Fin (n + 1)))) {S : Finset (Fin (n + 1)) | #S = m + 1}
    (Finset.image (α := Fin ((unop (op ⦋m⦌)).len + 1))
      (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
        (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
      univ)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx : Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x
⊢ Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))

Tactic:
rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective] at hx

Premises used: SimplexCategory.mono_iff_injective, SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx :
  Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
⊢ Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
      (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx :
  Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
⊢ Function.Injective (α := Fin (m + 1)) (β := Fin (n + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
      (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
exact hx
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
Goal:
n m : ℕ
x_1 : { x : Δ[n] _⦋m⦌ // Membership.mem (γ := Set (Δ[n] _⦋m⦌)) (Δ[n].nonDegenerate m) x }
x : Δ[n] _⦋m⦌
hx :
  Function.Injective (α := Fin ((unop (op ⦋m⦌)).len + 1)) (β := Fin (⦋n⦌.len + 1))
    (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → unop (op ⦋m⦌) ⟶ ⦋n⦌) x)) :
      (a : Fin ((unop (op ⦋m⦌)).len + 1)) → Fin (⦋n⦌.len + 1))
rw : card (α := Fin (m + 1)) univ = m + 1
rw₁ : Fintype.card (Fin (m + 1)) = m + 1
rw₂ rw₃ : m + 1 = m + 1
⊢ card (α := Fin (n + 1))
      (Finset.image (α := Fin (m + 1))
        (⇑(Hom.toOrderHom (((objEquiv : Δ[n] _⦋m⦌ ≃ (unop (op ⦋m⦌) ⟶ ⦋n⦌)) : (a : Δ[n] _⦋m⦌) → ⦋m⦌ ⟶ ⦋n⦌) x)) :
          (a : Fin (m + 1)) → Fin (n + 1))
        univ) =
    m + 1

Tactic:
rw [Finset.card_image_of_injective _ (by exact hx), Finset.card_univ,
          Fintype.card_fin]

Premises used: Finset.card_univ, Fintype.card_fin, Finset.card_image_of_injective