mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons.inl
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : j < a
⊢ j ∈ a :: L

pp: case cons.inr.inl
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : j = a
⊢ j ∈ a :: L

pp: case cons.inr.inr
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : a < j
⊢ j ∈ a :: L

Tactic:
<;>

Goal state after:
case cons.inl
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : j < a
⊢ j ∈ a :: L

case cons.inr.inl
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : j = a
⊢ j ∈ a :: L

case cons.inr.inr
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : a < j
⊢ j ∈ a :: L
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 0 ≤ 0

pp: case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 0 ≤ 1

pp: case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 1 ≤ 0

pp: case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 1 ≤ 1

Tactic:
<;>

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 0 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 0 ≤ 1

case pos
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : j₂.castSucc < i
⊢ 1 ≤ 0

case neg
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h✝¹ : ¬j₁.castSucc < i
h✝ : ¬j₂.castSucc < i
⊢ 1 ≤ 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case succ
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
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this : (ConcreteCategory.hom (X.map α.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map (α.hom ≫ (inclusion 2).op.map (Hom.right β₁)))) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app α₁)) x

Tactic:
Functor.map_comp_apply

Goal state after:
case succ
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
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this : (ConcreteCategory.hom (X.map α.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map ((inclusion 2).op.map (Hom.right β₁))))
      ((ConcreteCategory.hom (X.map α.hom)) (lift sx s x)) =
    (ConcreteCategory.hom (s.π.app α₁)) x
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right.inr
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
ht : a✝ ∈ {t | ∃ v, t = {v}}
⊢ a✝ ∈ (fun K ↦ K.faces) L

Tactic:
obtain ⟨v, hv⟩ := ht
        exact hv ▸ L.singleton_mem v

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i✝ : Fin (x₁.len + 1)
h : Fin.castAdd (x₂.len + 1) i✝ ≤ j
⊢ (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)
      (Fin.castAdd (x₂.len + 1) i✝) ≤
    (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)
      j

pp: case right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i✝ : Fin (x₂.len + 1)
h : Fin.natAdd (x₁.len + 1) i✝ ≤ j
⊢ (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)
      (Fin.natAdd (x₁.len + 1) i✝) ≤
    (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)
      j

Tactic:
<;>

Goal state after:
case left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i✝ : Fin (x₁.len + 1)
h : Fin.castAdd (x₂.len + 1) i✝ ≤ j
⊢ (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)
      (Fin.castAdd (x₂.len + 1) i✝) ≤
    (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)
      j

case right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
j : Fin (x₁.len + 1 + (x₂.len + 1))
i✝ : Fin (x₂.len + 1)
h : Fin.natAdd (x₁.len + 1) i✝ ≤ j
⊢ (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)
      (Fin.natAdd (x₁.len + 1) i✝) ≤
    (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)
      j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : i✝¹ ≤ i✝
⊢ (SimplexCategory.Hom.toOrderHom f₁) i✝¹ ≤ (SimplexCategory.Hom.toOrderHom f₁) i✝

pp: case left.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₁.len + 1)
i✝ : Fin (x₂.len + 1)
h : ↑i✝¹ ≤ x₁.len + 1 + ↑i✝
⊢ ↑((SimplexCategory.Hom.toOrderHom f₁) i✝¹) ≤ y₁.len + 1 + ↑((SimplexCategory.Hom.toOrderHom f₂) i✝)

pp: case right.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₂.len + 1)
i✝ : Fin (x₁.len + 1)
h : x₁.len + 1 + ↑i✝¹ ≤ ↑i✝
⊢ y₁.len + 1 + ↑((SimplexCategory.Hom.toOrderHom f₂) i✝¹) ≤ ↑((SimplexCategory.Hom.toOrderHom f₁) i✝)

pp: case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : i✝¹ ≤ i✝
⊢ (SimplexCategory.Hom.toOrderHom f₂) i✝¹ ≤ (SimplexCategory.Hom.toOrderHom f₂) i✝

Tactic:
<;>

