awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
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₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage
      (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔
    W₂ f

Tactic:
W₂.arrow_mk_iso_iff
      (Arrow.isoMk (Φ.functor.asEquivalence.counitIso.app _)
        (Φ.functor.asEquivalence.counitIso.app _))

Premises used: CategoryTheory.MorphismProperty.inverseImage, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.isoMk, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
Goal:
C₁ : Type u₁
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₃} C₃
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₃, u₃} C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
inst_5 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_6 : L₂.IsLocalization W₂
G : Functor.{v₄, v₅, u₄, u₅} D₁ D₂
inst_7 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_8 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_9 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage
      (Φ.inv (W₁ := W₁) (W₂ := W₂).functor (W₁ := W₂) (W₂ := W₁)) f ↔
    W₂ f

Tactic:
exact W₂.arrow_mk_iso_iff
      (Arrow.isoMk (Φ.functor.asEquivalence.counitIso.app _)
        (Φ.functor.asEquivalence.counitIso.app _))

Premises used: CategoryTheory.LocalizerMorphism.functor, CategoryTheory.Functor.asEquivalence, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.Iso.app, CategoryTheory.Arrow.isoMk, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
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₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_3 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_4 : W₂.RespectsIso
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
IsLocalizedEquivalence.of_equivalence _ (fun X Y f hf ↦ ?_)

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
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₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_3 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_4 : W₂.RespectsIso
refine : ∀ (X Y : C₂) (f : X ⟶ Y) (hf : W₂ f), W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f
⊢ Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)

Tactic:
refine IsLocalizedEquivalence.of_equivalence _ (fun X Y f hf ↦ ?_)

Premises used: CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
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₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_3 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_4 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
e : Arrow.mk (X := Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage X)) (Y :=
    Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage Y))
    (Φ.functor (W₁ := W₁) (W₂ := W₂).map
      (Φ.functor (W₁ := W₁) (W₂ := W₂).preimage
        (Iso.hom (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X) ≫
          f ≫ Iso.inv (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y)))) ≅
  Arrow.mk f :=
  Arrow.isoMk (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X)
    (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y) ⋯
simp : (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f
⊢ W₁.map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f

Tactic:
simp only [← Φ.inverseImage_eq]

Premises used: CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
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₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_3 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_4 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
e : Arrow.mk (X := Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage X)) (Y :=
    Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage Y))
    (Φ.functor (W₁ := W₁) (W₂ := W₂).map
      (Φ.functor (W₁ := W₁) (W₂ := W₂).preimage
        (Iso.hom (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X) ≫
          f ≫ Iso.inv (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y)))) ≅
  Arrow.mk f :=
  Arrow.isoMk (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X)
    (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y) ⋯
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f

Tactic:
⟨_, _, _, (W₂.arrow_mk_iso_iff e).2 hf, ⟨e⟩⟩

Premises used: Iff.mpr, Nonempty.intro, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.MorphismProperty.map, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism
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₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : Φ.functor (W₁ := W₁) (W₂ := W₂).IsEquivalence
inst_3 : Φ.IsInduced (W₁ := W₁) (W₂ := W₂)
inst_4 : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
e : Arrow.mk (X := Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage X)) (Y :=
    Φ.functor (W₁ := W₁) (W₂ := W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).objPreimage Y))
    (Φ.functor (W₁ := W₁) (W₂ := W₂).map
      (Φ.functor (W₁ := W₁) (W₂ := W₂).preimage
        (Iso.hom (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X) ≫
          f ≫ Iso.inv (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y)))) ≅
  Arrow.mk f :=
  Arrow.isoMk (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso X)
    (Φ.functor (W₁ := W₁) (W₂ := W₂).objObjPreimageIso Y) ⋯
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).map (Φ.functor (W₁ := W₁) (W₂ := W₂)) f

Tactic:
exact ⟨_, _, _, (W₂.arrow_mk_iso_iff e).2 hf, ⟨e⟩⟩
-- Module: Mathlib.CategoryTheory.Localization.LocallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
⊢ LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)

Tactic:
have : LocallySmall.{w} (InducedCategory _ L.obj) :=
    ⟨fun X Y ↦ small_of_injective InducedCategory.homEquiv.injective⟩
-- Module: Mathlib.CategoryTheory.Localization.LocallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L W
-- Module: Mathlib.CategoryTheory.Localization.LocallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this_1 : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
this : L.EssSurj
⊢ EssSurj.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)

Tactic:
have : (inducedFunctor L.obj).EssSurj := ⟨fun Y ↦ ⟨_, ⟨L.objObjPreimageIso Y⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Localization.LocallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this_1 : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
this_2 : L.EssSurj
this : EssSurj.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
⊢ IsEquivalence.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)

Tactic:
have : (inducedFunctor L.obj).IsEquivalence := { }
-- Module: Mathlib.CategoryTheory.Localization.LocallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this_1 : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
this_2 : L.EssSurj
this_3 : EssSurj.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
this : IsEquivalence.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
e : Equivalence.{v₂, v₂, u₁, u₂} (InducedCategory D L.obj) D := asEquivalence (inducedFunctor L.obj)
e' : (L' ⋙ e.functor) ⋙ e.inverse ≅ L' :=
  L'.associator e.functor e.inverse ≪≫ L'.isoWhiskerLeft e.unitIso.symm ≪≫ L'.rightUnitor
⊢ L'.IsLocalization W

Tactic:
have : L'.IsLocalization W :=
    Functor.IsLocalization.of_iso W (L₁ := L ⋙ e.inverse) e'
