awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
F : Functor.{v₁, v₄, u₁, u₄} C₁ E
hF : W₃.IsInvertedBy F
rw : L₁ ⋙ L₂ ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F ⋯) ⋯ = F
rw₁ : L₁ ⋙ h₁.lift (W := W₁) F ⋯ = F
rw₂ rw₃ : F = F
⊢ (L₁ ⋙ L₂) ⋙ h₂.lift (W := W₂) (h₁.lift (W := W₁) F ⋯) ⋯ = F

Tactic:
rw [Functor.assoc, h₂.fac, h₁.fac]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
E : Type u₄
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
inst_3 : Category.{v₄, u₄} E
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
h₁ : StrictUniversalPropertyFixedTarget.{v₁, u₁, v₂, u₂, v₄, u₄} L₁ W₁ E
h₂ : StrictUniversalPropertyFixedTarget.{v₂, u₂, v₃, u₃, v₄, u₄} L₂ W₂ E
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
x x_1 : Functor.{v₃, v₄, u₃, u₄} C₃ E
h : (L₁ ⋙ L₂) ⋙ x = (L₁ ⋙ L₂) ⋙ x_1
⊢ L₁ ⋙ L₂ ⋙ x = L₁ ⋙ L₂ ⋙ x_1

Tactic:
simpa only [Functor.assoc] using h

Premises used: CategoryTheory.Functor.assoc
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
⊢ (W₂.isoClosure.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure

Tactic:
have eq := W₂.isoClosure.inverseImage_map_eq_of_isEquivalence E₂.functor
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
eq : (W₂.isoClosure.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure
⊢ (W₂.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure

Tactic:
rw [MorphismProperty.map_isoClosure] at eq

Premises used: CategoryTheory.MorphismProperty.map_isoClosure
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
eq : (W₂.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure
rw : W₂ ≤ W₂.isoClosure
⊢ W₂ ≤ W₂'.inverseImage E₂.functor

Tactic:
rw [eq]
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
eq : (W₂.map E₂.functor).inverseImage E₂.functor = W₂.isoClosure
⊢ W₂ ≤ W₂.isoClosure

Tactic:
apply W₂.le_isoClosure

Premises used: CategoryTheory.MorphismProperty.le_isoClosure
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
⊢ W₂' ≤ W₂'

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
⊢ Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')

Tactic:
have := LocalizerMorphism.IsLocalizedEquivalence.of_equivalence Φ (by rfl)
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
⊢ (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂

Tactic:
calc
      _ ≅ L₁ ⋙ E₂.functor ⋙ W₂'.Q ⋙ E₃.inverse :=
          Functor.associator _ _ _ ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm _ ≪≫
            Functor.associator _ _ _
      _ ≅ L₁ ⋙ L₂ ⋙ E₃.functor ⋙ E₃.inverse :=
          isoWhiskerLeft _ ((Functor.associator _ _ _).symm ≪≫
            isoWhiskerRight (Φ.catCommSq L₂ W₂'.Q).iso E₃.inverse ≪≫ Functor.associator _ _ _)
      _ ≅ L₁ ⋙ L₂ := isoWhiskerLeft _ (isoWhiskerLeft _ E₃.unitIso.symm ≪≫ L₂.rightUnitor)

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.associator, CategoryTheory.Equivalence.functor, CategoryTheory.CatCommSq.iso, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
⊢ W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)

Tactic:
simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse,
      MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp, CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
⊢ W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)

Tactic:
have hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q) := by
    simpa only [← MorphismProperty.IsInvertedBy.iff_comp _ _ E₃.inverse,
      MorphismProperty.IsInvertedBy.iff_of_iso W₃ iso] using hW₃
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
⊢ (fun (x : MorphismProperty.{v₂, u₂} C₂) ↦ x.map E₂.functor) (W₃.map L₁) ≤ W₃.map W₁.Q

Tactic:
simpa only [W₃.map_map]
      using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁))

Premises used: CategoryTheory.MorphismProperty.map_map, CategoryTheory.MorphismProperty.Q, CategoryTheory.MorphismProperty.map_eq_of_iso, CategoryTheory.Localization.compUniqFunctor, le_of_eq
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
⊢ W₂' ≤ W₃.map W₁.Q

Tactic:
have hW₂₃' : W₂' ≤ W₃.map W₁.Q := (MorphismProperty.monotone_map E₂.functor hW₂₃).trans
    (by simpa only [W₃.map_map]
      using le_of_eq (W₃.map_eq_of_iso (compUniqFunctor L₁ W₁.Q W₁)))
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
⊢ (W₁.Q ⋙ W₂'.Q).IsLocalization W₃

Tactic:
IsLocalization.mk' _ _ ?_ ?_

Premises used: CategoryTheory.Functor.IsLocalization.mk'
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
refine_1 : StrictUniversalPropertyFixedTarget (W₁.Q ⋙ W₂'.Q) W₃ W₂'.Localization
refine_2 : StrictUniversalPropertyFixedTarget (W₁.Q ⋙ W₂'.Q) W₃ W₃.Localization
⊢ (W₁.Q ⋙ W₂'.Q).IsLocalization W₃

Tactic:
refine IsLocalization.mk' _ _ ?_ ?_

Premises used: CategoryTheory.Functor.IsLocalization.mk'
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
⊢ StrictUniversalPropertyFixedTarget (W₁.Q ⋙ W₂'.Q) W₃ W₂'.Localization

Tactic:
exact (StrictUniversalPropertyFixedTarget.comp
        (strictUniversalPropertyFixedTargetQ W₁ _)
        (strictUniversalPropertyFixedTargetQ W₂' _) W₃ hW₃' hW₁₃ hW₂₃')

Premises used: CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.comp