J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ lift h { pt := W, π := NatTrans.mk fun b => f ≫ t.π.app b } =
    lift h { pt := W, π := NatTrans.mk fun b => f' ≫ t.π.app b }
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ f = f'
rw [h.hom_lift f, h.hom_lift f']
case h.e_8.h.e_π.e_app
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ (fun b => f ≫ t.π.app b) = fun b => f' ≫ t.π.app b
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ lift h { pt := W, π := NatTrans.mk fun b => f ≫ t.π.app b } =
    lift h { pt := W, π := NatTrans.mk fun b => f' ≫ t.π.app b }
congr
no goals
case h.e_8.h.e_π.e_app
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ (fun b => f ≫ t.π.app b) = fun b => f' ≫ t.π.app b
exact funext w