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

Goal state before:
pp: case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 0

pp: case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv =
    stdSimplex.δ 0

Tactic:
<;>

Goal state after:
case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 0

case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 2 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv =
    stdSimplex.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

pp: case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0

Tactic:
<;>

Goal state after:
case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv =
    stdSimplex.δ 2

case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv) ≫ f₀ =
    (((stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv) ≫ f₃

Tactic:
convert! h₁₂ <;> decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv =
    stdSimplex.δ 2

pp: case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 1

Tactic:
<;>

Goal state after:
case e'_2
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 1).inv =
    stdSimplex.δ 2

case e'_3
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ((stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 3).inv =
    stdSimplex.δ 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case «0»
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ ↑(((stdSimplex.spineId (n + 2)).arrow j) ((fun i ↦ i) ⟨0, ⋯⟩)) = ↑(↑(primitiveEdge h₀ hₙ j) ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case «1»
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ ↑(((stdSimplex.spineId (n + 2)).arrow j) ((fun i ↦ i) ⟨1, ⋯⟩)) = ↑(↑(primitiveEdge h₀ hₙ j) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
<;>

Goal state after:
case «0»
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ ↑(((stdSimplex.spineId (n + 2)).arrow j) ((fun i ↦ i) ⟨0, ⋯⟩)) = ↑(↑(primitiveEdge h₀ hₙ j) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ ↑(((stdSimplex.spineId (n + 2)).arrow j) ((fun i ↦ i) ⟨1, ⋯⟩)) = ↑(↑(primitiveEdge h₀ hₙ j) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).vertex i = f.vertex i.castSucc

Tactic:
simp only [SimplicialObject.δ, spine_vertex]
  rw [← Functor.map_comp_apply, ← op_comp, SimplexCategory.const_comp,
    spineToSimplex_vertex]
  simp only [SimplexCategory.δ, Hom.toOrderHom, len_mk, mkHom, Hom.mk,
    OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply]
  rw [Fin.succAbove_of_castSucc_lt j i h]

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case «0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
m : Fin (1 + 1)
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
m : Fin (1 + 1)
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
m : Fin (1 + 1)
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
m : Fin (1 + 1)
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩ ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ.«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑(horn.primitiveTriangle i h₀ hₙ ↑k ⋯)))
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    (stdSimplex.objEquiv.symm (intervalEdge (↑k) 2 ⋯)) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.inr.inr.succ.«1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑(horn.primitiveTriangle i h₀ hₙ ↑k ⋯)))
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    (stdSimplex.objEquiv.symm (intervalEdge (↑k) 2 ⋯)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case h.inr.inr.succ.«0»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑(horn.primitiveTriangle i h₀ hₙ ↑k ⋯)))
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    (stdSimplex.objEquiv.symm (intervalEdge (↑k) 2 ⋯)) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.inr.inr.succ.«1»
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑(horn.primitiveTriangle i h₀ hₙ ↑k ⋯)))
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    (stdSimplex.objEquiv.symm (intervalEdge (↑k) 2 ⋯)) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ eHomWhiskerLeft V X (g ≫ g') = eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g'

Tactic:
dsimp [eHomWhiskerLeft]

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) (g ≫ g') ≫ eComp V X Y Y'' =
    ((ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫ eComp V X Y Y') ≫
      (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ eHomWhiskerLeft V X g = (X ⟶[V] Y) ◁ eHomWhiskerLeft V Y g ≫ eComp V X Y Z'

Tactic:
dsimp [eHomWhiskerLeft]

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ eComp V X Y Z ≫ (ρ_ (X ⟶[V] Z)).inv ≫ (X ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V X Z Z' =
    (X ⟶[V] Y) ◁ ((ρ_ (Y ⟶[V] Z)).inv ≫ (Y ⟶[V] Z) ◁ (eHomEquiv V) g ≫ eComp V Y Z Z') ≫ eComp V X Y Z'
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ (α_ (F.obj (P ⟶[V] Q)) (F.obj (Q ⟶[V] R)) (F.obj (R ⟶[V] S))).inv ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] R) ▷ F.obj (R ⟶[V] S) ≫
        F.map (eComp V P Q R) ▷ F.obj (R ⟶[V] S) ≫ μ F (P ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V P R S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)

Tactic:
μ_natural_left_assoc,

Goal state after:
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
P Q R S : TransportEnrichment F C
⊢ (α_ (F.obj (P ⟶[V] Q)) (F.obj (Q ⟶[V] R)) (F.obj (R ⟶[V] S))).inv ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] R) ▷ F.obj (R ⟶[V] S) ≫
        μ F ((P ⟶[V] Q) ⊗ Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V P Q R ▷ R ⟶[V] S) ≫ F.map (eComp V P R S) =
    F.obj (P ⟶[V] Q) ◁ (μ F (Q ⟶[V] R) (R ⟶[V] S) ≫ F.map (eComp V Q R S)) ≫
      μ F (P ⟶[V] Q) (Q ⟶[V] S) ≫ F.map (eComp V P Q S)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = eId V X

Tactic:
change _ = eId V X.obj

Goal state after:
V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X : P.FullSubcategory
⊢ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) (𝟙 X) = eId V X.obj
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i.castSucc) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j))
    ((Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ j.succ) ≫
      (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i))

