J : Type u
f : J → Grpd
j : J
⊢ (piLimitFan f).π.app { as := j } = Pi.eval (fun i => ↑(f i)) j
J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun i => ↑(f i)) j
simp [piIsoPi]
no goals
J : Type u
f : J → Grpd
j : J
⊢ (piLimitFan f).π.app { as := j } = Pi.eval (fun i => ↑(f i)) j
rfl