C : Type u
inst✝ : Category C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
C : Type u
inst✝ : Category C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
⊢ eqToHom h i = eqToHom (_ : x i = x' i)
subst h
no goals
C : Type u
inst✝ : Category C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
rfl