case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → Mono (e A)

case mpr
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono (e A) → EqId A
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ Mono (e A)
constructor
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ Mono (e A)
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → Mono (e A)
intro h
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono (e A)
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ Mono (e A)
dsimp at h
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (e (id Δ))
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ Mono (e A)
subst h
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 Δ.unop)
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (e (id Δ))
dsimp only [id, e]
no goals
case mp
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
⊢ Mono (𝟙 Δ.unop)
infer_instance
case mpr
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ EqId A
case mpr
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Mono (e A) → EqId A
intro h
case mpr
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ len Δ.unop ≤ len A.fst.unop
case mpr
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ EqId A
rw [eqId_iff_len_le]
no goals
case mpr
C : Type ?u.5440
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : Mono (e A)
⊢ len Δ.unop ≤ len A.fst.unop
exact len_le_of_mono h