Theorem: Tutorial.Category.Initial.uniq' (Solution/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:
rw [h.uniq f]
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:
rw [h.uniq g]
State after:
no goals