case w.h
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
E : Type u_2
inst✝² : Category E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
x✝ : C
⊢ (natIsoOfCompFullyFaithful H i).hom.app x✝ = (natTransOfCompFullyFaithful H i.hom).app x✝
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
E : Type u_2
inst✝² : Category E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
⊢ (natIsoOfCompFullyFaithful H i).hom = natTransOfCompFullyFaithful H i.hom
ext
no goals
case w.h
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
E : Type u_2
inst✝² : Category E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : Full H
inst✝ : Faithful H
i : F ⋙ H ≅ G ⋙ H
x✝ : C
⊢ (natIsoOfCompFullyFaithful H i).hom.app x✝ = (natTransOfCompFullyFaithful H i.hom).app x✝
simp [natIsoOfCompFullyFaithful]