no goals
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type u_4
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
F G : MorphismProperty.Localization W ⥤ D
τ : MorphismProperty.Q W ⋙ F ⟶ MorphismProperty.Q W ⋙ G
⊢ 𝟙 (MorphismProperty.Q W) ◫ natTransExtension τ = τ
aesop_cat