case h
β : Type w
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ (G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b => G.obj (f b)) j =
    (Pi.lift fun j => G.map (g j)) ≫ Pi.π (fun b => G.obj (f b)) j
β : Type w
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
⊢ G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j)
ext j
no goals
case h
β : Type w
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ (G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b => G.obj (f b)) j =
    (Pi.lift fun j => G.map (g j)) ≫ Pi.π (fun b => G.obj (f b)) j
simp only [Discrete.functor_obj, Category.assoc, piComparison_comp_π, ← G.map_comp,
  limit.lift_π, Fan.mk_pt, Fan.mk_π_app]