Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image φ = Δ'
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ image φ = Δ'
haveI := strongEpi_of_epi e
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ image φ = Δ'
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image φ = Δ'
let e := image.isoStrongEpiMono e i fac
case a
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ len (image φ) = len Δ'
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ image φ = Δ'
ext
no goals
case a
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ len (image φ) = len Δ'
exact
  le_antisymm (len_le_of_epi (inferInstance : Epi e.hom))
    (len_le_of_mono (inferInstance : Mono e.hom))