case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ ↑(limitEquivSections F) x = ↑(limitEquivSections F) y
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ x = y
apply (limitEquivSections.{v, u} F).injective
case a.a.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
j : J
⊢ ↑(↑(limitEquivSections F) x) j = ↑(↑(limitEquivSections F) y) j
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
⊢ ↑(limitEquivSections F) x = ↑(limitEquivSections F) y
ext j
no goals
case a.a.h
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x y : limit F
w : ∀ (j : J), limit.π F j x = limit.π F j y
j : J
⊢ ↑(↑(limitEquivSections F) x) j = ↑(↑(limitEquivSections F) y) j
simp [w j]