Goal state after:
case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : i✝¹ ≤ i✝
⊢ (SimplexCategory.Hom.toOrderHom f₁) i✝¹ ≤ (SimplexCategory.Hom.toOrderHom f₁) i✝

case left.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₁.len + 1)
i✝ : Fin (x₂.len + 1)
h : ↑i✝¹ ≤ x₁.len + 1 + ↑i✝
⊢ ↑((SimplexCategory.Hom.toOrderHom f₁) i✝¹) ≤ y₁.len + 1 + ↑((SimplexCategory.Hom.toOrderHom f₂) i✝)

case right.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₂.len + 1)
i✝ : Fin (x₁.len + 1)
h : x₁.len + 1 + ↑i✝¹ ≤ ↑i✝
⊢ y₁.len + 1 + ↑((SimplexCategory.Hom.toOrderHom f₂) i✝¹) ≤ ↑((SimplexCategory.Hom.toOrderHom f₁) i✝)

case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : i✝¹ ≤ i✝
⊢ (SimplexCategory.Hom.toOrderHom f₂) i✝¹ ≤ (SimplexCategory.Hom.toOrderHom f₂) i✝
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case of
a✝ : SimplexCategory
⊢ WithInitial.of a✝ ◁ 𝟙 WithInitial.star = 𝟙 (WithInitial.of a✝ ⊗ WithInitial.star)

pp: case star
⊢ WithInitial.star ◁ 𝟙 WithInitial.star = 𝟙 (WithInitial.star ⊗ WithInitial.star)

Tactic:
<;>

Goal state after:
case of
a✝ : SimplexCategory
⊢ WithInitial.of a✝ ◁ 𝟙 WithInitial.star = 𝟙 (WithInitial.of a✝ ⊗ WithInitial.star)

case star
⊢ WithInitial.star ◁ 𝟙 WithInitial.star = 𝟙 (WithInitial.star ⊗ WithInitial.star)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case of
a✝ : SimplexCategory
⊢ 𝟙 WithInitial.star ▷ WithInitial.of a✝ = 𝟙 (WithInitial.star ⊗ WithInitial.of a✝)

pp: case star
⊢ 𝟙 WithInitial.star ▷ WithInitial.star = 𝟙 (WithInitial.star ⊗ WithInitial.star)

Tactic:
<;>

Goal state after:
case of
a✝ : SimplexCategory
⊢ 𝟙 WithInitial.star ▷ WithInitial.of a✝ = 𝟙 (WithInitial.star ⊗ WithInitial.of a✝)

case star
⊢ 𝟙 WithInitial.star ▷ WithInitial.star = 𝟙 (WithInitial.star ⊗ WithInitial.star)
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
    change EnrichedFunctor.comp SSet (SimplicialThickening.functor
      (f.unop.toOrderHom.uliftMap.comp g.unop.toOrderHom.uliftMap)) _ = _
    rw [SimplicialThickening.functor_comp]
    rfl