Tactic:
exact FreeSimplexQuiver.homRel.σ_comp_σ H

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len

pp: case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len

Tactic:
<;>

Goal state after:
case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len

case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ x✝.len < z✝.len

pp: case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ x✝.len < z✝.len

Tactic:
<;>

Goal state after:
case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ x✝.len < z✝.len

case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ x✝.len < z✝.len
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m a : ℕ
⊢ IsAdmissible m [a] ↔ a ≤ m ∧ (∀ (x : 0 < [].length), a < [][0]) ∧ IsAdmissible (m + 1) []

pp: case cons
m a head✝ : ℕ
tail✝ : List ℕ
⊢ IsAdmissible m (a :: head✝ :: tail✝) ↔
    a ≤ m ∧ (∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]) ∧ IsAdmissible (m + 1) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
m a : ℕ
⊢ IsAdmissible m [a] ↔ a ≤ m ∧ (∀ (x : 0 < [].length), a < [][0]) ∧ IsAdmissible (m + 1) []

case cons
m a head✝ : ℕ
tail✝ : List ℕ
⊢ IsAdmissible m (a :: head✝ :: tail✝) ↔
    a ≤ m ∧ (∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]) ∧ IsAdmissible (m + 1) (head✝ :: tail✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m a : ℕ
h : IsAdmissible m [a]
⊢ IsAdmissible (m + 1) []

pp: case cons
m a head✝ : ℕ
tail✝ : List ℕ
h : IsAdmissible m (a :: head✝ :: tail✝)
⊢ IsAdmissible (m + 1) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
m a : ℕ
h : IsAdmissible m [a]
⊢ IsAdmissible (m + 1) []

case cons
m a head✝ : ℕ
tail✝ : List ℕ
h : IsAdmissible m (a :: head✝ :: tail✝)
⊢ IsAdmissible (m + 1) (head✝ :: tail✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m a : ℕ
ha : a ≤ m
hL : IsAdmissible (m + 1) []
ha' : ∀ (x : 0 < [].length), a < [][0]
⊢ IsAdmissible m [a]

pp: case cons
m a : ℕ
ha : a ≤ m
head✝ : ℕ
tail✝ : List ℕ
hL : IsAdmissible (m + 1) (head✝ :: tail✝)
ha' : ∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]
⊢ IsAdmissible m (a :: head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
m a : ℕ
ha : a ≤ m
hL : IsAdmissible (m + 1) []
ha' : ∀ (x : 0 < [].length), a < [][0]
⊢ IsAdmissible m [a]

case cons
m a : ℕ
ha : a ≤ m
head✝ : ℕ
tail✝ : List ℕ
hL : IsAdmissible (m + 1) (head✝ :: tail✝)
ha' : ∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]
⊢ IsAdmissible m (a :: head✝ :: tail✝)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
a : ℕ
⊢ (simplicialInsert a []).length = [].length + 1

pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (a : ℕ), (simplicialInsert a tail✝).length = tail✝.length + 1
a : ℕ
⊢ (simplicialInsert a (head✝ :: tail✝)).length = (head✝ :: tail✝).length + 1

Tactic:
<;>

Goal state after:
case nil
a : ℕ
⊢ (simplicialInsert a []).length = [].length + 1

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (a : ℕ), (simplicialInsert a tail✝).length = tail✝.length + 1
a : ℕ
⊢ (simplicialInsert a (head✝ :: tail✝)).length = (head✝ :: tail✝).length + 1
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons.nil
a m j : ℕ
hj : j ≤ m
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) [] → ∀ j ≤ m, IsAdmissible m (simplicialInsert j [])
hL : IsAdmissible (m + 1) [a]
⊢ IsAdmissible m (simplicialInsert j [a])

pp: case cons.cons
a m j : ℕ
hj : j ≤ m
head✝ : ℕ
tail✝ : List ℕ
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) (head✝ :: tail✝) → ∀ j ≤ m, IsAdmissible m (simplicialInsert j (head✝ :: tail✝))
hL : IsAdmissible (m + 1) (a :: head✝ :: tail✝)
⊢ IsAdmissible m (simplicialInsert j (a :: head✝ :: tail✝))

Tactic:
<;>

Goal state after:
case cons.nil
a m j : ℕ
hj : j ≤ m
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) [] → ∀ j ≤ m, IsAdmissible m (simplicialInsert j [])
hL : IsAdmissible (m + 1) [a]
⊢ IsAdmissible m (simplicialInsert j [a])

