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

Goal state before:
pp: case inl.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₁
hy₃ : (ConcreteCategory.hom l) x₁ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq :
  (ConcreteCategory.hom k) ((ConcreteCategory.hom r) ((ConcreteCategory.hom t) x₁)) =
    (ConcreteCategory.hom k) ((ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁))
⊢ (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁)

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case a
X : SSet
n d : ℕ
hd✝ : d < n + 1
hd : d ≤ n
x : ↑(X.nonDegenerate ↑⟨d, hd✝⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x
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₃ : (ConcreteCategory.hom l) x₁ ∉ Set.range ⇑(ConcreteCategory.hom l)
eq :
  (ConcreteCategory.hom k) ((ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁)) =
    (ConcreteCategory.hom k) ((ConcreteCategory.hom r) ((ConcreteCategory.hom t) x₁))
⊢ (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x₁)

Tactic:
]

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

Goal state before:
pp: case a
⊢ ∀ (i : ↑{2}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
]

Goal state after:
case a
⊢ ∀ (i : ↑{2}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ stdSimplex.face {↑j, ↑k}ᶜ = stdSimplex.face ({↑j}ᶜ ⊓ {↑k}ᶜ)

Tactic:
]

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ ∀ (i_1 : ℕ), Y.skeleton i_1 ≤ ⨆ n, (skeletonOfMono i) n

Tactic:
]

Goal state after:
X Y : SSet
i : X ⟶ Y
⊢ ∀ (i_1 : ℕ), Y.skeleton i_1 ≤ ⨆ n, (skeletonOfMono i) n
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: 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)
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)

Tactic:
]

Goal state after:
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)
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ (Y.skeleton n).obj (op ⦋d⦌) ⊆ ((skeletonOfMono i) n).obj (op ⦋d⦌)

Tactic:
]

Goal state after:
X Y : SSet
i : X ⟶ Y
d n : ℕ
h : d < n
⊢ (Y.skeleton n).obj (op ⦋d⦌) ⊆ ((skeletonOfMono i) n).obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ k ≫ stdSimplex.δ j.castSucc

Tactic:
]

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∂Δ[d] ≤ ((skeletonOfMono i) d).preimage c.map ∧ ((skeletonOfMono i) d).preimage c.map ≠ ⊤

Tactic:
]

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∂Δ[d] ≤ ((skeletonOfMono i) d).preimage c.map ∧ ((skeletonOfMono i) d).preimage c.map ≠ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∀ (n : ℕ) (x : ↑(Δ[d].nonDegenerate n)),
    ↑x ∈ ∂Δ[d].obj (op ⦋n⦌) → ↑x ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋n⦌)

Tactic:
]

Goal state after:
case refine_1
X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
⊢ ∀ (n : ℕ) (x : ↑(Δ[d].nonDegenerate n)),
    ↑x ∈ ∂Δ[d].obj (op ⦋n⦌) → ↑x ∈ (((skeletonOfMono i) d).preimage c.map).obj (op ⦋n⦌)
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
⊢ (facePairComplIso a b hab).inv ≫ stdSimplex.δ (a.castPred ⋯) ≫ f b ⋯ =
    (facePairComplIso a b hab).inv ≫ stdSimplex.δ (a.castPred ⋯) ≫ f b hb✝

Tactic:
]

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

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ((t i d).app (op ⦋n⦌) ≫ ↾fun x ↦ ⟨↑x, ⋯⟩) = (l i d).app (op ⦋n⦌) ≫ (b i d).app (op ⦋n⦌) ∧
    (∀ (x₁ y₁ : (fun X ↦ X) (sigmaBoundary i d _⦋n⦌)),
        (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) y₁ ∧
            (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))) (x₃ : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)),
        (ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) x₂ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₃ →
          ∃ x₁,
            (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = x₂ ∧
              (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = x₃

Tactic:
]

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ((t i d).app (op ⦋n⦌) ≫ ↾fun x ↦ ⟨↑x, ⋯⟩) = (l i d).app (op ⦋n⦌) ≫ (b i d).app (op ⦋n⦌) ∧
    (∀ (x₁ y₁ : (fun X ↦ X) (sigmaBoundary i d _⦋n⦌)),
        (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) y₁ ∧
            (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))) (x₃ : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)),
        (ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) x₂ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₃ →
          ∃ x₁,
            (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = x₂ ∧
              (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = x₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
y : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : x ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
h : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) ⟨x, hx⟩) = ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y)
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = ⟨x, hx⟩ ∧ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = y

Tactic:
]

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
y : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : x ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
h : ↑((ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) ⟨x, hx⟩) = ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y)
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = ⟨x, hx⟩ ∧ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
    (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj

Tactic:
]

Goal state after:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
j : Fin (n + 2)
hj : j ≠ i
⊢ (stdSimplex.faceSingletonComplIso j).inv ≫ ι i j hj ≫ (isColimit i).desc hf.multicofork =
    (stdSimplex.faceSingletonComplIso j).inv ≫ f j hj
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_1
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 (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ ∂Δ[d].obj (op ⦋n⦌)

Tactic:
]

Goal state after:
case refine_1
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 (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ y ∈ ∂Δ[d].obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_1
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 (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)

Tactic:
]

Goal state after:
case refine_1
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 (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ (ConcreteCategory.hom (c.map.app (op ⦋n⦌))) y ∈ ((skeletonOfMono i) d).obj (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:
]

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: X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ ⊤ ≤ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)

Tactic:
]

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ ⊤ ≤ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)
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:
]

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: 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₃
⊢ horn.faceι 1 0 ι₀._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀

Tactic:
]

Goal state after:
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₃
⊢ horn.faceι 1 0 ι₀._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: 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₃
⊢ horn.faceι 1 2 ι₂._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂

Tactic:
]

Goal state after:
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₃
⊢ horn.faceι 1 2 ι₂._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inl
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
k : Fin (m + 1)
hk : j = k.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op)) (g.arrow k) =
    (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op)) (g.arrow k)

Tactic:
]

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

Goal state before:
pp: case refine_3
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 ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)

Tactic:
]

Goal state after:
case refine_3
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 ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
⊢ (ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁) =
    (ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ.inr
n : ℕ
X : Truncated (n + 1)
m : ℕ
f g : X.Path (m + 1)
h : ∀ (i : Fin (m + 1)), f.arrow i = g.arrow i
j : Fin (m + 1 + 1)
hl : j = Fin.last (m + 1)
⊢ (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (g.arrow (Fin.last m)) =
    (ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 0) ⋯ ⋯).op)) (g.arrow (Fin.last m))

Tactic:
]

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

Goal state before:
pp: 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₃
⊢ horn.faceι 1 3 ι₃._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
]

Goal state after:
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₃
⊢ horn.faceι 1 3 ι₃._proof_1 ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
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 ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
⊢ ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))

Tactic:
]

Goal state after:
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 ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
⊢ ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₁.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₁))) =
    ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌)))
        ((ConcreteCategory.hom (c₂.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f₂)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
⊢ f.vertex i = f.vertex i

Tactic:
]

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
i : Fin m
f : X.Path m
⊢ f.arrow i = f.arrow i

Tactic:
]

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
⊢ X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f)) =
    f.interval j l hjl

Tactic:
]

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f)) =
    f.interval j l hjl
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) =
    (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m ?h f)

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

Tactic:
]

Goal state after: