[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X
[PROOFSTEP]
ext
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X)).hom =
    ((Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X).hom
[PROOFSTEP]
dsimp [equivalence, Equivalence.mk]
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ NatTrans.app (liftNatTrans L₂ W₂ (F ⋙ G') L₂ (F' ⋙ G') (𝟭 D₂) β.hom) (L₂.obj X) =
    NatTrans.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom X ≫ NatTrans.app β.hom X
[PROOFSTEP]
rw [liftNatTrans_app]
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ NatTrans.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom X ≫
      NatTrans.app β.hom X ≫ NatTrans.app (Lifting.iso L₂ W₂ L₂ (𝟭 D₂)).inv X =
    NatTrans.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom X ≫ NatTrans.app β.hom X
[PROOFSTEP]
dsimp [Lifting.iso]
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ G'.map (NatTrans.app (Lifting.iso' W₂).hom X) ≫ NatTrans.app β.hom X ≫ 𝟙 (L₂.obj X) =
    G'.map (NatTrans.app (Lifting.iso' W₂).hom X) ≫ NatTrans.app β.hom X
[PROOFSTEP]
rw [comp_id]
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf =>
  by
  obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
  exact
    ((MorphismProperty.RespectsIso.isomorphisms _).arrow_mk_iso_iff (W₂.Q.mapArrow.mapIso e)).1
      (Localization.inverts W₂.Q W₂ _ hf')
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso ((E.functor ⋙ MorphismProperty.Q W₂).map f)
[PROOFSTEP]
obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
[GOAL]
case intro.intro.intro.intro.intro
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
w✝¹ w✝ : C₂
f' : w✝¹ ⟶ w✝
hf' : W₂ f'
e : Arrow.mk f' ≅ Arrow.mk (E.functor.map f)
⊢ IsIso ((E.functor ⋙ MorphismProperty.Q W₂).map f)
[PROOFSTEP]
exact
  ((MorphismProperty.RespectsIso.isomorphisms _).arrow_mk_iso_iff (W₂.Q.mapArrow.mapIso e)).1
    (Localization.inverts W₂.Q W₂ _ hf')
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : MorphismProperty.IsInvertedBy W₁ (E.functor ⋙ MorphismProperty.Q W₂)
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
exact
  { inverts := hW₂
    nonempty_isEquivalence :=
      ⟨Localization.isEquivalence W₂.Q W₂ L₁ W₁ L₂ (Construction.lift L₂ hW₂) (E.functor ⋙ W₂.Q)
          (Localization.lift (E.functor ⋙ W₂.Q) h L₁)
          (by
            calc
              L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
              _ ≅ _ := (isoWhiskerRight E.counitIso.symm _)
              _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ := (Functor.associator _ _ _)
              _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                (isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight iso _))
              _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q := (isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁))
              _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
              _ ≅ 𝟭 C₂ ⋙ W₂.Q := (isoWhiskerRight E.counitIso _)
              _ ≅ W₂.Q := leftUnitor _)
          (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Lifting.iso W₂.Q W₂ _ _) ≪≫ iso)⟩ }
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : MorphismProperty.IsInvertedBy W₁ (E.functor ⋙ MorphismProperty.Q W₂)
⊢ L₂ ⋙ lift (E.functor ⋙ MorphismProperty.Q W₂) h L₁ ≅ MorphismProperty.Q W₂
[PROOFSTEP]
calc
  L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
  _ ≅ _ := (isoWhiskerRight E.counitIso.symm _)
  _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ := (Functor.associator _ _ _)
  _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
    (isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight iso _))
  _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q := (isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁))
  _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
  _ ≅ 𝟭 C₂ ⋙ W₂.Q := (isoWhiskerRight E.counitIso _)
  _ ≅ W₂.Q := leftUnitor _
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{u_1, u_1} C₁
inst✝⁵ : Category.{u_2, u_2} C₂
inst✝⁴ : Category.{?u.32200, u_3} D
inst✝³ : Category.{u_6, u_4} D₁
inst✝² : Category.{u_7, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
haveI : (E.functor ⋙ L₂).IsLocalization W₁ := of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{u_1, u_1} C₁
inst✝⁵ : Category.{u_2, u_2} C₂
inst✝⁴ : Category.{?u.32200, u_3} D
inst✝³ : Category.{u_6, u_4} D₁
inst✝² : Category.{u_7, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
this : IsLocalization (E.functor ⋙ L₂) W₁
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
exact of_equivalence_source (E.functor ⋙ L₂) W₁ L₂ W₂ E hW₁ hW₂ (Iso.refl _)
