Theorem: Tutorial.Category.Initial.uniq' (Tutorial/Advanced/Category/Lecture2.lean)

State before:
C : Type u
inst✝ : Category C
a : C
h : Initial a
b : C
f g : Hom a b
⊢ f = h.fromInitial b
Tactic:
sorry
State after:
no goals

State before:
C : Type u
inst✝ : Category C
a : C
h : Initial a
b : C
f g : Hom a b
⊢ h.fromInitial b = g
Tactic:
sorry
State after:
no goals