awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
h₁ : obj curry F₁ = obj curry F₂
⊢ F₁ = F₂

Tactic:
apply Functor.curry_obj_injective

Premises used: CategoryTheory.Functor.curry_obj_injective
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
h₁ : W₁.Q ⋙ obj curry F₁ = W₁.Q ⋙ obj curry F₂
⊢ obj curry F₁ = obj curry F₂

Tactic:
apply Construction.uniq

Premises used: CategoryTheory.Localization.Construction.uniq
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
h₁ : (W₁.Q ⋙ obj curry F₁).flip = (W₁.Q ⋙ obj curry F₂).flip
⊢ W₁.Q ⋙ obj curry F₁ = W₁.Q ⋙ obj curry F₂

Tactic:
apply Functor.flip_injective

Premises used: CategoryTheory.Functor.flip_injective
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
h₁ : W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip
⊢ (W₁.Q ⋙ obj curry F₁).flip = (W₁.Q ⋙ obj curry F₂).flip

Tactic:
apply Construction.uniq

Premises used: CategoryTheory.Localization.Construction.uniq
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
h₁ : (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip).flip
⊢ W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip = W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip

Tactic:
apply Functor.flip_injective

Premises used: CategoryTheory.Functor.flip_injective
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
h₁ : obj uncurry (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip).flip = obj uncurry (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip).flip
⊢ (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip).flip = (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip).flip

Tactic:
apply Functor.uncurry_obj_injective

Premises used: CategoryTheory.Functor.uncurry_obj_injective
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F₁ F₂ : Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ obj uncurry (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₁).flip).flip = obj uncurry (W₂.Q ⋙ (W₁.Q ⋙ obj curry F₂).flip).flip

Tactic:
simpa only [Functor.uncurry_obj_curry_obj_flip_flip] using h

Premises used: CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
inst_5 : W₂.ContainsIdentities
hF : (W₁.prod W₂).IsInvertedBy F
x x_1 : C₁
f₁ : x ⟶ x_1
hf₁ : W₁ f₁
⊢ ∀ (X₂ : C₂), IsIso (((obj curry F).map f₁).app X₂)

Tactic:
haveI : ∀ (X₂ : C₂), IsIso (((curry.obj F).map f₁).app X₂) :=
      fun X₂ => hF _ ⟨hf₁, MorphismProperty.id_mem _ _⟩
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
inst_5 : W₂.ContainsIdentities
hF : (W₁.prod W₂).IsInvertedBy F
x x_1 : C₁
f₁ : x ⟶ x_1
hf₁ : W₁ f₁
this : ∀ (X₂ : C₂), IsIso (((obj curry F).map f₁).app X₂)
⊢ IsIso ((obj curry F).map f₁)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₂.ContainsIdentities
⊢ W₁.Q ⋙ prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF = obj curry F

Tactic:
Construction.fac _ _

Premises used: CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁, CategoryTheory.Localization.Construction.fac
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
refine : W₂.IsInvertedBy (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip
⊢ Prod.{u₁, u₂} W₁.Localization W₂.Localization ⥤ E

Tactic:
refine uncurry.obj (Construction.lift (prodLift₁ F hF).flip ?_).flip

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Localization.Construction.lift, CategoryTheory.Functor.uncurry, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X : C₂
_ : ∀ ⦃Y : C₂⦄ (f : X ⟶ Y), W₂ f → IsIso ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f)
⊢ ∀ ⦃Y : C₂⦄ (f : X ⟶ Y), W₂ f → IsIso ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X Y : C₂
f₂ : X ⟶ Y
hf₂ : W₂ f₂
X₁ : W₁.Localization
obtain :
  ∀ (X₁ : C₁),
    IsIso (X :=
      ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.obj X).obj
        ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))
      (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app
        ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))
⊢ IsIso (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app X₁)

Tactic:
obtain ⟨X₁, rfl⟩ := (Construction.objEquiv W₁).surjective X₁

Premises used: Equiv.surjective, CategoryTheory.Localization.Construction.objEquiv, rfl
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X Y : C₂
f₂ : X ⟶ Y
hf₂ : W₂ f₂
X₁ : C₁
⊢ IsIso (X :=
    ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.obj X).obj
      ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))
    (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app
      ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))

Tactic:
((MorphismProperty.isomorphisms E).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (eqToIso (Functor.congr_obj (prod_fac₁ F hF) X₁))).app (Arrow.mk f₂))).2
          (hF _ ⟨MorphismProperty.id_mem _ _, hf₂⟩)