case cons.cons
a m j : ℕ
hj : j ≤ m
head✝ : ℕ
tail✝ : List ℕ
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) (head✝ :: tail✝) → ∀ j ≤ m, IsAdmissible m (simplicialInsert j (head✝ :: tail✝))
hL : IsAdmissible (m + 1) (a :: head✝ :: tail✝)
⊢ IsAdmissible m (simplicialInsert j (a :: head✝ :: tail✝))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
⊢ Monotone (simplicialEvalσ [])

pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : Monotone (simplicialEvalσ tail✝)
⊢ Monotone (simplicialEvalσ (head✝ :: tail✝))

Tactic:
<;>

Goal state after:
case nil
⊢ Monotone (simplicialEvalσ [])

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : Monotone (simplicialEvalσ tail✝)
⊢ Monotone (simplicialEvalσ (head✝ :: tail✝))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m : ℕ
hL : IsAdmissible m []
k : ℕ
hk : k < [].length
⊢ simplicialEvalσ [] [][k] = simplicialEvalσ [] ([][k] + 1)

pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ :
  ∀ {m : ℕ},
    IsAdmissible m tail✝ →
      ∀ {k : ℕ} {hk : k < tail✝.length}, simplicialEvalσ tail✝ tail✝[k] = simplicialEvalσ tail✝ (tail✝[k] + 1)
m : ℕ
hL : IsAdmissible m (head✝ :: tail✝)
k : ℕ
hk : k < (head✝ :: tail✝).length
⊢ simplicialEvalσ (head✝ :: tail✝) (head✝ :: tail✝)[k] = simplicialEvalσ (head✝ :: tail✝) ((head✝ :: tail✝)[k] + 1)

Tactic:
<;>

Goal state after:
case nil
m : ℕ
hL : IsAdmissible m []
k : ℕ
hk : k < [].length
⊢ simplicialEvalσ [] [][k] = simplicialEvalσ [] ([][k] + 1)

case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ :
  ∀ {m : ℕ},
    IsAdmissible m tail✝ →
      ∀ {k : ℕ} {hk : k < tail✝.length}, simplicialEvalσ tail✝ tail✝[k] = simplicialEvalσ tail✝ (tail✝[k] + 1)
m : ℕ
hL : IsAdmissible m (head✝ :: tail✝)
k : ℕ
hk : k < (head✝ :: tail✝).length
⊢ simplicialEvalσ (head✝ :: tail✝) (head✝ :: tail✝)[k] = simplicialEvalσ (head✝ :: tail✝) ((head✝ :: tail✝)[k] + 1)