J : Type w
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
F f : J → C
t : Bicone f
ht : IsLimit (toCone t)
j : J
j' : Discrete J
⊢ ι t j ≫ (toCone t).π.app j' = (Fan.mk (f j) fun j' => if h : j = j' then eqToHom (_ : f j = f j') else 0).π.app j'
J : Type w
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
F f : J → C
t : Bicone f
ht : IsLimit (toCone t)
j : J
j' : Discrete J
⊢ ι t j ≫ (toCone t).π.app j' =
    IsLimit.lift ht (Fan.mk (f j) fun j' => if h : j = j' then eqToHom (_ : f j = f j') else 0) ≫ (toCone t).π.app j'
rw [ht.fac]
no goals
J : Type w
C : Type u
inst✝¹ : Category C
inst✝ : HasZeroMorphisms C
F f : J → C
t : Bicone f
ht : IsLimit (toCone t)
j : J
j' : Discrete J
⊢ ι t j ≫ (toCone t).π.app j' = (Fan.mk (f j) fun j' => if h : j = j' then eqToHom (_ : f j = f j') else 0).π.app j'
simp [t.ι_π]