C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : D
f : X ⟶ Y
⊢ F.map ((Functor.inv F).map f) = ((asEquivalence F).inverse ⋙ (asEquivalence F).functor).map f
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : D
f : X ⟶ Y
⊢ F.map ((Functor.inv F).map f) =
    (Equivalence.counit (asEquivalence F)).app X ≫ f ≫ (Equivalence.counitInv (asEquivalence F)).app Y
erw [NatIso.naturality_2]
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : D
f : X ⟶ Y
⊢ F.map ((Functor.inv F).map f) = ((asEquivalence F).inverse ⋙ (asEquivalence F).functor).map f
rfl