Module: Mathlib.CategoryTheory.Localization.Composition

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty 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₂' := { functor := E₂.functor, map := ⋯ }
this : Φ.IsLocalizedEquivalence
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans
    (Trans.trans
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (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 L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor 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:
refine IsLocalization.mk' _ _ ?_ ?_

Goal state after:
case refine_1
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty 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₂' := { functor := E₂.functor, map := ⋯ }
this : Φ.IsLocalizedEquivalence
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans
    (Trans.trans
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (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 L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor 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

case refine_2
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty 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₂' := { functor := E₂.functor, map := ⋯ }
this : Φ.IsLocalizedEquivalence
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans
    (Trans.trans
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (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 L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor 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