C : Type u_3
D : Type u_6
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category E
inst✝ : Functor.IsLocalization L W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ 𝟙 ((L ⋙ F').obj X) = 𝟙 (F'.obj (L.obj X))
C : Type u_3
D : Type u_6
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category E
inst✝ : Functor.IsLocalization L W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ (liftNatTrans L W F F F' F' (𝟙 F)).app (L.obj X) = (𝟙 F').app (L.obj X)
simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]
no goals
C : Type u_3
D : Type u_6
inst✝³ : Category C
inst✝² : Category D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category E
inst✝ : Functor.IsLocalization L W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ 𝟙 ((L ⋙ F').obj X) = 𝟙 (F'.obj (L.obj X))
rfl