mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x✝ : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x✝) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
x : Fin ((unop ((inclusion 2).op.obj α₀.right)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop) x) =
    ↑((Hom.toOrderHom α₀.hom.unop) x)

Tactic:
fin_cases x

Goal state after:
case «0»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom α₀.hom.unop) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop)
        ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₀.right)).len, ⋯⟩)) =
    ↑((Hom.toOrderHom α₀.hom.unop) ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₀.right)).len, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi (toSimplexCategory.map e)

Tactic:
constructor

Goal state after:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ Nonempty (SplitEpi (toSimplexCategory.map e))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ Nonempty (SplitEpi (toSimplexCategory.map e))

Tactic:
constructor

Goal state after:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ SplitEpi (toSimplexCategory.map e)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ IsSplitMono (toSimplexCategory.map m)

Tactic:
constructor

Goal state after:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ Nonempty (SplitMono (toSimplexCategory.map m))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ Nonempty (SplitMono (toSimplexCategory.map m))

Tactic:
constructor

Goal state after:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ SplitMono (toSimplexCategory.map m)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
⊢ Fin.ofNat (m₂ + 1) a = a₀

Tactic:
ext

Goal state after:
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := ⋯
aux : ∀ (t : Fin (m₂ + 2)), ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t
this : ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯))) ⟨j, hj⟩) = simplicialEvalσ L j
⊢ ↑(Fin.ofNat (m₂ + 1) a) = ↑a₀
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ { toFunctor := functor X Y } ≫ { toFunctor := inverse X Y } = 𝟙 (Cat.of (X ⊗ Y).HomotopyCategory)

Tactic:
ext

Goal state after:
X X' Y Y' Z : Truncated 2
⊢ ({ toFunctor := functor X Y } ≫ { toFunctor := inverse X Y }).toFunctor =
    (𝟙 (Cat.of (X ⊗ Y).HomotopyCategory)).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ { toFunctor := inverse X Y } ≫ { toFunctor := functor X Y } = 𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))

Tactic:
ext