-- Module: Mathlib.CategoryTheory.Localization.LocallySmall
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : L.IsLocalization W
this_1 : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : Functor.{v₁, v₂, u₁, u₁} C (InducedCategory D L.obj) :=
  { obj := fun (X : C) ↦ X, map := fun {X Y : C} (f : X ⟶ Y) ↦ InducedCategory.homMk (L.map f), map_id := ⋯,
    map_comp := ⋯ }
this_2 : L.EssSurj
this_3 : EssSurj.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
this_4 : IsEquivalence.{v₂, v₂, u₁, u₂} (inducedFunctor L.obj)
e : Equivalence.{v₂, v₂, u₁, u₂} (InducedCategory D L.obj) D := asEquivalence (inducedFunctor L.obj)
e' : (L' ⋙ e.functor) ⋙ e.inverse ≅ L' :=
  L'.associator e.functor e.inverse ≪≫ L'.isoWhiskerLeft e.unitIso.symm ≪≫ L'.rightUnitor
this : L'.IsLocalization W
⊢ HasLocalization.{w, v₁, u₁} W

Tactic:
exact hasLocalizationOfLocallySmall.{w} W L'
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMultiplicative
h :
  ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ⊗ₘ g)
X x x_1 : C
g : x ⟶ x_1
hg : W g
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X x) (X ◁ g)

Tactic:
simpa using h (𝟙 X) g (W.id_mem _) hg

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMultiplicative
h :
  ∀ {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂), W f → W g → W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ⊗ₘ g)
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
Y : C
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y) (f ▷ Y)

Tactic:
simpa using h f (𝟙 Y) hf (W.id_mem _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMonoidal
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hg : W g
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X Y₁) (X ◁ g)

Tactic:
IsMonoidal.whiskerLeft _ _ hg

Premises used: CategoryTheory.MorphismProperty.IsMonoidal.whiskerLeft
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
Y : C
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y) (f ▷ Y)

Tactic:
IsMonoidal.whiskerRight _ hf Y

Premises used: CategoryTheory.MorphismProperty.IsMonoidal.whiskerRight
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
rw : W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ▷ Y₁ ≫ X₂ ◁ g)
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ⊗ₘ g)

Tactic:
rw [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ▷ Y₁ ≫ X₂ ◁ g)

Tactic:
comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.whiskerLeft_mem, CategoryTheory.MorphismProperty.whiskerRight_mem
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) (f ▷ Y₁ ≫ X₂ ◁ g)

Tactic:
exact comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)

Premises used: CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.whiskerLeft_mem, CategoryTheory.MorphismProperty.whiskerRight_mem
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W.inverseImage F f
hg : W.inverseImage F g
simp :
  ∀ (hf : W (F.map f)) (hg : W (F.map g)), W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (F.map (f ⊗ₘ g))
⊢ W.inverseImage F (X := tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁) (f ⊗ₘ g)

Tactic:
simp only [inverseImage_iff] at hf hg ⊢

Premises used: CategoryTheory.MorphismProperty.inverseImage_iff
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
rw :
  W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (Y := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Functor.OplaxMonoidal.δ F X₁ Y₁)
      ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂))
⊢ W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (F.map (f ⊗ₘ g))

Tactic:
rw [Functor.Monoidal.map_tensor _ f g]

Premises used: CategoryTheory.Functor.Monoidal.map_tensor
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
hf₁ :
  W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Y :=
    F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂)) ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂)
⊢ W (X := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₁ Y₁)) (Y := F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂))
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Functor.OplaxMonoidal.δ F X₁ Y₁)
      ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂))

Tactic:
apply MorphismProperty.RespectsIso.precomp

Premises used: CategoryTheory.MorphismProperty.RespectsIso.precomp
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
hf₁ : W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (F.map f ⊗ₘ F.map g)
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (Y :=
    F.obj (tensorObj.{v_3, u_3} (𝒞 := inst_4) X₂ Y₂)) ((F.map f ⊗ₘ F.map g) ≫ Functor.LaxMonoidal.μ F X₂ Y₂)

Tactic:
apply MorphismProperty.RespectsIso.postcomp

Premises used: CategoryTheory.MorphismProperty.RespectsIso.postcomp
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (F.map f ⊗ₘ F.map g)

Tactic:
tensorHom_mem _ _ _ hf hg

Premises used: CategoryTheory.MorphismProperty.tensorHom_mem
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
C' : Type u_3
inst_4 : Category.{v_3, u_3} C'
inst_5 : MonoidalCategory.{v_3, u_3} C'
F : Functor.{v_3, v_1, u_3, u_1} C' C
inst_6 : F.Monoidal
inst_7 : W.RespectsIso
X₁ X₂ Y₁ Y₂ : C'
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : W (F.map f)
hg : W (F.map g)
⊢ W (X := tensorObj.{v_1, u_1} (𝒞 := inst) (F.obj X₁) (F.obj Y₁)) (F.map f ⊗ₘ F.map g)

Tactic:
exact tensorHom_mem _ _ _ hf hg

Premises used: CategoryTheory.MorphismProperty.tensorHom_mem
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
⊢ Functor.IsLocalization (D := LocalizedMonoidal L W ε) L' W

Tactic:
inferInstanceAs (L.IsLocalization W)

Premises used: _private.0.CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory._proof_1
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ Y₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
⊢ IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (X₁, Y₁).1 Y₁))
    (Functor.map L' (f₁ ▷ Y₁))

Tactic:
have := Localization.inverts L' W _ (W.whiskerRight_mem f₁ hf₁ Y₁)
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ Y₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
this :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (X₁, Y₁).1 Y₁))
    (Functor.map L' (f₁ ▷ Y₁))
⊢ IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ (X₁, Y₁).2))
    (Functor.map L' (X₂ ◁ f₂))

Tactic:
have := Localization.inverts L' W _ (W.whiskerLeft_mem X₂ f₂ hf₂)