-- Mathlib/CategoryTheory/Localization/Prod.lean
lemma prod_uniq (F₁ F₂ : (W₁.Localization × W₂.Localization ⥤ E))
    (h : (W₁.Q.prod W₂.Q) ⋙ F₁ = (W₁.Q.prod W₂.Q) ⋙ F₂) :
      F₁ = F₂

Proof state:
case h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₁.Q ⋙ curry.obj F₁).flip = (W₁.Q ⋙ curry.obj F₂).flip

Tactic:
apply Construction.uniq

Result:
case h.h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip

Proof state:
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ F₁ = F₂

Tactic:
apply Functor.curry_obj_injective

Result:
case h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ curry.obj F₁ = curry.obj F₂

Proof state:
case h.h.h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip

Tactic:
apply Functor.uncurry_obj_injective

Result:
case h.h.h.h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip

Proof state:
case h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ curry.obj F₁ = curry.obj F₂

Tactic:
apply Construction.uniq

Result:
case h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₁.Q ⋙ curry.obj F₁ = W₁.Q ⋙ curry.obj F₂

Proof state:
case h.h.h.h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = uncurry.obj (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip

Tactic:
simpa only [Functor.uncurry_obj_curry_obj_flip_flip] using h

Result:
no goals

Proof state:
case h.h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip

Tactic:
apply Functor.flip_injective

Result:
case h.h.h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ curry.obj F₂).flip).flip

Proof state:
case h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ W₁.Q ⋙ curry.obj F₁ = W₁.Q ⋙ curry.obj F₂

Tactic:
apply Functor.flip_injective

Result:
case h.h.h
C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ (W₁.Q ⋙ curry.obj F₁).flip = (W₁.Q ⋙ curry.obj F₂).flip