Premises used: Iff.mpr, CategoryTheory.Functor.congr_obj, CategoryTheory.eqToIso, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, And.intro, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X Y : C₂
f₂ : X ⟶ Y
hf₂ : W₂ f₂
X₁ : C₁
⊢ IsIso (X :=
    ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.obj X).obj
      ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))
    (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app
      ((Construction.objEquiv W₁ : (a : C₁) → W₁.Localization) X₁))

Tactic:
exact ((MorphismProperty.isomorphisms E).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (eqToIso (Functor.congr_obj (prod_fac₁ F hF) X₁))).app (Arrow.mk f₂))).2
          (hF _ ⟨MorphismProperty.id_mem _ _, hf₂⟩)

Premises used: Iff.mpr, CategoryTheory.Functor.congr_obj, CategoryTheory.eqToIso, CategoryTheory.Functor.mapArrowFunctor, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, And.intro, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.Iso.app, CategoryTheory.Arrow.mk, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X Y : C₂
f₂ : X ⟶ Y
hf₂ : W₂ f₂
⊢ ∀ (X₁ : W₁.Localization), IsIso (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app X₁)

Tactic:
haveI : ∀ (X₁ : W₁.Localization),
      IsIso (((Functor.flip (prodLift₁ F hF)).map f₂).app X₁) := fun X₁ => by
    obtain ⟨X₁, rfl⟩ := (Construction.objEquiv W₁).surjective X₁
    exact ((MorphismProperty.isomorphisms E).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (eqToIso (Functor.congr_obj (prod_fac₁ F hF) X₁))).app (Arrow.mk f₂))).2
          (hF _ ⟨MorphismProperty.id_mem _ _, hf₂⟩)
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_5 : W₁.ContainsIdentities
inst_6 : W₂.ContainsIdentities
X Y : C₂
f₂ : X ⟶ Y
hf₂ : W₂ f₂
this : ∀ (X₁ : W₁.Localization), IsIso (((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂).app X₁)
⊢ IsIso ((prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.map f₂)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
simp :
  W₂.Q ⋙ Construction.lift (W := W₂) (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip ⋯ =
    (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip
⊢ W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip = (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip

Tactic:
simp only [prodLift, Functor.curry_obj_uncurry_obj, Functor.flip_flip]

Premises used: CategoryTheory.Functor.curry_obj_uncurry_obj, CategoryTheory.Functor.flip_flip, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
⊢ W₂.Q ⋙ Construction.lift (W := W₂) (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip ⋯ =
    (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip

Tactic:
apply Construction.fac

Premises used: CategoryTheory.Localization.Construction.fac
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
E : Type u₅
inst_2 : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst_3 : W₁.ContainsIdentities
inst_4 : W₂.ContainsIdentities
rw : obj uncurry (W₁.Q ⋙ (W₂.Q ⋙ (obj curry (prodLift (W₁ := W₁) (W₂ := W₂) F hF)).flip).flip) = F
rw₁ : obj uncurry (W₁.Q ⋙ (prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF).flip.flip) = F
rw₂ : obj uncurry (W₁.Q ⋙ prodLift₁ (W₁ := W₁) (W₂ := W₂) F hF) = F
rw₃ : obj uncurry (obj curry F) = F
rw₄ rw₅ : F = F
⊢ W₁.Q.prod W₂.Q ⋙ prodLift (W₁ := W₁) (W₂ := W₂) F hF = F

Tactic:
rw [← Functor.uncurry_obj_curry_obj_flip_flip', prod_fac₂, Functor.flip_flip, prod_fac₁,
    Functor.uncurry_obj_curry_obj]

Premises used: CategoryTheory.Functor.uncurry_obj_curry_obj, CategoryTheory.Functor.flip_flip, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₂, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac₁, CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip'
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_2 : W₁.ContainsIdentities
inst_3 : W₂.ContainsIdentities
⊢ (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)

Tactic:
Functor.IsLocalization.mk' _ _
    (StrictUniversalPropertyFixedTarget.prod W₁ W₂)
    (StrictUniversalPropertyFixedTarget.prod W₁ W₂)

Premises used: CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod, CategoryTheory.Functor.IsLocalization.mk'
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_4 : W₁.ContainsIdentities
inst_5 : W₂.ContainsIdentities
inst_6 : L₁.IsLocalization W₁
inst_7 : L₂.IsLocalization W₂
⊢ (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)

Tactic:
haveI := Construction.prodIsLocalization W₁ W₂
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_4 : W₁.ContainsIdentities
inst_5 : W₂.ContainsIdentities
inst_6 : L₁.IsLocalization W₁
inst_7 : L₂.IsLocalization W₂
this : (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)
⊢ (L₁.prod L₂).IsLocalization (W₁.prod W₂)

Tactic:
of_equivalence_target (W₁.Q.prod W₂.Q) (W₁.prod W₂) (L₁.prod L₂)
    ((uniq W₁.Q L₁ W₁).prod (uniq W₂.Q L₂ W₂))
    (NatIso.prod (compUniqFunctor W₁.Q L₁ W₁) (compUniqFunctor W₂.Q L₂ W₂))

Premises used: CategoryTheory.Equivalence.prod, CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.uniq, CategoryTheory.MorphismProperty.prod, CategoryTheory.Functor.prod, CategoryTheory.NatIso.prod, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- Module: Mathlib.CategoryTheory.Localization.Prod
Goal:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} D₁
inst_3 : Category.{v₄, u₄} D₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
W₁ : MorphismProperty.{v₁, u₁} C₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_4 : W₁.ContainsIdentities
inst_5 : W₂.ContainsIdentities
inst_6 : L₁.IsLocalization W₁
inst_7 : L₂.IsLocalization W₂
this : (W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)
⊢ (L₁.prod L₂).IsLocalization (W₁.prod W₂)

Tactic:
exact of_equivalence_target (W₁.Q.prod W₂.Q) (W₁.prod W₂) (L₁.prod L₂)
    ((uniq W₁.Q L₁ W₁).prod (uniq W₂.Q L₂ W₂))
    (NatIso.prod (compUniqFunctor W₁.Q L₁ W₁) (compUniqFunctor W₂.Q L₂ W₂))

Premises used: CategoryTheory.Equivalence.prod, CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.uniq, CategoryTheory.MorphismProperty.prod, CategoryTheory.Functor.prod, CategoryTheory.NatIso.prod, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- Module: Mathlib.CategoryTheory.Localization.Quotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
homRel : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
h : homRel.FactorsThroughLocalization W
W' : MorphismProperty.{v_1, u_1} (CategoryTheory.Quotient homRel)
hW : W = W'.inverseImage (Quotient.functor homRel)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
x x_1 : C
x_2 : x ⟶ x_1
hf : W x_2
rwa rwa₁ rwa₂ rwa₃ : ∀ (hf : W'.inverseImage (Quotient.functor homRel) x_2), W' ((Quotient.functor homRel).map x_2)
⊢ W' ((Quotient.functor homRel).map x_2)

Tactic:
rwa [hW] at hf
-- Module: Mathlib.CategoryTheory.Localization.Quotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
homRel : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
h : homRel.FactorsThroughLocalization W
W' : MorphismProperty.{v_1, u_1} (CategoryTheory.Quotient homRel)
hW : W = W'.inverseImage (Quotient.functor homRel)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
F : CategoryTheory.Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
K L : CategoryTheory.Quotient homRel
f_1 : K ⟶ L
f : K.as (r := homRel) ⟶ L.as (r := homRel)
hf : W' (Quot.mk (HomRel.CompClosure homRel) f)
⊢ W f

Tactic:
simpa [hW] using hf
-- Module: Mathlib.CategoryTheory.Localization.Quotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
homRel : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
h : homRel.FactorsThroughLocalization W
W' : MorphismProperty.{v_1, u_1} (CategoryTheory.Quotient homRel)
hW : W = W'.inverseImage (Quotient.functor homRel)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
F : CategoryTheory.Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
K L : CategoryTheory.Quotient homRel
f_1 : K ⟶ L
f : K.as (r := homRel) ⟶ L.as (r := homRel)
hf : W' (Quot.mk (HomRel.CompClosure homRel) f)
⊢ IsIso ((CategoryTheory.Quotient.lift homRel F ⋯).map (Quot.mk (HomRel.CompClosure homRel) f))

Tactic:
exact hF _ (by simpa [hW] using hf)
-- Module: Mathlib.CategoryTheory.Localization.Quotient
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
homRel : HomRel.{u_1, v_1} C
W : MorphismProperty.{v_1, u_1} C
h : homRel.FactorsThroughLocalization W
W' : MorphismProperty.{v_1, u_1} (CategoryTheory.Quotient homRel)
hW : W = W'.inverseImage (Quotient.functor homRel)
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L' : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} (CategoryTheory.Quotient homRel) D
univ : StrictUniversalPropertyFixedTarget.{v_1, u_1, v_2, u_2, v_3, u_3} L' W' E
F : CategoryTheory.Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
rw : Quotient.functor homRel ⋙ L' ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F ⋯) ⋯ = F
rw₁ : Quotient.functor homRel ⋙ CategoryTheory.Quotient.lift homRel F ⋯ = F
rw₂ rw₃ : F = F
⊢ (Quotient.functor homRel ⋙ L') ⋙ univ.lift (W := W') (CategoryTheory.Quotient.lift homRel F ⋯) ⋯ = F

Tactic:
rw [Functor.assoc, univ.fac, Quotient.lift_spec]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac, CategoryTheory.Quotient.lift_spec