C : Type u_6
D : Type u_3
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₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : EssSurj L
⊢ τ = τ'
C : Type u_6
D : Type u_3
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₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
⊢ τ = τ'
haveI : CategoryTheory.EssSurj L := essSurj L W
case w.h
C : Type u_6
D : Type u_3
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₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : EssSurj L
Y : D
⊢ τ.app Y = τ'.app Y
C : Type u_6
D : Type u_3
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₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : EssSurj L
⊢ τ = τ'
ext Y
no goals
case w.h
C : Type u_6
D : Type u_3
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₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : EssSurj L
Y : D
⊢ τ.app Y = τ'.app Y
rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]