J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j
      (↑(limitEquivSections F).symm { val := x, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), F.map f (x j) = x j') }) =
    x j
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j (mk F x h) = x j
dsimp [Limit.mk]
no goals
J : Type v
inst✝ : SmallCategory J
F : J ⥤ TypeMax
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'
j : J
⊢ limit.π F j
      (↑(limitEquivSections F).symm { val := x, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), F.map f (x j) = x j') }) =
    x j
simp