case intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
c : Cone F
t : IsLimit c
j : J
x : c.pt
⊢ c.π.app j (↑(isLimitEquivSections t).symm (↑(isLimitEquivSections t) x)) = ↑(↑(isLimitEquivSections t) x) j
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
c : Cone F
t : IsLimit c
x : ↑(Functor.sections F)
j : J
⊢ c.π.app j (↑(isLimitEquivSections t).symm x) = ↑x j
obtain ⟨x, rfl⟩ := (isLimitEquivSections.{v, u} t).surjective x
no goals
case intro
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
c : Cone F
t : IsLimit c
j : J
x : c.pt
⊢ c.π.app j (↑(isLimitEquivSections t).symm (↑(isLimitEquivSections t) x)) = ↑(↑(isLimitEquivSections t) x) j
simp