U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast (_ : (u ⟶ v) = (u' ⟶ v')) e = e' ↔ HEq e e'
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ cast hu hv e = e' ↔ HEq e e'
rw [Hom.cast_eq_cast]
no goals
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast (_ : (u ⟶ v) = (u' ⟶ v')) e = e' ↔ HEq e e'
exact _root_.cast_eq_iff_heq