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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
⊢ stdSimplex.objEquiv.symm f ∉ Λ[n, i].obj (op d)

Tactic:
mem_horn_iff,

Goal state after:
n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
⊢ ¬Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm f)) ∪ {i} ≠ Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
⊢ stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∈ Λ[n + 1, j].obj (op ⦋n⦌) ↔ i ≠ j

Tactic:
dsimp

Goal state after:
n : ℕ
i j : Fin (n + 2)
⊢ stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∈ Λ[n + 1, j].obj (op ⦋n⦌) ↔ ¬i = j
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst✝ : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ c.multispanIndex.left (i, j) = c.multispanIndex.left (j, i)

Tactic:
dsimp

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst✝ : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
⊢ V i j = V j i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case refine_2.inl
i : Fin (2 + 1)
j : Fin 2
h₀ : 0 < ↑i
hₙ : ↑i < 2
⊢ #{i, j.castSucc, j.succ} ≤ 2

Tactic:
revert i j

Goal state after:
case refine_2.inl
⊢ ∀ {i : Fin (2 + 1)} (j : Fin 2), 0 < ↑i → ↑i < 2 → #{i, j.castSucc, j.succ} ≤ 2
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.«_@»._internal._hyg.0.«1»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}

Tactic:
exact le_sup_left

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

Goal state before:
pp: case a.«_@»._internal._hyg.0.«1»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}

Tactic:
exact le_sup_left

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

Goal state before:
pp: case a.«_@»._internal._hyg.0.«1»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
exact le_sup_left

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ⨆ i_1, stdSimplex.face {↑i_1}ᶜ = Λ[n, i]

Tactic:
horn_eq_iSup

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ ⨆ i_1, stdSimplex.face {↑i_1}ᶜ = ⨆ j, stdSimplex.face {↑j}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
⊢ (fun n ↦ Subcomplex.range i ⊔ Y.skeleton n) n ≤ (fun n ↦ Subcomplex.range i ⊔ Y.skeleton n) m

Tactic:
dsimp

Goal state after:
X Y : SSet
i : X ⟶ Y
n m : ℕ
h : n ≤ m
⊢ Subcomplex.range i ⊔ Y.skeleton n ≤ Subcomplex.range i ⊔ Y.skeleton m
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ (skeletonOfMono i) (n + 1) =
    (skeletonOfMono i) n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
dsimp only [skeletonOfMono, OrderHom.coe_mk]
  apply le_antisymm
  · simp only [sup_le_iff, iSup_le_iff, skeleton_succ]
    refine ⟨le_sup_left.trans le_sup_left,
      le_sup_right.trans le_sup_left, fun x ↦ ?_⟩
    by_cases hx : x.1 ∈ (Subcomplex.range i).obj _
    · exact le_trans (le_trans (by simpa) le_sup_left) le_sup_left
    · exact (le_trans (by exact le_trans (by rfl) (le_iSup _ hx))
        (le_iSup _ x)).trans le_sup_right
  · simp only [sup_le_iff, iSup_le_iff]
    exact ⟨⟨le_sup_left, (Y.skeleton.monotone (by simp)).trans le_sup_right⟩,
      fun _ _ ↦ (Y.ofSimplex_le_skeleton _ (by simp)).trans le_sup_right⟩

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

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha✝ : a ∈ {i}ᶜ
b : Fin (n + 1 + 1 + 1)
hb✝ : b ∈ {i}ᶜ
hab : a < b
ha : ¬a = i
hb : ¬b = i
⊢ (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst
        ⟨(⟨a, ha✝⟩, ⟨b, hb✝⟩), hab⟩ ≫
      match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst ⟨(⟨a, ha✝⟩, ⟨b, hb✝⟩), hab⟩ with
      | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd
        ⟨(⟨a, ha✝⟩, ⟨b, hb✝⟩), hab⟩ ≫
      match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd ⟨(⟨a, ha✝⟩, ⟨b, hb✝⟩), hab⟩ with
      | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

Tactic:
dsimp

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha✝ : a ∈ {i}ᶜ
b : Fin (n + 1 + 1 + 1)
hb✝ : b ∈ {i}ᶜ
hab : a < b
ha : ¬a = i
hb : ¬b = i
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso a).inv ≫ f a ha✝ =
    Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso b).inv ≫ f b hb✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsPullback (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (t i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d)) (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (r i d))
    (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))

Tactic:
dsimp

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ IsPullback ((t i d).app (op ⦋n⦌)) ((l i d).app (op ⦋n⦌)) (↾fun x ↦ ⟨↑x, ⋯⟩) ((b i d).app (op ⦋n⦌))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩) =
    ⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)), hx⟩

Tactic:
rw [Subtype.ext_iff]

