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