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

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

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

Tactic:
·

Goal state after:
case a.«_@»._internal._hyg.0.«0»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case neg
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
h₂ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

Tactic:
·

Goal state after:
case neg
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
h₂ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
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:
·

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

Goal state before:
pp: case zero
i : Fin (0 + 1)
h0 : 0 < i
hn : i < Fin.last 0
⊢ innerHornInclusions Λ[0, i].ι

pp: case succ.zero
i : Fin (0 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (0 + 1)
⊢ innerHornInclusions Λ[0 + 1, i].ι

pp: case succ.succ
k : ℕ
i : Fin (k + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (k + 1 + 1)
⊢ innerHornInclusions Λ[k + 1 + 1, i].ι

Tactic:
·

Goal state after:
case zero
i : Fin (0 + 1)
h0 : 0 < i
hn : i < Fin.last 0
⊢ innerHornInclusions Λ[0, i].ι
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case succ.zero
i : Fin (0 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (0 + 1)
⊢ innerHornInclusions Λ[0 + 1, i].ι

pp: case succ.succ
k : ℕ
i : Fin (k + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (k + 1 + 1)
⊢ innerHornInclusions Λ[k + 1 + 1, i].ι

Tactic:
·

Goal state after:
case succ.zero
i : Fin (0 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (0 + 1)
⊢ innerHornInclusions Λ[0 + 1, i].ι
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case succ.succ
k : ℕ
i : Fin (k + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (k + 1 + 1)
⊢ innerHornInclusions Λ[k + 1 + 1, i].ι

Tactic:
·

Goal state after:
case succ.succ
k : ℕ
i : Fin (k + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (k + 1 + 1)
⊢ innerHornInclusions Λ[k + 1 + 1, i].ι
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case refine_1
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : innerHornInclusions f✝
⊢ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝

pp: case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
⊢ innerHornInclusions f✝

Tactic:
·

Goal state after:
case refine_1
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : innerHornInclusions f✝
⊢ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
⊢ innerHornInclusions f✝

Tactic:
·

Goal state after:
case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
⊢ innerHornInclusions f✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 1]

pp: case a
⊢ Λ[2, 1] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}

Tactic:
·

Goal state after:
case a
⊢ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 1]
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.left
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1]

pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
·

Goal state after:
case a.left
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 1]
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
·

Goal state after:
case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 1]
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i j : ℕ
h : i ≤ j
k : Fin i
x : ↑(X.nonDegenerate ↑k)
⊢ ↑k < j

Tactic:
by lia

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

Goal state before:
pp: case a
⊢ Λ[2, 1] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}

Tactic:
·

Goal state after:
case a
⊢ Λ[2, 1] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

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

Tactic:
·

Goal state after:
case a.«_@»._internal._hyg.0.«0»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 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 {1, 2}

Tactic:
·

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
a✝ : ↑x ∈ ⊤.obj (op ⦋n⦌)
⊢ n < n + 1

Tactic:
by lia

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

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ X.skeleton (n + 1) ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

pp: case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)

Tactic:
·

Goal state after:
case a
X : SSet
n : ℕ
⊢ X.skeleton (n + 1) ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 2]

pp: case a
⊢ Λ[2, 2] ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
·

Goal state after:
case a
⊢ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2} ≤ Λ[2, 2]
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr.inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) y₂)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom r) y₂

pp: case inr.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃

Tactic:
·

Goal state after:
case inr.inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₂ : X₂
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom r) y₂)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom r) y₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.left
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 2]

pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 2]

Tactic:
·

Goal state after:
case a.left
⊢ stdSimplex.face {0, 2} ≤ Λ[2, 2]
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 2]

Tactic:
·

Goal state after:
case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 2]
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ Λ[2, 2] ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
·

Goal state after:
case a
⊢ Λ[2, 2] ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.inl
X : SSet
n d : ℕ
hd✝¹ : d < n + 1
hd✝ : d ≤ n
x : ↑(X.nonDegenerate ↑⟨d, hd✝¹⟩)
hd : d < n
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

pp: case a.inr
X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton d ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
·

Goal state after:
case a.inl
X : SSet
n d : ℕ
hd✝¹ : d < n + 1
hd✝ : d ≤ n
x : ↑(X.nonDegenerate ↑⟨d, hd✝¹⟩)
hd : d < n
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃

Tactic:
·

Goal state after:
case inr.inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₃
hx₃ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
y₃ : X₃
hy₃ : y₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq : (ConcreteCategory.hom k) ((ConcreteCategory.hom b) x₃) = (ConcreteCategory.hom k) ((ConcreteCategory.hom b) y₃)
⊢ (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom b) y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.inr
X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton d ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
·

Goal state after:
case a.inr
X : SSet
d : ℕ
hd✝ : d < d + 1
hd : d ≤ d
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton d ⊔ ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

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

Tactic:
·

Goal state after:
case a.«_@»._internal._hyg.0.«0»
⊢ stdSimplex.face {↑⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}
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:
·

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

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)

Tactic:
·

Goal state after:
case a
X : SSet
n : ℕ
⊢ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.left
X : SSet
n : ℕ
⊢ X.skeleton n ≤ X.skeleton (n + 1)

pp: case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)

Tactic:
·

Goal state after:
case a.left
X : SSet
n : ℕ
⊢ X.skeleton n ≤ X.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)

Tactic:
·

Goal state after:
case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case zero
X : SSet
i : Fin (0 + 2)
g : Λ[0 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

Tactic:
·

Goal state after:
case zero
X : SSet
i : Fin (0 + 2)
g : Λ[0 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g

Tactic:
·

Goal state after:
case succ
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
⊢ horn.IsCompatible fun j hj ↦ ι i j hj ≫ g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

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

pp: case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton (n + 1)

Tactic:
·

Goal state after:
case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton (n + 1) ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₂ : X₂
⊢ ∃ a, (ConcreteCategory.hom φ) a = (ConcreteCategory.hom r) x₂

pp: case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₃ : X₃
⊢ ∃ a, (ConcreteCategory.hom φ) a = (ConcreteCategory.hom b) x₃

Tactic:
·

Goal state after:
case inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₂ : X₂
⊢ ∃ a, (ConcreteCategory.hom φ) a = (ConcreteCategory.hom r) x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case pos
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∈ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

pp: case neg
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
·

Goal state after:
case pos
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∈ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₃ : X₃
⊢ ∃ a, (ConcreteCategory.hom φ) a = (ConcreteCategory.hom b) x₃

Tactic:
·

Goal state after:
case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₃ : X₃
⊢ ∃ a, (ConcreteCategory.hom φ) a = (ConcreteCategory.hom b) x₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case neg
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x

Tactic:
·

Goal state after:
case neg
X Y : SSet
i : X ⟶ Y
n : ℕ
x : ↑(Y.nonDegenerate n)
hx : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)
⊢ Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₃ : X₃
⊢ ∃ a, (ConcreteCategory.hom φ) a = (ConcreteCategory.hom b) x₃

Tactic:
· exact ⟨_, ConcreteCategory.congr_hom hφ₂ x₃⟩

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

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

Tactic:
·

Goal state after:
case a
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Subcomplex.range i ⊔ Y.skeleton n ⊔ ⨆ x, ⨆ (_ : ↑x ∉ (Subcomplex.range i).obj (op ⦋n⦌)), Subcomplex.ofSimplex ↑x ≤
    Subcomplex.range i ⊔ Y.skeleton (n + 1)