Goal state after:
case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩)) =
    ↑⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)), hx⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ (ConcreteCategory.hom ((b i d).app (op n)))
      ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f.unop)) =
    ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩

Tactic:
rw [Subtype.ext_iff]

Goal state after:
case inr
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
y : Y _⦋d⦌
hy₁ : y ∈ Y.nonDegenerate d
hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (i.app (op ⦋d⦌))) x = y
f : op ⦋d⦌ ⟶ op n
hx : (ConcreteCategory.hom (Y.map f)) y ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩ ∈ ⊤.obj (op n)
c : Cell i d := { simplex := y, nonDegenerate := hy₁, notMem := ⋯ }
⊢ ↑((ConcreteCategory.hom ((b i d).app (op n)))
        ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f.unop))) =
    ↑⟨(ConcreteCategory.hom (Y.map f)) y, hx⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «1»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
dsimp

Goal state after:
case «1»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀ =
    Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
y : sigmaStdSimplex i d _⦋n⦌
hy : y ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
⊢ ∃ c f, ∃ (_ : Epi f), (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f) = y

Tactic:
by
  obtain ⟨c, s, rfl⟩ := ιSigmaStdSimplex_jointly_surjective y
  have hs : s ∉ ∂Δ[d].obj _ :=
    fun hs ↦ hy (⟨c.ιSigmaBoundary.app _ ⟨s, hs⟩, congr($(c.ι_l).app _ ⟨s, _⟩)⟩)
  refine ⟨c, stdSimplex.objEquiv s, ?_, by simp⟩
  simpa [SimplexCategory.epi_iff_surjective, boundary] using! hs

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

Goal state before:
pp: case «2»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
dsimp

Goal state after:
case «2»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂ =
    Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ∀ (x₃ y₃ : evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d)),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
        (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) x₃ =
            (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) y₃ →
          x₃ = y₃

Tactic:
dsimp

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ∀ (x₃ y₃ : sigmaStdSimplex i d _⦋n⦌),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
        (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₃ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y₃ → x₃ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «0»
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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ 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₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ 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:
dsimp

Goal state after:
case «0»
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₁
⊢ Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀ =
    Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ 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₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ 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:
dsimp

Goal state after:
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₁
⊢ Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀ =
    Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inl
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
hlt : ksucc < j
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌))) ((horn.spineId i h₀ hₙ).arrow k.castSucc) =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
dsimp

Goal state after:
case h.inl
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
hlt : ksucc < j
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌))) ((horn.spineId i h₀ hₙ).arrow k.castSucc) =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ 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₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ 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:
dsimp

Goal state after:
case «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₁
⊢ Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁ =
    Subcomplex.homOfLE ⋯ ≫ (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
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
hgt : j < ksucc
⊢ ((horn.spineId i h₀ hₙ).map σ₀).arrow k.succ =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
dsimp

Goal state after:
case h.inr.inl
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
hgt : j < ksucc
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌))) ((horn.spineId i h₀ hₙ).arrow k.succ) =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

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

Tactic:
dsimp

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i).op)) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) =
    ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
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
    apply Functor.ext
    · rintro ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟨⟩⟩⟩⟩
      simp only [eqToHom_refl, Category.comp_id, Category.id_comp]
      exact (Functor.map_id _ _).symm
    · intro; rfl

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

Goal state after:
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✝ ≍ Prod.mkHom (x✝⁴.fst.toFunctor.map x✝) (x✝⁴.snd.toFunctor.map x✝)
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
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ (ConcreteCategory.hom
          (((↾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)).toFun
      ((f, g), h) =
    (ConcreteCategory.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))).toFun
      ((f, g), h)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
⊢ ((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g) ⊗ₘ h)) ≫ (α_ X Y Z).hom =
    (λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (g ⊗ₘ h))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case succ.refine_2.inl
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯)).arrow 0 = p.arrow 0

Tactic:
dsimp

Goal state after:
case succ.refine_2.inl
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op)) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯) = p.arrow 0
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ
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)
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ((ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (diag 2).op)) triangle) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
dsimp

Goal state after:
case h.inr.inr.succ
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)
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (diag 2).op)) ↑triangle, ⋯⟩ =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩
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
X Y : TransportEnrichment F C
⊢ (λ_ (F.obj (X ⟶[V] Y))).inv ≫
      (ε F ≫ F.map (eId V X)) ▷ F.obj (X ⟶[V] Y) ≫ μ F (X ⟶[V] X) (X ⟶[V] Y) ≫ F.map (eComp V X X Y) =
    𝟙 (F.obj (X ⟶[V] Y))

Tactic:
by
    simp only [comp_whiskerRight, Category.assoc, Functor.LaxMonoidal.μ_natural_left_assoc,
      Functor.LaxMonoidal.left_unitality_inv_assoc]
    simp_rw [← F.map_comp]
    convert! F.map_id _
    simp

Goal state after: