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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w✝¹ : Epi f₁
hx₁ :
  (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w✝ : Epi f₂
hx₂ :
  (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂) ∉
    Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
h : (ConcreteCategory.hom (Y.map f₁.op)) c₁.simplex = (ConcreteCategory.hom (Y.map f₂.op)) c₂.simplex
⊢ c₁ = c₂

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
f : X.Path m
j l : ℕ
h : j + l ≤ m
i : Fin (l + 1)
⊢ j + ↑i < m + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
f : X.Path m
j l : ℕ
h : j + l ≤ m
i : Fin l
⊢ j + ↑i < m

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    sx.spineToSimplex l ⋯ (f.interval j l hjl)

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ l ≤ n + 1

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ 2 < 3

Tactic:
by

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ }))) (f.vertex i.castSucc)

Tactic:
by

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsColimit (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.mapCocone (PushoutCocone.mk (r i d) (b i d) ⋯))

Tactic:
by

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
inst✝ : Mono i
⊢ ⋯.functor.obj ⊥ = Subcomplex.range i

Tactic:
by

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
s : X.N
⊢ ¬IsMax s.dim

Tactic:
by

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
s : X.N
⊢ s.simplex ∉ Set.range ⇑(ConcreteCategory.hom (⊥.ι.app (op ⦋s.dim⦌)))

Tactic:
by

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ }))) (f.vertex i.succ)

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i.castSucc) ⋯ h).op)) Δ

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
⊢ ksucc < j ∨ j < ksucc ∨ j = ksucc

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    sx.spineToDiagonal l ⋯ (f.interval j l hjl)

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i.succ) ⋯ h).op)) Δ

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ 1 < 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
⊢ sy.spineToSimplex (m + 1) ⋯ (f.map σ) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f)

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (X.spine a hₐ ((ConcreteCategory.hom (X.map φ.op)) Δ)).vertex i = (X.spine m hₘ Δ).vertex ((Hom.toOrderHom φ.hom) i)

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ 0 < 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).vertex
      i =
    f.vertex i.castSucc

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
⊢ l ≤ n + 1

Tactic:
by

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

Goal state before:
pp: 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₁
x : (MultispanShape.ofLinearOrder ↑{2}ᶜ).L
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst x ≫
      match (MultispanShape.ofLinearOrder ↑{2}ᶜ).fst x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
        | 2, hi => ⋯.elim
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd x ≫
      match (MultispanShape.ofLinearOrder ↑{2}ᶜ).snd x with
      | ⟨i, hi⟩ =>
        match i, hi with
        | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
        | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
        | 2, hi => ⋯.elim
        | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (X.spine m ⋯
          ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).vertex
      i =
    f.vertex i.succ

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ 0 ∈ {2}ᶜ

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ 1 ∈ {2}ᶜ

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ 3 ∈ {2}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (X.spine m ⋯ ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.castSucc

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ ι₀ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₀

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (X.spine m ⋯ ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    f.arrow i.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
sx✝ : X✝.StrictSegal
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ 2 ≤ n + 1 + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
sx✝ : X✝.StrictSegal
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ ↑i + 2 ≤ m + 1

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (X.spine m ⋯ ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      i =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
⊢ X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ) = (X.spine m hₘ Δ).interval j l h

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ i).op)) (sx.spineToSimplex f) = f.vertex i

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin (n + 1)
⊢ f.vertex i = g.vertex i

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin n
⊢ f.arrow i = g.arrow i

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) (sx.spineToSimplex f) = f.arrow i

Tactic:
by

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

Goal state before:
pp: X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
⊢ f = g

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
i : Fin (0 + 3)
σ₀ : Λ[0 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (0 + 2)
j : Fin (0 + 3)
hj : j ≠ i
k : Fin (0 + 1)
ksucc : Fin (0 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ k = 0

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f) = sx.spineToSimplex (f.interval j l hjl)

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
f : X.Path n
j l : ℕ
k' : Fin l
k : Fin n
h : j + l ≤ n
hkk' : j + ↑k' = ↑k
⊢ (f.interval j l h).arrow k' = f.arrow k

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    sx.spineToDiagonal (f.interval j l hjl)

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ ι₃ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₃

Tactic:
by

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

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ 0 < i.succ.castSucc

Tactic:
by

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

Goal state before:
pp: 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₁
⊢ ι₀ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₀ ∧ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁ ∧ ι₃ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₃

Tactic:
by

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

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ 1 + ↑i = ↑i.succ

Tactic:
by

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

Goal state before:
pp: X : SSet
m : ℕ
x : X _⦋m + 1⦌
⊢ X.spine m ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1) x).interval 1 m ⋯

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
Δ : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ n ≤ max m n + 1

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
Δ : X _⦋n⦌
m : ℕ
φ : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ m ≤ max m n + 1

