mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
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 : ↑(Fin.castAdd (x₂.len + 1) 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)
        (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)
        (Fin.natAdd (x₁.len + 1) i✝))

Tactic:
]

Goal state after:
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 : ↑(Fin.castAdd (x₂.len + 1) 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)
        (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)
        (Fin.natAdd (x₁.len + 1) i✝))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
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 : ↑(Fin.natAdd (x₁.len + 1) 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)
        (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)
        (Fin.castAdd (x₂.len + 1) i✝))

Tactic:
]

Goal state after:
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 : ↑(Fin.natAdd (x₁.len + 1) 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)
        (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)
        (Fin.castAdd (x₂.len + 1) i✝))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : ↑(Fin.natAdd (x₁.len + 1) 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)
        (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)
        (Fin.natAdd (x₁.len + 1) i✝))

Tactic:
]

Goal state after:
case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : ↑(Fin.natAdd (x₁.len + 1) 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)
        (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)
        (Fin.natAdd (x₁.len + 1) i✝))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: 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

pp: 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

Tactic:
· intro h' i hi
    by_contra!
    exact hi.not_ge (by simpa using h' i.castSucc (by simpa))

Goal state after:
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.SimplicialObject.II

Goal state before:
pp: case inl
n : ℕ
x : Fin (n + 1)
⊢ x.castSucc ≤ (OrderHom.id x).castSucc ∧ ∀ i < x, (OrderHom.id i).castSucc < x.castSucc

Tactic:
]

Goal state after:
case inl
n : ℕ
x : Fin (n + 1)
⊢ x.castSucc ≤ (OrderHom.id x).castSucc ∧ ∀ i < x, (OrderHom.id i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case 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 : map' g x.castSucc = y.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
]

Goal state after:
case 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 : map' g x.castSucc = y.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case 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
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
]

Goal state after:
case 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
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ j)) = ↑((ConcreteCategory.hom g) (Fin.cast ⋯ j))

Tactic:
]

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ j)) = ↑((ConcreteCategory.hom g) (Fin.cast ⋯ j))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g))
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j)))

Tactic:
]

Goal state after:
case left
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inl' x y ≫ g))
h₂ : inr' x y ≫ f = inr' x y ≫ g
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (x.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.castAdd (y.len + 1) j)))
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
f : Path i.as j.as
g : Path j.as k.as
l : J
⊢ l ∈ f.I ∪ g.I → l ≤ k.as

Tactic:
rintro (h | h)
      exacts [(f.le_right _ h).trans (Path.le g), (g.le_right l h)]

Goal state after:
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 : map' f y.castSucc = z.castSucc
⊢ map' (g.comp f) x.castSucc = z.castSucc

Tactic:
]

Goal state after:
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 : map' f y.castSucc = z.castSucc
⊢ map' (g.comp f) x.castSucc = z.castSucc
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:
]

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case right
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g))
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (y.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j)))

Tactic:
]

Goal state after:
case right
x✝ y✝ z✝ : AugmentedSimplexCategory
f✝ g✝ : x✝ ⊗ y✝ ⟶ z✝
x y z : SimplexCategory
f g : tensorObjOf x y ⟶ z
h₁ : inl' x y ≫ f = inl' x y ≫ g
h₂ : ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ f)) = ⇑(SimplexCategory.Hom.toOrderHom (inr' x y ≫ g))
i : Fin ((tensorObjOf x y).len + 1)
j✝ : Fin (x.len + 1 + (y.len + 1)) := Fin.cast ⋯ i
this : i = Fin.cast ⋯ j✝
j : Fin (y.len + 1)
⊢ ↑((ConcreteCategory.hom f) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j))) =
    ↑((ConcreteCategory.hom g) (Fin.cast ⋯ (Fin.natAdd (x.len + 1) j)))
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))
⊢ (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 ⋯)) (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)))) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))

Tactic:
]

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))
⊢ (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 ⋯)) (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)))) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inr
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
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)

Tactic:
]

Goal state after:
case inl.inl.inr
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
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: 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
⊢ EnrichedFunctor.comp SSet
      (EnrichedFunctor.id SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1))))) x✝ =
    (ConcreteCategory.hom
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x✝

Tactic:
]

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
⊢ EnrichedFunctor.comp SSet
      (EnrichedFunctor.id SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1))))) x✝ =
    (ConcreteCategory.hom
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inr
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
hz : ∀ (i : Fin (n + 1)), (f i).castSucc < y.castSucc
⊢ ∀ (i : Fin (n + 1)), ((g.comp f) i).castSucc < x.castSucc

Tactic:
]

Goal state after:
case inl.inl.inr
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
hz : ∀ (i : Fin (n + 1)), (f i).castSucc < y.castSucc
⊢ ∀ (i : Fin (n + 1)), ((g.comp f) i).castSucc < x.castSucc
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✝
x✝ : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X✝).len + 1)))) C
⊢ EnrichedFunctor.comp SSet
      (EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)
        (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap))
      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✝

Tactic:
]

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
⊢ EnrichedFunctor.comp SSet
      (EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)
        (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap))
      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 inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)

Tactic:
]

Goal state after:
case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : ∀ (i : Fin (m + 1)), (g i).castSucc < x.castSucc
⊢ ∀ (i : Fin (n + 1)), ((g.comp f) i).castSucc < x.castSucc

Tactic:
]

Goal state after:
case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : ∀ (i : Fin (m + 1)), (g i).castSucc < x.castSucc
⊢ ∀ (i : Fin (n + 1)), ((g.comp f) i).castSucc < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
x y : A.N
⊢ x.toS = y.toS ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = x

Tactic:
]

Goal state after:
case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = 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 (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 ⋯)) (Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)))) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))

Tactic:
]

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 ⋯)) (Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)))) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ d + 1 = d + 1

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
⊢ d + 1 = d + 1

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.left.inl
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc ≤ x.castSucc

pp: case pos.inl.left.inl.h
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc < i

Tactic:
]

Goal state after:
case pos.inl.left.inl.h
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx✝ : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc < i
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ j < x

Tactic:
]

Goal state after:
case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ j < x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex ∈
    (y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌)

Tactic:
]

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex ∈
    (y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
⊢ d + 1 = d + 1

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ x.succ.castSucc ≤ (i.succAboveOrderEmb.toOrderHom x).castSucc ∧
    ∀ i_1 < x, (i.succAboveOrderEmb.toOrderHom i_1).castSucc < x.succ.castSucc

Tactic:
]

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ x.succ.castSucc ≤ (i.succAboveOrderEmb.toOrderHom x).castSucc ∧
    ∀ i_1 < x, (i.succAboveOrderEmb.toOrderHom i_1).castSucc < x.succ.castSucc