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

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd : d < x.dim + 1
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate (x.dim + 1)
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
·

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd : d < x.dim + 1
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inl.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd✝ : d ≤ x.dim
hd : d < x.dim
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

pp: case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate x.dim
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
hd : x.dim ≤ x.dim
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
·

Goal state after:
case inl.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd✝ : d ≤ x.dim
hd : d < x.dim
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate d
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) (stdSimplex.objEquiv.symm g) ∉ (range (f.m j)).obj (op ⦋d⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd✝ : d ≤ x.dim
hd : d < x.dim
⊢ d + 1 < x.dim + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : isCardinalPresentable C κ X
⊢ P.retractClosure X

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.retractClosure ≤ isCardinalPresentable C κ

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : isCardinalPresentable C κ X
⊢ P.retractClosure X
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate x.dim
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
hd : x.dim ≤ x.dim
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
·

Goal state after:
case inl.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate x.dim
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
hd : x.dim ≤ x.dim
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.retractClosure ≤ isCardinalPresentable C κ

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
⊢ P.retractClosure ≤ isCardinalPresentable C κ
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Injective h.functor.mapArrow.obj

pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Surjective h.functor.mapArrow.obj

Tactic:
·

Goal state after:
case left
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Injective h.functor.mapArrow.obj
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Surjective h.functor.mapArrow.obj

Tactic:
·

Goal state after:
case right
Ω : Type w
C : Type u
inst✝ : Category.{v, u} C
h : CoreSmallCategoryOfSet Ω C
⊢ Function.Surjective h.functor.mapArrow.obj
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate (x.dim + 1)
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c

Tactic:
·

Goal state after:
case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌
hs✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∈
    (f.sigmaStdSimplex j).nonDegenerate (x.dim + 1)
hs : Mono g
hs'✝ :
  (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g) ∉
    (range (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' : stdSimplex.objEquiv.symm g ∉ Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ c,
    N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₁ f c ∨
      N.mk ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌))) (stdSimplex.objEquiv.symm g)) hs✝ hs'✝ =
        Cell.type₂ f c
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) = y

pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b

Tactic:
·

Goal state after:
case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b

Tactic:
·

Goal state after:
case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: case hsurj
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (x : (c.pt.mapCocone cX).pt), ∃ i xi, x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) xi

pp: case hinj
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (i : J) (x y : (fun X ↦ X) ((X ⋙ c.pt).obj i)),
    (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) y →
      ∃ k f, (ConcreteCategory.hom ((X ⋙ c.pt).map f)) x = (ConcreteCategory.hom ((X ⋙ c.pt).map f)) y

Tactic:
·

Goal state after:
case hsurj
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (x : (c.pt.mapCocone cX).pt), ∃ i xi, x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) xi
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ A.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

Tactic:
·

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ A.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

Tactic:
·

Goal state after:
case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: case hinj
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (i : J) (x y : (fun X ↦ X) ((X ⋙ c.pt).obj i)),
    (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) y →
      ∃ k f, (ConcreteCategory.hom ((X ⋙ c.pt).map f)) x = (ConcreteCategory.hom ((X ⋙ c.pt).map f)) y

Tactic:
·

Goal state after:
case hinj
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
this : IsFiltered J
⊢ ∀ (i : J) (x y : (fun X ↦ X) ((X ⋙ c.pt).obj i)),
    (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) y →
      ∃ k f, (ConcreteCategory.hom ((X ⋙ c.pt).map f)) x = (ConcreteCategory.hom ((X ⋙ c.pt).map f)) y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi✝ : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i < j
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x

Tactic:
·

Goal state after:
case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi✝ : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i < j
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x

Tactic:
·

Goal state after:
case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (f.mapN (Cell.type₁ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₁ f c)).dim

pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (f.mapN (Cell.type₂ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₂ f c)).dim

Tactic:
·

Goal state after:
case inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ (f.mapN (Cell.type₁ f c)).simplex ∈ X.nonDegenerate (f.mapN (Cell.type₁ f c)).dim