no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F F' : C ⥤ D
G : D ⥤ E
inst✝ : Faithful F
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₁✝ = F.map a₂✝
rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]