mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
⊢ x₁ ∈ c.multispanIndex.left (i₁, i₂)

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ stdSimplex.objMk OrderHom.id ∈ ⊤.obj (op ⦋n⦌)

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ S = Finset.univ

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
hd : n < d
hS : Finset.univ.card = d + 1
hx : stdSimplex.face Finset.univ ≤ A
⊢ stdSimplex.face {i}ᶜ ≤ stdSimplex.face Finset.univ

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : S.card = n + 1
⊢ Sᶜ.card = 1

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
hf : Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom f)
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hS : Sᶜ = {j}
⊢ S = {j}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : Sᶜ.card = 1
⊢ ∃ j, S = {j}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
hd : n ≤ n
j : Fin (n + 1 + 1)
hx : stdSimplex.face {j}ᶜ ≤ A
hS : {j}ᶜᶜ.card = 1
⊢ j ≠ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
i₁ i₂ : ι
x✝¹ : (c.multispanIndex.map Set.functorToTypes).right i₁
x✝ : (c.multispanIndex.map Set.functorToTypes).right i₂
x₁ : X
h₁ : x₁ ∈ U i₁
h₂ : x₁ ∈ U i₂
h :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₁) ⟨x₁, h₁⟩ =
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
      (WalkingMultispan.right i₂) ⟨x₁, h₂⟩
eq₁ :
  e.ιColimitType (WalkingMultispan.right ((MultispanShape.prod ι).fst (i₁, i₂)))
      ((ConcreteCategory.hom (e.map (WalkingMultispan.Hom.fst (i₁, i₂)))) ⟨x₁, ⋯⟩) =
    e.ιColimitType (WalkingMultispan.left (i₁, i₂)) ⟨x₁, ⋯⟩
⊢ x₁ ∈ c.multispanIndex.left (i₁, i₂)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : m < n
⊢ ∂Δ[n].obj (op ⦋m⦌) = Set.univ

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
⊢ A ≤ Λ[n + 1, i] ↔ ¬stdSimplex.face {i}ᶜ ≤ A

Tactic:
by

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

Goal state before:
pp: m : SimplexCategoryᵒᵖ
x✝ : Δ[0].obj m
x : Fin 1
⊢ (stdSimplex.asOrderHom x✝) 0 = x

Tactic:
by

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

Goal state before:
pp: ⊢ ∂Δ[0] = ⊥

Tactic:
by

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

Goal state before:
pp: n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k
l : Fin (d + 1)
x✝ : j l = k.rev
⊢ (j l.rev.rev).rev = k

Tactic:
by

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

Goal state before:
pp: n d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
hk : ∀ (x : Fin (d + 1)), ¬j x = k
l : Fin (d + 1)
x✝ : (j l.rev).rev = k.rev
⊢ j l.rev = k

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ S = Finset.univ ∨ S = {j}ᶜ → {j}ᶜ ⊆ S

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].op.preimage (stdSimplex.opIso ⦋n⦌).inv = ∂Δ[n]

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ stdSimplex.face S ≤ Λ[n + 1, j] ↔ S ≠ Finset.univ ∧ S ≠ {j}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
i✝ : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
i : Fin (n + 1)
⊢ (stdSimplex.asOrderHom (stdSimplex.objEquiv.symm f)) ((ConcreteCategory.hom (inv f)) i) = i

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha : objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ A.obj (op ⦋n⦌)
⊢ A ≤ ⊤

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha : objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ A.obj (op ⦋n⦌)
⊢ ⊤ ≤ A

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
i : ℕ
hi : n ≤ i
⊢ A.toSSet.degenerate i = ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i
h₂ : ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k
⊢ ¬k.rev = i.rev

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
⊢ IsColimit (c.multicofork.map Set.functorToTypes)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i
h₂ : ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k
l : Fin (d + 1)
hl : j l = k.rev
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : ℕ
j : Δ[n] _⦋d⦌
k : Fin (n + 1)
h₁ : ¬k = i.rev
h₂ : ∀ (x : Fin (d + 1)), ¬j x = k
⊢ ¬k.rev = i ∧ ∀ (x : Fin (d + 1)), ¬(j x.rev).rev = k.rev

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i].op.preimage (stdSimplex.opIso ⦋n⦌).inv = Λ[n, i.rev]

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} = Set.univ

Tactic:
by

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

Goal state before:
pp: n : ℕ
i k : Fin (n + 3)
m : SimplexCategoryᵒᵖ
⊢ stdSimplex.obj₀Equiv.symm k ∈ Λ[n + 2, i].obj (op ⦋0⦌)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ (MultispanShape.ofLinearOrder Bool).fst default ≠ (MultispanShape.ofLinearOrder Bool).snd default

