[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F : Cᵒᵖ ⥤ E
hF : MorphismProperty.IsInvertedBy (MorphismProperty.op W) F
⊢ L.op ⋙ (fun F hF => (lift h F.rightOp (_ : MorphismProperty.IsInvertedBy W F.rightOp)).leftOp) F hF = F
[PROOFSTEP]
convert congr_arg Functor.leftOp (h.fac F.rightOp hF.rightOp)
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁ = F₂
[PROOFSTEP]
suffices F₁.rightOp = F₂.rightOp by rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
this : F₁.rightOp = F₂.rightOp
⊢ F₁ = F₂
[PROOFSTEP]
rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁.rightOp = F₂.rightOp
[PROOFSTEP]
have eq' := congr_arg Functor.rightOp eq
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
eq' : (L.op ⋙ F₁).rightOp = (L.op ⋙ F₂).rightOp
⊢ F₁.rightOp = F₂.rightOp
[PROOFSTEP]
exact h.uniq _ _ eq'