Goal state after:
X X' Y Y' Z : Truncated 2
⊢ ({ toFunctor := inverse X Y } ≫ { toFunctor := functor X Y }).toFunctor =
    (𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X✝ Y✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Truncated 2
⊢ hoFunctor₂.map x✝¹ ▷ hoFunctor₂.obj x✝ ≫ (iso Y✝ x✝).symm.hom = (iso X✝ x✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ▷ x✝)

Tactic:
ext

Goal state after:
X✝ Y✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Truncated 2
⊢ (hoFunctor₂.map x✝¹ ▷ hoFunctor₂.obj x✝ ≫ (iso Y✝ x✝).symm.hom).toFunctor =
    ((iso X✝ x✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ▷ x✝)).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X✝ Y✝ x✝¹ : Truncated 2
x✝ : X✝ ⟶ Y✝
⊢ hoFunctor₂.obj x✝¹ ◁ hoFunctor₂.map x✝ ≫ (iso x✝¹ Y✝).symm.hom = (iso x✝¹ X✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ◁ x✝)

Tactic:
ext

Goal state after:
X✝ Y✝ x✝¹ : Truncated 2
x✝ : X✝ ⟶ Y✝
⊢ (hoFunctor₂.obj x✝¹ ◁ hoFunctor₂.map x✝ ≫ (iso x✝¹ Y✝).symm.hom).toFunctor =
    ((iso x✝¹ X✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ◁ x✝)).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: x✝² x✝¹ x✝ : Truncated 2
⊢ (iso x✝² x✝¹).symm.hom ▷ hoFunctor₂.obj x✝ ≫ (iso (x✝² ⊗ x✝¹) x✝).symm.hom ≫ hoFunctor₂.map (α_ x✝² x✝¹ x✝).hom =
    (α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
      hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom

Tactic:
ext

Goal state after:
x✝² x✝¹ x✝ : Truncated 2
⊢ ((iso x✝² x✝¹).symm.hom ▷ hoFunctor₂.obj x✝ ≫
        (iso (x✝² ⊗ x✝¹) x✝).symm.hom ≫ hoFunctor₂.map (α_ x✝² x✝¹ x✝).hom).toFunctor =
    ((α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
        hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: Y : Truncated 2
⊢ (λ_ (hoFunctor₂.obj Y)).hom =
    (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ▷ hoFunctor₂.obj Y ≫
      (iso (𝟙_ (Truncated 2)) Y).symm.hom ≫ hoFunctor₂.map (λ_ Y).hom

Tactic:
ext

Goal state after:
Y : Truncated 2
⊢ (λ_ (hoFunctor₂.obj Y)).hom.toFunctor =
    ((HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ▷ hoFunctor₂.obj Y ≫
        (iso (𝟙_ (Truncated 2)) Y).symm.hom ≫ hoFunctor₂.map (λ_ Y).hom).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X : Truncated 2
⊢ (ρ_ (hoFunctor₂.obj X)).hom =
    hoFunctor₂.obj X ◁ (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ≫
      (iso X (𝟙_ (Truncated 2))).symm.hom ≫ hoFunctor₂.map (ρ_ X).hom

Tactic:
ext

Goal state after:
X : Truncated 2
⊢ (ρ_ (hoFunctor₂.obj X)).hom.toFunctor =
    (hoFunctor₂.obj X ◁ (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ≫
        (iso X (𝟙_ (Truncated 2))).symm.hom ≫ hoFunctor₂.map (ρ_ X).hom).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty ∧
    ∀ ⦃b : Finset β⦄, b ⊆ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ (Finset.image f s').Nonempty

case right
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
s' : Finset α
hs' : s' ∈ K.faces
⊢ ∀ ⦃b : Finset β⦄, b ⊆ Finset.image f s' → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

case right
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
x✝² x✝¹ : AbstractSimplicialComplex ι
x✝ : (fun K ↦ K.faces) x✝² = (fun K ↦ K.faces) x✝¹
⊢ x✝² = x✝¹

Tactic:
ext

Goal state after:
ι : Type u_1
x✝³ x✝² : AbstractSimplicialComplex ι
x✝¹ : (fun K ↦ K.faces) x✝³ = (fun K ↦ K.faces) x✝²
x✝ : Finset ι
⊢ x✝ ∈ x✝³.faces ↔ x✝ ∈ x✝².faces
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {t | ∃ v, t = {v}}

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

case right
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {t | ∃ v, t = {v}}
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty

case right
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ IsLUB x✝ (sSup x✝)

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ upperBounds x✝

case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ lowerBounds (upperBounds x✝)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) ↔ ∀ (i : Fin (n + 1)), (f i).castSucc < x

Tactic:
constructor

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) → ∀ (i : Fin (n + 1)), (f i).castSucc < x

case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ (i : Fin (n + 1)), (f i).castSucc < x) → ∀ b ∈ finset f x, b = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, (f i).castSucc < x

Tactic:
constructor

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) → ∀ i < y, (f i).castSucc < x

case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ i < y, (f i).castSucc < x) → ∀ b ∈ finset f x, y.castSucc ≤ b
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
i : Fin (x.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)

Tactic:
ext

Goal state after:
x y : SimplexCategory
i : Fin (x.len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom (inl' x y)) i) = ↑(Fin.cast ⋯ (Fin.castAdd (y.len + 1) i))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
i : Fin (y.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom
        (𝟙 (WithInitial.of y) ≫
          𝟙 (WithInitial.of y) ≫ SimplexCategory.Hom.mk (Fin.natAddOrderEmb (x.len + 1)).toOrderHom ≫ eqToHom ⋯))
      i =
    Fin.cast ⋯ (Fin.natAdd (x.len + 1) i)

Tactic:
ext

Goal state after:
x y : SimplexCategory
i : Fin (y.len + 1)
⊢ ↑((SimplexCategory.Hom.toOrderHom
          (𝟙 (WithInitial.of y) ≫
            𝟙 (WithInitial.of y) ≫ SimplexCategory.Hom.mk (Fin.natAddOrderEmb (x.len + 1)).toOrderHom ≫ eqToHom ⋯))
        i) =
    ↑(Fin.cast ⋯ (Fin.natAdd (x.len + 1) i))
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
⊢ x.I = y.I

Tactic:
ext

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
x✝ : J
⊢ x✝ ∈ x.I ↔ x✝ ∈ y.I
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f

Tactic:
ext

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (𝟙 X✝ ≫ f).I ↔ t✝ ∈ f.I
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f

Tactic:
by ext; simpa using fun h ↦ h ▸ f.left

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
⊢ f ≫ 𝟙 Y✝ = f

Tactic:
ext

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (f ≫ 𝟙 Y✝).I ↔ t✝ ∈ f.I
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
⊢ eId SSet i ≫ nerveMap (functorMap f i i) = eId SSet { as := f i.as }

Tactic:
ext

Goal state after:
J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (𝟙_ SSet).obj n✝
⊢ (ConcreteCategory.hom ((eId SSet i ≫ nerveMap (functorMap f i i)).app n✝)).toFun x✝ =
    (ConcreteCategory.hom ((eId SSet { as := f i.as }).app n✝)).toFun x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ x.castSucc ≤ ((g.comp f) z).castSucc ∧ ∀ i < z, ((g.comp f) i).castSucc < x.castSucc

Tactic:
constructor

Goal state after:
case inl.inl.inl.left
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ x.castSucc ≤ ((g.comp f) z).castSucc

case inl.inl.inl.right
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : y.castSucc ≤ (f z).castSucc ∧ ∀ i < z, (f i).castSucc < y.castSucc
⊢ ∀ i < z, ((g.comp f) i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
⊢ eComp SSet i j k ≫ nerveMap (functorMap f i k) =
    (nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
      eComp SSet { as := f i.as } { as := f j.as } { as := f k.as }

Tactic:
ext

Goal state after:
J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : ((i ⟶[SSet] j) ⊗ j ⟶[SSet] k).obj n✝
⊢ (ConcreteCategory.hom ((eComp SSet i j k ≫ nerveMap (functorMap f i k)).app n✝)).toFun x✝ =
    (ConcreteCategory.hom
          (((nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
                eComp SSet { as := f i.as } { as := f j.as } { as := f k.as }).app
            n✝)).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ (functor OrderHom.id).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.id SSet (SimplicialThickening J)).map i j

Tactic:
ext

Goal state after:
J : Type u
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (i ⟶[SSet] j).obj n✝
⊢ (ConcreteCategory.hom (((functor OrderHom.id).map i j ≫ eqToHom ⋯).app n✝)).toFun x✝ =
    (ConcreteCategory.hom (((EnrichedFunctor.id SSet (SimplicialThickening J)).map i j).app n✝)).toFun x✝
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
⊢ (functor (g.comp f)).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.comp SSet (functor f) (functor g)).map i j

Tactic:
ext

Goal state after:
J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
x✝ : (i ⟶[SSet] j).obj n✝
⊢ (ConcreteCategory.hom (((functor (g.comp f)).map i j ≫ eqToHom ⋯).app n✝)).toFun x✝ =
    (ConcreteCategory.hom (((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n✝)).toFun x✝
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
i : SimplexCategoryᵒᵖ
⊢ ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (𝟙 i).unop).uliftMap) =
    𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
i : SimplexCategoryᵒᵖ
x✝ : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
⊢ (ConcreteCategory.hom
          (↾EnrichedFunctor.comp SSet
              (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (𝟙 i).unop).uliftMap))).toFun
      x✝ =
    (ConcreteCategory.hom
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i = Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))
| {
      toFun := fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i,
      monotone' := ⋯ }
    (Fin.castAdd (x₂.len + 1) i)

Tactic:
change Fin.addCases
        (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
        (fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i))
        (Fin.castAdd (x₂.len + 1) i)
      rw [Fin.addCases_left]

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
i : Fin (x₁.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i = Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))
| Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i)
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
X✝ Y✝ Z✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap) =
    ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
      ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : SimplicialCategory C
X✝ Y✝ Z✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X✝).len + 1)))) C
⊢ (ConcreteCategory.hom
          (↾EnrichedFunctor.comp SSet
              (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap))).toFun
      x✝ =
    (ConcreteCategory.hom
          (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
            ↾EnrichedFunctor.comp SSet
                (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ x.castSucc ≤ i.succAbove x ∧ ∀ i_1 < x, i.succAbove i_1 < x.castSucc

Tactic:
constructor

Goal state after:
case pos.inl.left
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ x.castSucc ≤ i.succAbove x

case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ ∀ i_1 < x, i.succAbove i_1 < x.castSucc