[GOAL]
x : SimplexCategory
⊢ Fintype (ConcreteCategory.forget.obj x)
[PROOFSTEP]
change (Fintype (Fin _))
[GOAL]
x : SimplexCategory
⊢ Fintype (Fin (len x + 1))
[PROOFSTEP]
infer_instance
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ (fun i => ∑ j in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g j) ∈ toTopObj y
[PROOFSTEP]
simp only [Finset.sum_congr, toTopObj, Set.mem_setOf]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ ∑ i : (forget SimplexCategory).obj y, ∑ x_1 in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
[PROOFSTEP]
rw [← Finset.sum_biUnion]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ ∑ x_1 in Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
have hg := g.2
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
hg : ↑g ∈ toTopObj x
⊢ ∑ x_1 in Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
dsimp [toTopObj] at hg 
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
hg : ∑ i : (forget SimplexCategory).obj x, ↑g i = 1
⊢ ∑ x_1 in Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ, ↑g x_1 = 1
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
convert hg
[GOAL]
case h.e'_2.h
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
hg : ∑ i : (forget SimplexCategory).obj x, ↑g i = 1
⊢ (Finset.biUnion Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ) = Finset.univ
[PROOFSTEP]
simp [Finset.eq_univ_iff_forall]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
⊢ Set.PairwiseDisjoint ↑Finset.univ fun i => Finset.filter (fun k => ↑f k = i) Finset.univ
[PROOFSTEP]
intro i _ j _ h
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
⊢ (Disjoint on fun i => Finset.filter (fun k => ↑f k = i) Finset.univ) i j
[PROOFSTEP]
rw [Function.onFun, disjoint_iff_inf_le]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
⊢ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ ≤ ⊥
[PROOFSTEP]
intro e he
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : e ∈ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ
⊢ e ∈ ⊥
[PROOFSTEP]
simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : e ∈ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ
⊢ False
[PROOFSTEP]
apply h
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : e ∈ Finset.filter (fun k => ↑f k = i) Finset.univ ⊓ Finset.filter (fun k => ↑f k = j) Finset.univ
⊢ i = j
[PROOFSTEP]
simp only [Finset.mem_univ, forall_true_left, ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
  Finset.mem_filter, true_and] at he 
[GOAL]
x y : SimplexCategory
f : x ⟶ y
g : ↑(toTopObj x)
i : (forget SimplexCategory).obj y
a✝¹ : i ∈ ↑Finset.univ
j : (forget SimplexCategory).obj y
a✝ : j ∈ ↑Finset.univ
h : i ≠ j
e : (forget SimplexCategory).obj x
he : ↑f e = i ∧ ↑f e = j
⊢ i = j
[PROOFSTEP]
rw [← he.1, he.2]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
⊢ Continuous (toTopMap f)
[PROOFSTEP]
refine' Continuous.subtype_mk (continuous_pi fun i => _) _
[GOAL]
x y : SimplexCategory
f : x ⟶ y
i : (forget SimplexCategory).obj y
⊢ Continuous fun a => ∑ j in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑a j
[PROOFSTEP]
dsimp only [coe_toTopMap]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
i : (forget SimplexCategory).obj y
⊢ Continuous fun a => ∑ j in Finset.filter (fun k => ↑f k = i) Finset.univ, ↑a j
[PROOFSTEP]
exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)
[GOAL]
X✝ Y✝ : SimplexCategory
f : X✝ ⟶ Y✝
⊢ Continuous (toTopMap f)
[PROOFSTEP]
continuity
[GOAL]
⊢ ∀ (X : SimplexCategory),
    { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 X) =
      𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X)
[PROOFSTEP]
intro Δ
[GOAL]
Δ : SimplexCategory
⊢ { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ) =
    𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
[PROOFSTEP]
ext f
[GOAL]
case w
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
⊢ ↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ)) f =
    ↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f
[PROOFSTEP]
apply toTopObj.ext
[GOAL]
case w.a
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ)) f) =
    ↑(↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f)
[PROOFSTEP]
funext i
[GOAL]
case w.a.h
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
i : (forget SimplexCategory).obj Δ
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (𝟙 Δ)) f) i =
    ↑(↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f) i
[PROOFSTEP]
change (Finset.univ.filter fun k => k = i).sum _ = _
[GOAL]
case w.a.h
Δ : SimplexCategory
f :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)
i : (forget SimplexCategory).obj Δ
⊢ ∑ j in Finset.filter (fun k => k = i) Finset.univ, ↑f j =
    ↑(↑(𝟙 ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj Δ)) f) i
[PROOFSTEP]
simp [Finset.sum_filter, CategoryTheory.id_apply]
[GOAL]
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g) =
    { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
      { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g
[PROOFSTEP]
ext h
[GOAL]
case w
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
⊢ ↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g)) h =
    ↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
          { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g)
      h
[PROOFSTEP]
apply toTopObj.ext
[GOAL]
case w.a
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g)) h) =
    ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
            { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g)
        h)
[PROOFSTEP]
funext i
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map (f ≫ g)) h)
      i =
    ↑(↑({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map f ≫
              { obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.map g)
          h)
      i
[PROOFSTEP]
dsimp
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ↑(↑(ContinuousMap.mk (toTopMap (Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))))) h) i =
    ↑(↑(ContinuousMap.mk (toTopMap f) ≫ ContinuousMap.mk (toTopMap g)) h) i
[PROOFSTEP]
rw [CategoryTheory.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_mk, ContinuousMap.coe_mk]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ↑(toTopMap (Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) h) i = ↑(toTopMap g (toTopMap f h)) i
[PROOFSTEP]
simp only [coe_toTopMap]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ∑ j in Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ,
      ↑h j =
    ∑ x in Finset.filter (fun k => ↑g k = i) Finset.univ, ∑ j in Finset.filter (fun k => ↑f k = x) Finset.univ, ↑h j
[PROOFSTEP]
erw [← Finset.sum_biUnion]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ∑ j in Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ,
      ↑h j =
    ∑ x in
      Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
        Finset.filter (fun k => ↑f k = x) Finset.univ,
      ↑h x
[PROOFSTEP]
apply Finset.sum_congr
[GOAL]
case w.a.h.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ =
    Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
      Finset.filter (fun k => ↑f k = x) Finset.univ
[PROOFSTEP]
exact Finset.ext (fun j => ⟨fun hj => by simpa using hj, fun hj => by simpa using hj⟩)
[GOAL]
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj X✝
hj : j ∈ Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ
⊢ j ∈
    Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
      Finset.filter (fun k => ↑f k = x) Finset.univ
[PROOFSTEP]
simpa using hj
[GOAL]
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj X✝
hj :
  j ∈
    Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
      Finset.filter (fun k => ↑f k = x) Finset.univ
⊢ j ∈ Finset.filter (fun k => ↑(Hom.mk (OrderHom.comp (Hom.toOrderHom g) (Hom.toOrderHom f))) k = i) Finset.univ
[PROOFSTEP]
simpa using hj
[GOAL]
case w.a.h.a
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ ∀ (x : (forget SimplexCategory).obj X✝),
    (x ∈
        Finset.biUnion (Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
          Finset.filter (fun k => ↑f k = x) Finset.univ) →
      ↑h x = ↑h x
[PROOFSTEP]
tauto
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
⊢ Set.PairwiseDisjoint ↑(Finset.filter (fun k => ↑g k = i) Finset.univ) fun x =>
    Finset.filter (fun k => ↑f k = x) Finset.univ
[PROOFSTEP]
intro j _ k _ h
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
⊢ (Disjoint on fun x => Finset.filter (fun k => ↑f k = x) Finset.univ) j k
[PROOFSTEP]
rw [Function.onFun, disjoint_iff_inf_le]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
⊢ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ ≤ ⊥
[PROOFSTEP]
intro e he
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : e ∈ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ
⊢ e ∈ ⊥
[PROOFSTEP]
simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : e ∈ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : e ∈ Finset.filter (fun k => ↑f k = j) Finset.univ ⊓ Finset.filter (fun k_1 => ↑f k_1 = k) Finset.univ
⊢ j = k
[PROOFSTEP]
simp only [Finset.mem_univ, forall_true_left, ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
  Finset.mem_filter, true_and] at he 
[GOAL]
case w.a.h
X✝ Y✝ Z✝ : SimplexCategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h✝ :
  (forget TopCat).obj
    ({ obj := fun x => TopCat.of ↑(toTopObj x), map := fun {X Y} f => ContinuousMap.mk (toTopMap f) }.obj X✝)
i : (forget SimplexCategory).obj Z✝
j : (forget SimplexCategory).obj Y✝
a✝¹ : j ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
k : (forget SimplexCategory).obj Y✝
a✝ : k ∈ ↑(Finset.filter (fun k => ↑g k = i) Finset.univ)
h : j ≠ k
e : (forget SimplexCategory).obj X✝
he : ↑f e = j ∧ ↑f e = k
⊢ j = k
[PROOFSTEP]
rw [← he.1, he.2]
