C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop ↔ len Δ.unop ≤ len A.fst.unop
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ len Δ.unop ≤ len A.fst.unop
rw [eqId_iff_len_eq]
case mp
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → len Δ.unop ≤ len A.fst.unop

case mpr
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len Δ.unop ≤ len A.fst.unop → len A.fst.unop = len Δ.unop
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop ↔ len Δ.unop ≤ len A.fst.unop
constructor
case mp
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len Δ.unop ≤ len A.fst.unop
case mp
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → len Δ.unop ≤ len A.fst.unop
intro h
no goals
case mp
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len Δ.unop ≤ len A.fst.unop
rw [h]
no goals
case mpr
C : Type ?u.4924
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len Δ.unop ≤ len A.fst.unop → len A.fst.unop = len Δ.unop
exact le_antisymm (len_le_of_epi (inferInstance : Epi A.e))