case w.h
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
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
⊢ τ₁.app X = τ₂.app X
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
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
⊢ τ₁ = τ₂
ext X
case w.h
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
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
eq : Equiv.toFun (objEquiv W) (Equiv.invFun (objEquiv W) X) = X
⊢ τ₁.app X = τ₂.app X
case w.h
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
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
⊢ τ₁.app X = τ₂.app X
have eq := (objEquiv W).right_inv X
case w.h
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
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
eq : (MorphismProperty.Q W).obj X.as.obj = X
⊢ τ₁.app X = τ₂.app X
case w.h
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
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
eq : Equiv.toFun (objEquiv W) (Equiv.invFun (objEquiv W) X) = X
⊢ τ₁.app X = τ₂.app X
simp only [objEquiv] at eq
no goals
case w.h
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
τ₁ τ₂ : F ⟶ G
h : 𝟙 (MorphismProperty.Q W) ◫ τ₁ = 𝟙 (MorphismProperty.Q W) ◫ τ₂
X : MorphismProperty.Localization W
eq : (MorphismProperty.Q W).obj X.as.obj = X
⊢ τ₁.app X = τ₂.app X
rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]