[GOAL]
⊢ LargeCategory SSet
[PROOFSTEP]
dsimp only [SSet]
[GOAL]
⊢ LargeCategory (SimplicialObject (Type ?u.23))
[PROOFSTEP]
infer_instance
[GOAL]
⊢ HasLimits SSet
[PROOFSTEP]
dsimp only [SSet]
[GOAL]
⊢ HasLimits (SimplicialObject (Type ?u.489))
[PROOFSTEP]
infer_instance
[GOAL]
⊢ HasColimits SSet
[PROOFSTEP]
dsimp only [SSet]
[GOAL]
⊢ HasColimits (SimplicialObject (Type ?u.577))
[PROOFSTEP]
infer_instance
  -- Porting note: added an `ext` lemma.
  -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
n : ℕ
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // ¬Function.Surjective ↑(asOrderHom α) }) m₁
⊢ ¬Function.Surjective ↑(asOrderHom (f.unop ≫ ↑α))
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // ¬Function.Surjective ↑(asOrderHom α) }) m₁
h : Function.Surjective ↑(asOrderHom (f.unop ≫ ↑α))
⊢ False
[PROOFSTEP]
apply α.property
[GOAL]
n : ℕ
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // ¬Function.Surjective ↑(asOrderHom α) }) m₁
h : Function.Surjective ↑(asOrderHom (f.unop ≫ ↑α))
⊢ Function.Surjective ↑(asOrderHom ↑α)
[PROOFSTEP]
exact Function.Surjective.of_comp h
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
⊢ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i} ≠ Set.univ
[PROOFSTEP]
intro h
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i} = Set.univ
⊢ False
[PROOFSTEP]
apply α.property
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i} = Set.univ
⊢ Set.range ↑(asOrderHom ↑α) ∪ {i} = Set.univ
[PROOFSTEP]
rw [Set.eq_univ_iff_forall] at h ⊢
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
⊢ ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom ↑α) ∪ {i}
[PROOFSTEP]
intro j
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
j : Fin (n + 1)
⊢ j ∈ Set.range ↑(asOrderHom ↑α) ∪ {i}
[PROOFSTEP]
apply Or.imp _ id (h j)
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
j : Fin (n + 1)
⊢ j ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) → j ∈ Set.range ↑(asOrderHom ↑α)
[PROOFSTEP]
intro hj
[GOAL]
n : ℕ
i : Fin (n + 1)
m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
α : (fun m => { α // Set.range ↑(asOrderHom α) ∪ {i} ≠ Set.univ }) m₁
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α)) ∪ {i}
j : Fin (n + 1)
hj : j ∈ Set.range ↑(asOrderHom (f.unop ≫ ↑α))
⊢ j ∈ Set.range ↑(asOrderHom ↑α)
[PROOFSTEP]
exact Set.range_comp_subset_range _ _ hj
[GOAL]
n : ℕ
⊢ LargeCategory (Truncated n)
[PROOFSTEP]
dsimp only [Truncated]
[GOAL]
n : ℕ
⊢ LargeCategory (SimplicialObject.Truncated (Type ?u.74955) n)
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ HasLimits (Truncated n)
[PROOFSTEP]
dsimp only [Truncated]
[GOAL]
n : ℕ
⊢ HasLimits (SimplicialObject.Truncated (Type ?u.75436) n)
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ HasColimits (Truncated n)
[PROOFSTEP]
dsimp only [Truncated]
[GOAL]
n : ℕ
⊢ HasColimits (SimplicialObject.Truncated (Type ?u.75544) n)
[PROOFSTEP]
infer_instance
  -- Porting note: added an `ext` lemma.
  -- See https://github.com/leanprover-community/mathlib4/issues/5229