Tactic:
by

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

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ sy.spineToSimplex (f.map σ) = (ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f)

Tactic:
by

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

Goal state before:
pp: 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
⊢ ↑k < n + 2

Tactic:
by

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

Goal state before:
pp: X : SSet
n j l : ℕ
h : j + l ≤ n
Δ : X _⦋n⦌
⊢ n ≤ n + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∀ (j : Fin (n + 2 + 1)), (stdSimplex.spineId (n + 2)).vertex j ∈ Λ[n + 2, i].obj (op ⦋0⦌)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ (Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝² : BinaryFan X Y
x✝¹ : x✝².pt ⟶ of (↑X × ↑Y)
h1 : x✝¹ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝².fst
h2 : x✝¹ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝².snd
x✝ : ↑x✝².pt
⊢ (x✝¹.toFunctor.obj x✝).1 = ((x✝².fst.toFunctor.prod' x✝².snd.toFunctor).toCatHom.toFunctor.obj x✝).1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝² : BinaryFan X Y
x✝¹ : x✝².pt ⟶ of (↑X × ↑Y)
h1 : x✝¹ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝².fst
h2 : x✝¹ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝².snd
x✝ : ↑x✝².pt
⊢ (x✝¹.toFunctor.obj x✝).2 = ((x✝².fst.toFunctor.prod' x✝².snd.toFunctor).toCatHom.toFunctor.obj x✝).2

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ (stdSimplex.spineId (n + 2)).arrow j ∈ Λ[n + 2, i].obj (op ⦋1⦌)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: 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 ⋯
⊢ ↑k + 2 ≤ n + 1 + 2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: X Y : Cat
x✝⁴ : BinaryFan X Y
x✝³ : x✝⁴.pt ⟶ of (↑X × ↑Y)
h1 : x✝³ ≫ (Prod.fst ↑X ↑Y).toCatHom = x✝⁴.fst
h2 : x✝³ ≫ (Prod.snd ↑X ↑Y).toCatHom = x✝⁴.snd
x✝² x✝¹ : ↑x✝⁴.pt
x✝ : x✝² ⟶ x✝¹
⊢ x✝³.toFunctor.map x✝ ≍ (x✝⁴.fst.toFunctor.prod' x✝⁴.snd.toFunctor).toCatHom.toFunctor.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
⊢ ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
    (((coyoneda.obj (op (𝟙_ C))).map f ⊗ₘ (coyoneda.obj (op (𝟙_ C))).map g) ≫ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) =
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (f ⊗ₘ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: ⊢ MonoidalCategory Cat

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: ⊢ SymmetricCategory Cat

Tactic:
by

Goal state after:
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 : j ≤ i.castSucc
⊢ (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex f))).vertex i = f.vertex i.succ

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ ((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom =
    (α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y) ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
      (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
        ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)

Tactic:
ext ⟨⟨f, g⟩, h⟩; dsimp at f g h
      dsimp; simp only [Category.assoc, Iso.cancel_iso_inv_left]
      conv_lhs =>
        rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality,
          ← Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]
      conv_rhs => rw [← Category.id_comp f, ← tensorHom_comp_tensorHom]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ ((↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ⊗ₘ 𝟙 ((coyoneda.obj (op (𝟙_ C))).obj Z)) ≫
      (↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫ (coyoneda.obj (op (𝟙_ C))).map (α_ X Y Z).hom =
    (α_ ((coyoneda.obj (op (𝟙_ C))).obj X) ((coyoneda.obj (op (𝟙_ C))).obj Y) ((coyoneda.obj (op (𝟙_ C))).obj Z)).hom ≫
      (𝟙 ((coyoneda.obj (op (𝟙_ C))).obj X) ⊗ₘ ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)) ≫
        ↾fun p ↦ (λ_ (𝟙_ C)).inv ≫ (p.1 ⊗ₘ p.2)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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)
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑i + 2 ≤ n + 1

Tactic:
by

Goal state after: