x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
⊢ e = Iso.refl x
x : SimplexCategory
e : x ≅ x
⊢ e = Iso.refl x
have h : (Finset.univ : Finset (Fin (x.len + 1))).card = x.len + 1 := Finset.card_fin (x.len + 1)
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
⊢ e = Iso.refl x
have eq₁ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso e) i)
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
have eq₂ :=
  Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso (Iso.refl x)) i)
case w.a.h.h.h
x✝ : SimplexCategory
e : x✝ ≅ x✝
h : Finset.card Finset.univ = len x✝ + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x✝)) = Finset.orderEmbOfFin Finset.univ h
x : Fin (len x✝ + 1)
⊢ ↑(↑(Hom.toOrderHom e.hom) x) = ↑(↑(Hom.toOrderHom (Iso.refl x✝).hom) x)
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
ext x
no goals
case w.a.h.h.h
x✝ : SimplexCategory
e : x✝ ≅ x✝
h : Finset.card Finset.univ = len x✝ + 1
x : Fin (len x✝ + 1)
eq₁ :
  (fun x_1 => ↑x_1 x) (RelIso.toRelEmbedding (orderIsoOfIso e)) =
    (fun x_1 => ↑x_1 x) (Finset.orderEmbOfFin Finset.univ h)
eq₂ :
  (fun x_1 => ↑x_1 x) (Finset.orderEmbOfFin Finset.univ h) =
    (fun x_1 => ↑x_1 x) (RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x✝)))
⊢ ↑(↑(Hom.toOrderHom e.hom) x) = ↑(↑(Hom.toOrderHom (Iso.refl x✝).hom) x)
simp_all