no goals
C : Type u
inst✝ : Category C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ X b = Y b
rw [h]
C : Type u
inst✝ : Category C
β : Type w
X : β → C
b : β
⊢ eqToHom (_ : X = X) b = eqToHom (_ : X b = X b)
C : Type u
inst✝ : Category C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ eqToHom h b = eqToHom (_ : X b = Y b)
subst h
no goals
C : Type u
inst✝ : Category C
β : Type w
X : β → C
b : β
⊢ eqToHom (_ : X = X) b = eqToHom (_ : X b = X b)
rfl