Goal state after:
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 (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
⊢ (SimplexCategory.Hom.toOrderHom (eqToHom ⋯))
      ({
          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' := ⋯ }
        ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯)) ((SimplexCategory.Hom.toOrderHom (inr' x₁ x₂)) i))) =
    (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i)

Tactic:
have e₂ := inr'_eval y₁ y₂ <| (WithInitial.down f₂).toOrderHom i

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 (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))
⊢ (SimplexCategory.Hom.toOrderHom (eqToHom ⋯))
      ({
          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' := ⋯ }
        ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯)) ((SimplexCategory.Hom.toOrderHom (inr' x₁ x₂)) i))) =
    (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ Fin.cast ⋯ ((SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i) =
    (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) ((SimplexCategory.Hom.toOrderHom (inr' y z)) i)

Tactic:
rw [e₁, e₂, e₃]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (z.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inr' (tensorObjOf x y) z)) i = Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)
e₂ : (SimplexCategory.Hom.toOrderHom (inr' y z)) i = Fin.cast ⋯ (Fin.natAdd y.len.succ i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inr' x (tensorObjOf y z))) (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
⊢ Fin.cast ⋯ (Fin.cast ⋯ (Fin.natAdd (x.len + y.len + 1).succ i)) =
    Fin.cast ⋯ (Fin.natAdd x.len.succ (Fin.cast ⋯ (Fin.natAdd (y.len + 1) i)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X Y : SSet
e : X ≅ Y
dx : ℕ
x : X _⦋dx⦌
y : X _⦋dx + 1⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace { dim := dx + 1, simplex := y }
⊢ hxy.index ⋯ = ⋯.index ⋯

Tactic:
simp [← (hxy.of_iso e).δ_eq_iff rfl,
    ← SSet.δ_naturality_apply, dsimp% hxy.δ_index rfl]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      ((SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) ((SimplexCategory.Hom.toOrderHom (inl' x y)) i)) =
    (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i

Tactic:
rw [e₁, e₂, e₃]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
i : Fin (x.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x y)) i = Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)
e₂ : (SimplexCategory.Hom.toOrderHom (inl' x (tensorObjOf y z))) i = Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
e₃ :
  (SimplexCategory.Hom.toOrderHom (inl' (tensorObjOf x y) z)) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)) =
    Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))
⊢ (SimplexCategory.Hom.toOrderHom (WithInitial.down (eqToHom ⋯)))
      (Fin.cast ⋯ (Fin.castAdd (z.len + 1) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) i)))) =
    Fin.cast ⋯ (Fin.castAdd (y.len + z.len + 1 + 1) i)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case h₁.h₁.h₁
w x y z : AugmentedSimplexCategory
⊢ w.inl x ≫
      (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    w.inl x ≫ (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

pp: case h₁.h₁.h₂
w x y z : AugmentedSimplexCategory
⊢ w.inr x ≫
      (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    w.inr x ≫ (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

pp: case h₁.h₂
w x y z : AugmentedSimplexCategory
⊢ (w ⊗ x).inr y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    (w ⊗ x).inr y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

pp: case h₂
w x y z : AugmentedSimplexCategory
⊢ ((w ⊗ x) ⊗ y).inr z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    ((w ⊗ x) ⊗ y).inr z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

Tactic:
<;>

Goal state after:
case h₁.h₁.h₁
w x y z : AugmentedSimplexCategory
⊢ w.inl x ≫
      (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    w.inl x ≫ (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

case h₁.h₁.h₂
w x y z : AugmentedSimplexCategory
⊢ w.inr x ≫
      (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    w.inr x ≫ (w ⊗ x).inl y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

case h₁.h₂
w x y z : AugmentedSimplexCategory
⊢ (w ⊗ x).inr y ≫ ((w ⊗ x) ⊗ y).inl z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    (w ⊗ x).inr y ≫ ((w ⊗ x) ⊗ y).inl z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom

case h₂
w x y z : AugmentedSimplexCategory
⊢ ((w ⊗ x) ⊗ y).inr z ≫ ((α_ w x y).hom ⊗ₘ 𝟙 z) ≫ (α_ w (x ⊗ y) z).hom ≫ (𝟙 w ⊗ₘ (α_ x y z).hom) =
    ((w ⊗ x) ⊗ y).inr z ≫ (α_ (w ⊗ x) y z).hom ≫ (α_ w x (y ⊗ z)).hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: case left
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ ((pair X Y).obj { as := WalkingPair.left }).Finite

pp: case right
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ ((pair X Y).obj { as := WalkingPair.right }).Finite

Tactic:
<;>

Goal state after:
case left
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ ((pair X Y).obj { as := WalkingPair.left }).Finite

case right
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ ((pair X Y).obj { as := WalkingPair.right }).Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits

Goal state before:
pp: case left
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ X.Finite

pp: case right
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ Y.Finite

Tactic:
<;>

Goal state after:
case left
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ X.Finite

case right
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ Y.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
t : (range (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN t
⊢ Cell.type₁ f c = t

pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
t : (range (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN t
⊢ Cell.type₂ f c = t

Tactic:
<;>

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
t : (range (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN t
⊢ Cell.type₁ f c = t

case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
t : (range (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN t
⊢ Cell.type₂ f c = t