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

case mpr
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → A.fst = Δ
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ ↔ len A.fst.unop = len Δ.unop
constructor
case mp
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ len A.fst.unop = len Δ.unop
case mp
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → len A.fst.unop = len Δ.unop
intro h
no goals
case mp
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ len A.fst.unop = len Δ.unop
rw [h]
case mpr
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst = Δ
case mpr
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ len A.fst.unop = len Δ.unop → A.fst = Δ
intro h
case mpr
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst.unop = Δ.unop
case mpr
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst = Δ
rw [← unop_inj_iff]
case mpr.a
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len A.fst.unop = len Δ.unop
case mpr
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ A.fst.unop = Δ.unop
ext
no goals
case mpr.a
C : Type ?u.4787
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : len A.fst.unop = len Δ.unop
⊢ len A.fst.unop = len Δ.unop
exact h