Tactic:
by

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

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
hS : {i, a, b} = univ
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
⊢ A ≤ ∂Δ[n] ↔ A ≠ ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n] ≤ ∂Δ[n]

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
i j : J
x : X
hx : x ∈ F.obj i
y : X
hy : y ∈ F.obj j
h :
  (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) ⟨x, hx⟩ =
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) ⟨y, hy⟩
⊢ x = y

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h₁ : ∂Δ[n] ≤ A
h₂ : A ≠ ⊤
⊢ A ≤ ∂Δ[n]

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
⊢ PreservesColimit F functorToTypes

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
⊢ A = ∂Δ[n] ↔ ∂Δ[n] ≤ A ∧ A ≠ ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Mono (faceι i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ faceι i ≫ ∂Δ[n + 1].ι = (stdSimplex.face {i}ᶜ).ι

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.range (stdSimplex.map (SimplexCategory.δ i)) ≤ ∂Δ[n + 1]

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
X : SSet
inst✝ : IsFilteredOrEmpty J
F : J ⥤ X.Subcomplex
j : SimplexCategoryᵒᵖ
⊢ (Preorder.colimitCoconeOfIsLUB (F ⋙ evaluation X j) ⋯).cocone.pt = (Preorder.colimitCoconeOfIsLUB F ⋯).cocone.pt.obj j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasIterationOfShape K C
⊢ (W.functorCategory J).transfiniteCompositionsOfShape K ≤ W.functorCategory J

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u''
inst✝ : Category.{v'', u''} J
⊢ (isomorphisms C).functorCategory J = isomorphisms (J ⥤ C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasPullbacks C
⊢ (monomorphisms C).functorCategory J = monomorphisms (J ⥤ C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasPushouts C
⊢ (epimorphisms C).functorCategory J = epimorphisms (J ⥤ C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝⁷ : Category.{v'', u''} J
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : (monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K
inst✝¹ : HasPullbacks C
inst✝ : HasIterationOfShape K C
⊢ (monomorphisms (J ⥤ C)).IsStableUnderTransfiniteCompositionOfShape K

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (stdSimplex.faceSingletonComplIso i).inv ≫ ι i = faceι i

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (ι i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝³ : Category.{v'', u''} J
K' : Type u'
inst✝² : (monomorphisms C).IsStableUnderCoproductsOfShape K'
inst✝¹ : HasCoproductsOfShape K' C
inst✝ : HasPullbacks C
⊢ (monomorphisms (J ⥤ C)).IsStableUnderCoproductsOfShape K'

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (stdSimplex.δ i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
h₀ : 0 < ↑i
hₙ : ↑i < n
⊢ n = 2 ∨ 2 < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h₀ : 0 < i
hₙ : i < Fin.last n
j : Fin n
⊢ Λ[n, i].toSSet _⦋1⦌

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k < n + 3 + 1

Tactic:
by

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

Goal state before:
pp: X : SSet
f g : ∂Δ[0].toSSet ⟶ X
⊢ f = g

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 1 < n + 3 + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 2 < n + 3 + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k < n + 4

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 1 < n + 4

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ k + 2 < n + 4

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
hS : {i, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
⊢ False

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 4)
h₀ : 0 < i
hₙ : i < Fin.last (n + 3)
k : ℕ
h : k < n + 2
⊢ Λ[n + 3, i].toSSet _⦋2⦌

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : j ≠ i
⊢ Subfunctor.range (stdSimplex.δ j) ≤ Λ[n + 1, i]

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
j : Fin (n + 1 + 1)
hj : ¬j = i
⊢ (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j hj) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j hj)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ σ₁ = σ₂

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hij : j ≠ i
⊢ faceι i j hij ≫ Λ[n, i].ι = (stdSimplex.face {j}ᶜ).ι

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ yonedaEquiv (ι i j hij) = face i j hij

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hij = faceι i j hij

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₃ ⟶ X₄
b : X₂ ⟶ X₄
sq : IsPushout l t r b
ht : monomorphisms (Type u) t
⊢ monomorphisms (Type u) r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ f ≫ inl f g = g ≫ inr f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
⊢ ∀ (a b : X₁ ⊕ X₂),
    Rel f g a b →
      (match a with
        | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
        | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂) =
        match b with
        | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
        | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
⊢ m =
    ↾Quot.lift
        (fun x ↦
          match x with
          | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
          | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂)
        ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔
    x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ y₁ : c₁.pt
h : (hom φ) x₁ = (hom φ) y₁
⊢ ∃ j x₁' y₁', x₁ = (hom (c₁.ι.app j)) x₁' ∧ y₁ = (hom (c₁.ι.app j)) y₁'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x y : X₁ ⊕ X₂
h : Rel' f g x y
⊢ Rel' f g y x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
hf : (monomorphisms (Type u)).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ monomorphisms (Type u) φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂)
⊢ (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
⊢ ∀ (X₁ X₂ : T → Type u) [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : T) → X₁ j ⟶ X₂ j),
    (∀ (j : T), monomorphisms (Type u) (f j)) → monomorphisms (Type u) (Limits.Sigma.map f)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ I ∂Δ[n].ι

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ J Λ[n, i].ι

Tactic:
by

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

Goal state before:
pp: ⊢ I ≤ monomorphisms SSet

Tactic:
by

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

Goal state before:
pp: ⊢ J ≤ monomorphisms SSet

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Cofibration f ↔ Mono f

Tactic:
by

Goal state after: