case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → A.fst = Δ

case mpr
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → EqId A
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A ↔ A.fst = Δ
constructor
case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ A.fst = Δ
case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ EqId A → A.fst = Δ
intro h
case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ
case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : EqId A
⊢ A.fst = Δ
dsimp at h
case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ
case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ A.fst = Δ
rw [h]
no goals
case mp
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A = id Δ
⊢ (id Δ).fst = Δ
rfl
case mpr
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ EqId A
case mpr
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ → EqId A
intro h
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : { fst := fst✝, snd := { val := f, property := hf } }.fst = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
case mpr
C : Type ?u.4324
inst✝ : Category C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : A.fst = Δ
⊢ EqId A
rcases A with ⟨_, ⟨f, hf⟩⟩
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : fst✝ = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : { fst := fst✝, snd := { val := f, property := hf } }.fst = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
simp only at h
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
Δ fst✝ : SimplexCategoryᵒᵖ
f : Δ.unop ⟶ fst✝.unop
hf : Epi f
h : fst✝ = Δ
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
subst h
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ EqId { fst := fst✝, snd := { val := f, property := hf } }
refine' ext _ _ rfl _
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
haveI := hf
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } = e (id fst✝)
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } ≫
      eqToHom (_ : { fst := fst✝, snd := { val := f, property := hf } }.fst.unop = (id fst✝).fst.unop) =
    e (id fst✝)
simp only [eqToHom_refl, comp_id]
no goals
case mpr.mk.mk
C : Type ?u.4324
inst✝ : Category C
fst✝ : SimplexCategoryᵒᵖ
f : fst✝.unop ⟶ fst✝.unop
hf this : Epi f
⊢ e { fst := fst✝, snd := { val := f, property := hf } } = e (id fst✝)
exact eq_id_of_epi f