case w
C : Type u
inst✝¹ : Category C
D : Type u₁
inst✝ : Category D
F✝ F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (↑(Iso.conjAut α) f)).hom = (↑(Iso.conjAut (F.mapIso α)) (F.mapIso f)).hom
C : Type u
inst✝¹ : Category C
D : Type u₁
inst✝ : Category D
F✝ F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ F.mapIso (↑(Iso.conjAut α) f) = ↑(Iso.conjAut (F.mapIso α)) (F.mapIso f)
ext
no goals
case w
C : Type u
inst✝¹ : Category C
D : Type u₁
inst✝ : Category D
F✝ F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (↑(Iso.conjAut α) f)).hom = (↑(Iso.conjAut (F.mapIso α)) (F.mapIso f)).hom
simp only [mapIso_hom, Iso.conjAut_hom, F.map_conj]